In Conference Proceedings

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

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

  3. Cardinality Analysis for Declarative Networking (PDF), in CAV'2009, with Juan Navarro Perez and Atul Singh

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

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

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

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

  8. Operational Semantics for Declarative Networking (PDF), in PADL'2009, with Juan Navarro Perez

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

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

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

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

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

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

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

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

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

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

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

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

  21. 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

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

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

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

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

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

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

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

In Journals

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

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

  3. 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

  4. 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.