| Publication | Date of Publication | Type |
|---|
Inferring inductive invariants from phase structures
Computer Aided Verification | 2024-02-16 | Paper |
Precise interprocedural dataflow analysis with applications to constant propagation
TAPSOFT '95: Theory and Practice of Software Development | 2022-08-18 | Paper |
| Verifying equivalence of Spark programs | 2022-08-12 | Paper |
Temporal prophecy for proving temporal properties of infinite-state systems
Formal Methods in System Design | 2021-12-08 | Paper |
Bounded quantifier instantiation for checking inductive invariants
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Some complexity results for stateful network verification
Formal Methods in System Design | 2019-11-18 | Paper |
Bounded quantifier instantiation for checking inductive invariants
(available as arXiv preprint) | 2019-09-13 | Paper |
Constrained image generation using binarized neural networks with decision procedures
(available as arXiv preprint) | 2018-08-10 | Paper |
On the automated verification of web applications with embedded SQL
(available as arXiv preprint) | 2018-07-18 | Paper |
A framework for numeric analysis of array operations
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2017-07-14 | Paper |
A semantics for procedure local heaps and its abstractions
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2017-07-14 | Paper |
Logical characterizations of heap abstractions
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Lecture Notes in Computer Science | 2017-02-21 | Paper |
Conjunctive abstract interpretation using paramodulation
Lecture Notes in Computer Science | 2017-02-21 | Paper |
Decidability of inferring inductive invariants
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Decentralizing SDN policies
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-09-29 | Paper |
A combination framework for tracking partition sizes
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-07-03 | Paper |
Specifying and verifying sparse matrix codes
Proceedings of the 15th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
Checking linearizability of encapsulated extended operations
Programming Languages and Systems | 2014-04-16 | Paper |
Modular reasoning about heap paths via effectively propositional formulas
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Solving geometry problems using a combination of symbolic and numerical reasoning
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
| Automatically verifying concurrent queue algorithms | 2013-08-30 | Paper |
Synthesis of circular compositional program proofs via abduction
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
Eventually consistent transactions
Programming Languages and Systems | 2012-06-22 | Paper |
Reasoning about lock placements
Programming Languages and Systems | 2012-06-22 | Paper |
Statically inferring complex heap, array, and numeric invariants
Static Analysis | 2010-10-01 | Paper |
Decidable fragments of many-sorted logic
Journal of Symbolic Computation | 2009-12-03 | Paper |
Generalizing DPLL to Richer Logics
Computer Aided Verification | 2009-06-30 | Paper |
Simulating reachability using first-order logic with applications to verification of linked data structures
Logical Methods in Computer Science | 2009-06-30 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
Static Analysis | 2009-03-12 | Paper |
Labelled Clauses
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Heap Decomposition for Concurrent Shape Analysis
Static Analysis | 2008-08-28 | Paper |
Proving Conditional Termination
Computer Aided Verification | 2008-07-15 | Paper |
Thread Quantification for Concurrent Shape Analysis
Computer Aided Verification | 2008-07-15 | Paper |
Local Reasoning for Storable Locks and Threads
Programming Languages and Systems | 2008-05-15 | Paper |
Decidable Fragments of Many-Sorted Logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
Ranking Abstractions
Programming Languages and Systems | 2008-04-11 | Paper |
Constructing Specialized Shape Analyses for Uniform Change
Lecture Notes in Computer Science | 2008-04-04 | Paper |
Comparison Under Abstraction for Verifying Linearizability
Computer Aided Verification | 2007-11-29 | Paper |
Leaping Loops in the Presence of Abstraction
Computer Aided Verification | 2007-11-29 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Self-stabilization Preserving Compiler
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Abstract Counterexample-Based Refinement for Powerset Domains
Program Analysis and Compilation, Theory and Practice | 2007-09-24 | Paper |
An Appreciation of the Work of Reinhard Wilhelm
Program Analysis and Compilation, Theory and Practice | 2007-09-24 | Paper |
Refinement-Based Verification for Possibly-Cyclic Lists
Program Analysis and Compilation, Theory and Practice | 2007-09-24 | Paper |
Shape Analysis by Graph Decomposition
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
A logic of reachable patterns in linked data-structures
The Journal of Logic and Algebraic Programming | 2007-08-23 | Paper |
Scaling model checking of dataraces using dynamic information
Journal of Parallel and Distributed Computing | 2007-05-23 | Paper |
Foundations of Software Science and Computation Structures
Lecture Notes in Computer Science | 2007-05-02 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2006-10-31 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2005-12-06 | Paper |
Establishing local temporal heap safety properties with applications to compile-time memory management
Science of Computer Programming | 2005-10-10 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2005-08-24 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2005-08-24 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2005-08-22 | Paper |
Finding circular attributes in attribute grammars
Journal of the ACM | 2005-01-25 | Paper |
| scientific article; zbMATH DE number 2090863 (Why is no real title available?) | 2004-08-13 | Paper |
| scientific article; zbMATH DE number 2087562 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 1956555 (Why is no real title available?) | 2003-07-30 | Paper |
| scientific article; zbMATH DE number 1956566 (Why is no real title available?) | 2003-07-30 | Paper |
| scientific article; zbMATH DE number 1948397 (Why is no real title available?) | 2003-07-13 | Paper |
| scientific article; zbMATH DE number 1832225 (Why is no real title available?) | 2002-11-19 | Paper |
| scientific article; zbMATH DE number 1693492 (Why is no real title available?) | 2002-01-22 | Paper |
| scientific article; zbMATH DE number 1629945 (Why is no real title available?) | 2001-11-06 | Paper |
| scientific article; zbMATH DE number 1617328 (Why is no real title available?) | 2001-07-11 | Paper |
| scientific article; zbMATH DE number 1617320 (Why is no real title available?) | 2001-07-11 | Paper |
| scientific article; zbMATH DE number 1251180 (Why is no real title available?) | 1999-02-17 | Paper |
A logic-based approach to program flow analysis
Acta Informatica | 1998-11-08 | Paper |
Precise interprocedural dataflow analysis with applications to constant propagation
Theoretical Computer Science | 1997-02-27 | Paper |
