Publications

In Conference Proceedings

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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

In Journals

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


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


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


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


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

Technical Reports

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


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


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

Theses

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


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