Papers

DBLP.
Bibtex Entries.
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. Preliminary version available upon request.
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.