A Sample of Three

[2017] Java Generics Are Turing Complete (arXiv, code)

[2016] Proving the Herman-Protocol Conjecture (arXiv, blog post)

[2014] On Abstraction Refinement for Program Analyses in Datalog (pdf, bib, blog post, talk, my slides, Xin's slides, Hongseok's slides)

By Year

[2018] Selective Monitoring (draft)

[2018] PrideMM: a Solver for Relaxed Memory Models (draft)

[2017] On the Quest for an Acyclic Graph (arXiv)

[2017] Effective Static Resolution of Static Analysis Alarms (pdf)

[2017] Maximum Satisfiability in Software Analysis: Applications and Techniques (pdf, invited tutorial at CAV)

[2017] Java Generics Are Turing Complete (arXiv, code)

[2016] Proving the Herman-Protocol Conjecture (arXiv, blog post)

[2016] Abstraction Refinement Guided by a Learnt Probabilistic Model (arXiv, experiments)

[2015] Tree Buffers (arXiv, slides, blog post)

[2014] On Abstraction Refinement for Program Analyses in Datalog (pdf, bib, blog post, talk, my slides, Xin's slides, Hongseok's slides, distinguished paper award at PLDI)

[2013] On QBF Proofs and Preprocessing (arXiv, bib, tools and experiment logs, blog post)

[2013] History-Register Automata (arXiv, bib)

[2013] Runtime Verification Based on Register Automata (arXiv, bib, code, slides, talk)

[2011] TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs (pdf, bib)

[2011] jStar-eclipse: An IDE for Automatic Verification of Java Programs (pdf, bib, website)

[2011] coreStar: The Core of jStar (pdf, bib, slides, website)

[2010] Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription (arXiv, bib)

[2010] The Design and Algorithms of a Verification Condition Generator (pdf, bib, code)

[2010] How to Complete an Interactive Configuration Process? (arXiv, bib)

[2009] Strongest Postcondition of Unstructured Programs (pdf, bib)

[2009] CLOPS: A DSL for Command Line Options (pdf, bib, website)

[2007] Edit and Verify (arXiv, bib, proofs)

[2007] Reachability Analysis for Annotated Code (pdf, bib)

[2005] Constructing Checkers from PSL Properties (pdf, bib)

---

Last updated: 1 February 2018