| Publication | Date of Publication | Type |
|---|
| Lockstep composition for unbalanced loops | 2024-04-05 | Paper |
Quantified invariants via syntax-guided synthesis
Computer Aided Verification | 2024-02-16 | Paper |
| Maximizing branch coverage with constrained Horn clauses | 2024-02-01 | Paper |
| Transition power abstractions for deep counterexample detection | 2024-01-23 | Paper |
SMT-based verification of program changes through summary repair
Formal Methods in System Design | 2023-10-30 | Paper |
Solving constrained Horn clauses over algebraic data types
Lecture Notes in Computer Science | 2023-08-17 | Paper |
Syntax-guided termination analysis
Computer Aided Verification | 2023-05-26 | Paper |
Exploiting synchrony and symmetry in relational verification
Computer Aided Verification | 2023-05-26 | Paper |
Fold/unfold transformations for fixpoint logic
Tools and Algorithms for the Construction and Analysis of Systems | 2021-11-10 | Paper |
| Bridging arrays and ADTs in recursive proofs | 2021-10-18 | Paper |
| Farkas-based tree interpolation | 2021-10-18 | Paper |
| Unbounded procedure summaries from bounded environments | 2021-10-18 | Paper |
Learning inductive invariants by sampling from frequency distributions
Formal Methods in System Design | 2021-02-08 | Paper |
| Synthesizing environment invariants for modular hardware verification | 2020-08-05 | Paper |
| Lazy but effective functional synthesis | 2020-01-23 | Paper |
Exploiting partial variable assignment in interpolation-based model checking
Formal Methods in System Design | 2019-11-29 | Paper |
Function summarization modulo theories
EPiC Series in Computing | 2019-07-04 | Paper |
Property directed equivalence via abstract simulation
Computer Aided Verification | 2019-05-03 | Paper |
Synchronizing constrained Horn clauses
EPiC Series in Computing | 2019-01-10 | Paper |
| Theory refinement for program verification | 2017-11-15 | Paper |
Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
Lecture Notes in Computer Science | 2016-04-01 | Paper |
Automated discovery of simulation between programs
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
eVolCheck: incremental upgrade checker for C
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
