| Publication | Date of Publication | Type |
|---|
Global guidance for local generalization in model checking
Formal Methods in System Design | 2024-11-04 | Paper |
Property directed self composition
Computer Aided Verification | 2024-02-16 | Paper |
Verification of threshold-based distributed algorithms by decomposition to decidable logics
Computer Aided Verification | 2024-02-16 | Paper |
Inferring inductive invariants from phase structures
Computer Aided Verification | 2024-02-16 | Paper |
Inferring invariants with quantifier alternations: taming the search space explosion
| 2024-01-23 | Paper |
Fast approximations of quantifier elimination
| 2024-01-12 | Paper |
Quantifiers on demand
Automated Technology for Verification and Analysis | 2023-07-28 | Paper |
Modular verification of concurrent programs via sequential model checking
Automated Technology for Verification and Analysis | 2023-07-28 | Paper |
Invariant inference with provable complexity from the monotone theory
Static Analysis | 2023-07-28 | Paper |
SAT-based invariant inference and its relation to concept learning
Lecture Notes in Computer Science | 2023-07-21 | Paper |
Order out of chaos: proving linearizability using local views
| 2022-07-21 | Paper |
Synthesis with abstract examples
| 2022-07-01 | Paper |
Temporal prophecy for proving temporal properties of infinite-state systems
Formal Methods in System Design | 2021-12-08 | Paper |
Run-time complexity bounds using squeezers
| 2021-10-18 | Paper |
Global guidance for local generalization in model checking
| 2021-02-09 | Paper |
Putting the squeeze on array programs: loop verification via inductive rank reduction
| 2020-08-05 | Paper |
Solving \(\mathrm{LIA}^\star\) using approximations
| 2020-08-05 | Paper |
Bounded quantifier instantiation for checking inductive invariants
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Abstraction-based interaction model for synthesis
Lecture Notes in Computer Science | 2020-07-07 | Paper |
Programming by predicates: a formal model for interactive synthesis
Acta Informatica | 2020-03-06 | Paper |
Automated circular assume-guarantee reasoning
FM 2015: Formal Methods | 2019-12-19 | Paper |
Some complexity results for stateful network verification
Formal Methods in System Design | 2019-11-18 | Paper |
Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
Static Analysis | 2019-09-16 | Paper |
Bounded quantifier instantiation for checking inductive invariants
| 2019-09-13 | Paper |
Automated circular assume-guarantee reasoning with N-way decomposition and alphabet refinement
Computer Aided Verification | 2019-05-03 | Paper |
Automated circular assume-guarantee reasoning
Formal Aspects of Computing | 2018-09-12 | Paper |
Property-directed inference of universal invariants or proving their absence
Journal of the ACM | 2018-08-02 | Paper |
Property-directed inference of universal invariants or proving their absence
| 2018-03-01 | Paper |
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
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 |
IC3 -- flipping the E in ICE
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 |
Symbolic automata for representing big code
Acta Informatica | 2016-06-28 | Paper |
\(D^3\): data-driven disjunctive abstraction
Lecture Notes in Computer Science | 2016-03-23 | Paper |
Property directed abstract interpretation
Lecture Notes in Computer Science | 2016-03-23 | Paper |
A framework for compositional verification of multi-valued systems via abstraction-refinement
Information and Computation | 2016-03-10 | Paper |
Symbolic automata for static specification mining
Static Analysis | 2014-01-21 | Paper |
Intertwined forward-backward reachability analysis using interpolants
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
Multi-valued model checking games
Journal of Computer and System Sciences | 2012-05-11 | Paper |
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Compositional verification and 3-valued abstractions join forces
Information and Computation | 2010-02-26 | Paper |
A framework for compositional verification of multi-valued systems via abstraction-refinement
Automated Technology for Verification and Analysis | 2009-12-01 | Paper |
Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules
Studia Logica | 2009-03-17 | Paper |
Compositional Verification and 3-Valued Abstractions Join Forces
Static Analysis | 2009-03-03 | Paper |
3-valued abstraction: More precision at less cost
Information and Computation | 2008-12-03 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
Information and Computation | 2007-08-23 | Paper |
Automated Technology for Verification and Analysis
Lecture Notes in Computer Science | 2006-10-10 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2005-12-06 | Paper |
