# Andreas Podelski - Papers

- DBLP.

- Model Checking of Hybrid Systems: From Reachability to Stability. In Proceedings of HSCC'06: Hybrid Systems: Computation and Control. Santa Barbara, California, March 29--31, 2006.
- Termination proofs for systems code. In Proceedings of PLDI'06: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation. Ottawa, Canada, June 10-16, 2006.
- Transition Predicates and Fair Termination. In: Martín Abadi, editor, Proceedings of POPL'04: Principles of Programming Languages, Long Beach, California, January 2005.
- Transition Invariants. In Proceedings of LICS'04 the 19th IEEE Annual Symposium on Logic in Computer Science, Turku, Finland, July 13 - 17, 2004.
- Software Model Checking for Termination and Liveness via Transition Invariants. Technical report.
- A Complete Method for Synthesis of Linear Ranking Functions. In Proceedings of VMCAI 2004: Verification, Model Checking and Abstract Interpretation. Venice, Italy, January 2004.
- Verification of Cryptographic Protocols: Tagging Enforces Termination. In Andrew Gordon, editor, Proceedings of FoSSaCS'03: Foundations of Software Science and Computation Structures. Warsaw, Poland, April 2003.
- Relative Completeness of Abstraction Refinement for Software Model Checking. In Proceedings of TACAS 2002: Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, France, April 2002.
- Boolean and Cartesian Abstraction for Model Checking C Programs. In Proceedings of TACAS: Tools and Algorithms for the Construction and Analysis of Systems. Genova, Italy, April 2001.
- Model Checking as Constraint Solving. In: Jens Palsberg, editor, Proceedings of SAS'2000: Static Analysis Symposium. Santa Barbara, CA, June 2000.
- Constraint-Based Deductive Model Checking. In STTT Journal.
- Efficient Algorithms for Pre Star and Post Star on Interprocedural Parallel Flow Graphs. In: Tom Reps, editor, Proceedings of POPL'00: Principles of Programming Languages, Boston, January 2000.
- Paths vs. Trees in Set-based Program Analysis. In: Tom Reps, editor, Proceedings of POPL'00: Principles of Programming Languages, Boston, January 2000.
- Beyond Region Graphs: Symbolic Forward Analysis for Timed Automata. In: C. Pandurangan, editor, Proceedings of Foundations of Software Technology and Theoretical Computer Science (FST & TCS '99), Chennai, India, December 13--15, 1999.
- Constraint-Based Analysis of Broadcast Protocols. In: Jorg Flum and Mario Rodriguez-Artalejo, editors, Proceedings of the Computer Science Logic Conference (CSL'99), Madrid, Spain, September 20-25, 1999.
- Widen, Narrow and Relax. Describes the three kinds of abstraction implemented in DMC and used in model checking for infinite-state systems over integers (such as narrowing for the verification of liveness properties of a parametrized elevator program) .
- Model Checking in CLP. In Rance Cleaveland, editor, Proceedings of TACAS'99, the Second International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Amsterdam, 22-26 March, 1999. Springer LNCS. Best Paper Award of EAPLS.
- Set-based Failure Analysis for Logic Programs and Concurrent Constraint Programs. In S. Doaitse Swierstra, editor, Proceedings of ESOP'99, the European Symposium of Programming, Amsterdam, 22-26 March, 1999. Springer LNCS. Presents the `greatest-model'analysis of logic programs with a potential application to the error diagnosis for concurrent constraint programs, whose execution states are (non-ground) atoms in the logic programming sense).
- Directional Type Inference for Logic Programs. In: Giorgio Levi, editor, Proceedings of SAS'98, the International Symposium on Static Analysis, Pisa, September 14 - 16, 1998. Springer LNCS.
- The Horn Mu-Calculus. In: Vaughan Pratt, editor, Proceedings of LICS'98, the 13th IEEE Annual Symposium on Logic in Computer Science, Indianapolis, Indiana, June 21 - 24, 1998. IEEE Press.
- Set-based Analysis of Reactive Infinite-state Systems. Presents a method for abstract verification of CTL properties of reactive systems whose states are modeled as ground atoms of logic programs. In: Bernhard Steffen, editor, Proceedings of TACAS'98, the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal, March 28 - April 4, 1998. Springer LNCS.
- Co-definite Set Constraints. Presents the first algorithm for solving set constraints used in the set-based analysis of non-terminating (reactive) programs with the greatest-fixpoint semantics. In: Tobias Nipkow, editor, Proceedings of RTA'98 - the 9th International Conference on Rewriting Techniques and Applications, Tsukuba, Japan, March-April 1998. Springer LNCS.
- LISA: A Specification Language Based on WS2S. In: Mogens Nielson and Wolfgang Thomas, editors, Proceedings of the Conference for Computer Science Logic - CSL'97 in Aarhus, Denmark, August 23-29, 1997, Springer LNCS.
- Set Constraints - a Pearl in Research on Constraints. Invited tutorial; in: Gert Smolka, editor, Proceedings of the Third International Conference on Constraint Programming, Springer LNCS 1330.
- Verification and Debugging of Concurrent Constraint Programs through Abstract Interpretation with Set Constraints. (Note on preliminary results presented at Dagstuhl Seminar Jan 19-23, 1997).
- Liveness and safety in concurrent constraint programs. (Note on preliminary results).
- Ordering Constraints over Feature Trees (in: Gert Smolka, editor, Proceedings of the Third International Conference on Constraint Programming, Springer LNCS 1330).
- Inclusion Constraints over Non-empty Sets of Trees (in: Michel Bidoit and Max Dauchet, editors, Proceedings of TAPSOFT'97 - the 9th International Joint Conference on Theory and Practice of Software Development, Springer LNCS).
- Set constraints with intersection (in: Glynn Winskel, editor, Proceedings of LICS'97, the 12th IEEE Annual Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2. IEEE Press, 1997). Extended version to appear in LICS'97 Special Issue of Information and Control.