VMCAI 2009

29 papers

1. A PosterioriSoundness for Non-deterministic Abstract Interpretations · Matthew Might, Panagiotis Manolios
2. A Scalable Memory Model for Low-Level Code · Zvonimir Rakamaric, Alan J. Hu
3. Abstraction Refinement for Probabilistic Software · Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker
4. Advances in Program Termination and Liveness · Byron Cook
5. An Abort-Aware Model of Transactional Programming · Kousha Etessami, Patrice Godefroid
6. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries · Johannes Kinder, Florian Zuleger, Helmut Veith
7. An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking · Rotem Oshman
8. Average-Price-per-Reward Games on Hybrid Automata with Strong Resets · Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski
9. Constraint-Based Invariant Inference over Predicate Abstraction · Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan
10. Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking · Ralf Wimmer, Bettina Braitling, Bernd Becker
11. Deciding Extensions of the Theories of Vectors and Bags · Patrick Maier
12. Extending Symmetry Reduction by Exploiting System Architecture · Richard J. Trefler, Thomas Wahl
13. Finding Concurrency-Related Bugs Using Random Isolation · Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri
14. LTL Generalized Model Checking Revisited · Patrice Godefroid, Nir Piterman
15. Mixed Transition Systems Revisited · Ou Wei, Arie Gurfinkel, Marsha Chechik
16. Model Checking Concurrent Programs · Aarti Gupta
17. Model Checking: Progress and Problems · E. Allen Emerson
18. Model-Checking the Linux Virtual File System · Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu Siminiceanu
19. Monitoring the Full Range of omega-Regular Properties of Stochastic Systems · Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla
20. Mostly-Functional Behavior in Java Programs · William C. Benton, Charles N. Fischer
21. Query-Driven Program Testing · Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
22. Reducing Behavioural to Structural Properties of Programs with Procedures · Dilian Gurov, Marieke Huisman
23. Shape-Value Abstraction for Verifying Linearizability · Viktor Vafeiadis
24. SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities · Vincent Laviron, Francesco Logozzo
25. Synthesizing Switching Logic Using Constraint Solving · Ankur Taly, Sumit Gulwani, Ashish Tiwari
26. The Higher-Order Aggregate Update Problem · Christos Dimoulas, Mitchell Wand
27. Thread-Modular Shape Analysis · Mooly Sagiv
28. Towards Automatic Stability Analysis for Rely-Guarantee Proofs · Hasan Amjad, Richard Bornat
29. Verification of Security Protocols · Véronique Cortier