VMCAI 2005

30 papers

1. Abstract Interpretation with Alien Expressions and Heap Structures · Bor-Yuh Evan Chang, K. Rustan M. Leino
2. Abstraction for Liveness · Amir Pnueli
3. An Overview of Semantics for the Validation of Numerical Programs · Matthieu Martel
4. Automata as Abstractions · Dennis Dams, Kedar S. Namjoshi
5. Checking Herbrand Equalities and Beyond · Markus Müller-Olm, Oliver Rüthing, Helmut Seidl
6. Cryptographic Protocol Analysis on Real C Code · Jean Goubault-Larrecq, Fabrice Parrennes
7. Don't Know in the µ-Calculus · Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham
8. Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives · Stephen F. Siegel
9. Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs · Paul C. Attie, Hana Chockler
10. Generalized Typestate Checking for Data Structure Consistency · Patrick Lam, Viktor Kuncak, Martin C. Rinard
11. I/O Efficient Directed Model Checking · Shahid Jabbar, Stefan Edelkamp
12. Information Flow Analysis for Java Bytecode · Samir Genaim, Fausto Spoto
13. Minimizing Counterexample with Unit Core Extraction and Incremental SAT · ShengYu Shen, Ying Qin, Sikun Li
14. Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties · Laura Bozzelli
15. Model Checking of Systems Employing Commutative Functions · A. Prasad Sistla, Min Zhou, Xiaodong Wang
16. On the Complexity of Error Explanation · Nirman Kumar, Viraj Kumar, Mahesh Viswanathan
17. Optimizing Bounded Model Checking for Linear Hybrid Systems · Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen
18. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists · Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv
19. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming · Patrick Cousot
20. Purity and Side Effect Analysis for Java Programs · Alexandru Salcianu, Martin C. Rinard
21. Scalable Analysis of Linear Systems Using Mathematical Programming · Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna
22. Shape Analysis by Predicate Abstraction · Ittai Balaban, Amir Pnueli, Lenore D. Zuck
23. Simple Is Better: Efficient Bounded Model Checking for Past LTL · Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
24. Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs · Julien Bertrane
25. Termination of Polynomial Programs · Aaron R. Bradley, Zohar Manna, Henny B. Sipma
26. The Arithmetic-Geometric Progression Abstract Domain · Jérôme Feret
27. The Verifying Compiler, a Grand Challenge for Computing Research · C. A. R. Hoare
28. Verification of an Error Correcting Code by Abstract Interpretation · Charles Hymans
29. Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement · Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin
30. Weak Automata for the Linear Time µ-Calculus · Martin Lange