In Conference Proceedings

  1. On Solving Universally Quantified Horn Clauses (PDF), in SAS 2013, with Nikolaj Bjørner and Ken McMillan

  2. Solving Existentially Quantified Horn Clauses (PDF), in CAV 2013, with Tewodros A. Beyene and Corneliu Popeea

  3. Synthesizing Software Verifiers from Proof Rules (PDF), in PLDI 2012, with Sergey Grebenshchikov Nuno P. Lopes and Corneliu Popeea

  4. Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs (PDF), in POPL 2011, with Ashutosh Gupta and Corneliu Popeea

  5. Distributed and Predictable Software Model Checking (PDF), in VMCAI 2011, with Nuno Lopes

  6. A Multi-Modal Framework for Achieving Accountability in Multi-Agent Systems (PDF), in LIS 2010, with Simon Kramer

  7. Constraint Solving for Verification: Theory and Practice by Example (PDF) and slides, in CAV 2010

  8. Approximation and Randomization for Quantitative Information-Flow Analysis (PDF), in CSF 2010, with Boris Köpf

  9. Applying Prolog to Develop Distributed Systems (PDF), in ICLP 2010, with Nuno Lopes, Juan Navarro Pérez and Atul Singh

  10. Finding Heap-Bounds For Hardware Synthesis (PDF), in FMCAD 2009, with Byron Cook, Ashutosh Gupta, Stephen Magill, Jiri Simsa, Satnam Singh and Viktor Vafeiadis

  11. Subsumer-First: Steering Symbolic Reachability Analysis (PDF), in SPIN 2009, with Rishabh Singh

  12. Cardinality Analysis for Declarative Networking (PDF), in CAV'2009, with Juan Navarro Pérez and Atul Singh

  13. An Efficient Invariant Generator (PDF), in CAV'2009, with Ashutosh Gupta

  14. Automatic Discovery and Quantification of Information Leaks (PDF), in S&P'2009, with Michael Backes and Boris Köpf

  15. From Tests To Proofs (PDF), in TACAS'2009 (best paper award at ETAPS'2009), with Ashutosh Gupta and Rupak Majumdar

  16. Verifying Liveness for Asynchronous Programs (PDF), in POPL'2009, with Pierre Ganty and Rupak Majumdar

  17. Operational Semantics for Declarative Networking (PDF), in PADL'2009, with Juan Navarro Pérez

  18. Heap Assumptions on Demand (PDF), in CAV'2008 , with Andreas Podelski and Thomas Wies

  19. Proving Conditional Termination (PDF), in CAV'2008 , with Byron Cook, Sumit Gulwani, Tal Lev-Ami and Mooly Sagiv

  20. Proving Non-Termination (PDF), in POPL'2008 , with Ashutosh Gupta, Thomas Henzinger, Rupak Majumdar and Ru-Gang Xu

  21. Precise Thread-Modular Verification (PDF to appear soon), in SAS'2007 , with Alexander Malkis and Andreas Podelski

  22. Path Invariants (PDF), in PLDI'2007 , with Dirk Beyer, Thomas Henzinger and Rupak Majumdar

  23. Proving Thread Termination (PDF), in PLDI'2007 , with Byron Cook and Andreas Podelski

  24. Invariant Synthesis for Combined Theories (PDF), in VMCAI'2007 , with Dirk Beyer, Thomas Henzinger and Rupak Majumdar

  25. Constraint Solving for Interpolation (PDF), in VMCAI'2007 , with Viorica Sofronie-Stokkermans

  26. ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement (PDF), in PADL'2007 , with Andreas Podelski

  27. Proving That Programs Eventually Do Something Good (PDF), in POPL'2007 , with Byron Cook, Alexey Gotsman, Andreas Podelski and Moshe Vardi

  28. Thread-Modular Verification is Cartesian Abstract Interpretation (PDF), in ICTAC'2006 , with Alexander Malkis and Andreas Podelski

  29. Model Checking Duration Calculus: A Practical Approach (PDF), in ICTAC'2006 , with Roland Meyer and Johannes Faber

  30. Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL (PDF), in MOCHART'06 , with Jürg Hoffmann, Jan-Georg Smaus, Sebastian Kupferschmid and Andreas Podelski

  31. Terminator: Beyond safety (tool description) (PDF), in CAV'2006 , with Byron Cook and Andreas Podelski

  32. Termination proofs for systems code (PDF), in PLDI'2006 , with Byron Cook and Andreas Podelski

  33. Abstraction-refinement for termination (PDF), in SAS'2005 , with Byron Cook and Andreas Podelski

  34. Separating fairness and well-foundedness for the analysis of fair discrete systems (PDF), in TACAS'2005, with Amir Pnueli and Andreas Podelski

  35. Transition predicate abstraction and fair termination (PDF), in POPL'2005, with Andreas Podelski

  36. Transition invariants (PDF), in LICS'2004, with Andreas Podelski

  37. A complete method for the synthesis of linear ranking functions (PDF), in VMCAI'2004, with Andreas Podelski

In Journals

  1. Constraint solving for interpolation PDF, in JSC (journal version of VMCAI'2007 paper) with Viorica Sofronie-Stokkermans

  2. Proving program termination (PDF), in CACM, with Byron Cook and Andreas Podelski

  3. Summarization for termination: no return! (PDF), in FMSD, with Byron Cook and Andreas Podelski

  4. Model Checking Duration Calculus: A Practical Approach (PDF), in FACS. Invited journal version of ICTAC'2006 paper, with Roland Meyer, Johannes Faber and Jochen Hoenicke

  5. Transition Predicate Abstraction and Fair Termination (PDF), in TOPLAS. Invited journal version of POPL'2005 paper, with Andreas Podelski

Technical Reports

  1. Heap Assumptions on Demand (PDF), University of Freiburg Technical Report , 2008. Exteded version of CAV'2008 paper, with Andreas Podelski and Thomas Wies

  2. Path Invariants (PDF), EPFL Technical Report MTC-003, 2006. Exteded version of PLDI'2007 paper, with Dirk Beyer, Thomas Henzinger and Rupak Majumdar

  3. Software Model Checking of Liveness Properties via Transition Invariants (PDF), MPI Technical Report 2-004, 2003, with Andreas Podelski


  1. Temporal Verification with Transition Invariants (PDF), PhD Thesis, Universität des Saarlandes, 2004

  2. A Model Checker Based on Abstraction Refinement (PDF), Master's thesis, Universität des Saarlandes, 2002

The documents referenced above are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright.