Software Engineering
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. 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.
