Publications

In Conference Proceedings

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

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

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

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

  5. Constraint Solving for Verification: Theory and Practice by Example (PDF), in CAV 2011

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theses

  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.