# 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