# Selected

[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)

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

# Refereed

[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)

[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
Generation*
(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)

# Unrefereed

[2007] *Generating Code and Documentation from
Lightweight Abstract Grammars*
(pdf)

[2003] *Modele de Trafic pentru Retele de Date*
(pdf)

Last updated: 14 May 2016