Selected

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

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

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

Refereed

[2014] On Abstraction Refinement for Program Analyses in Datalog (pdf, 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: 8 October 2014