| 2009 | Towards Performance Prediction of Compositional Models in Industrial GALS Designs. | Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe |
| 2009 | Requirements Validation for Hybrid Systems. | Alessandro Cimatti, Marco Roveri, Stefano Tonetta |
| 2009 | Automated Analysis of Java Methods for Confidentiality. | Pavol Cern, Rajeev Alur |
| 2009 | Automatic Verification of Integer Array Programs. | Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecn, Toms Vojnar |
| 2009 | HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment. | Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, Franck Vdrine |
| 2009 | Better Quality in Synthesis through Quantitative Objectives. | Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann |
| 2009 | Linear Functional Fixed-points. | Nikolaj S. Bjrner, Joe Hendrix |
| 2009 | D-Finder: A Tool for Compositional Deadlock Detection and Verification. | Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis |
| 2009 | Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?. | Luca Benini |
| 2009 | Size-Change Termination, Monotonicity Constraints and Ranking Functions. | Amir M. Ben-Amram |
| 2009 | Explaining Counterexamples Using Causality. | Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler |
| 2009 | Priority Scheduling of Distributed Systems Based on Model Checking. | Ananda Basu, Saddek Bensalem, Doron A. Peled, Joseph Sifakis |
| 2009 | Symbolic Counter Abstraction for Concurrent Software. | Grard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
| 2009 | Models and Proofs of Protocol Security: A Progress Report. | Martn Abadi, Bruno Blanchet, Hubert Comon-Lundh |
| 2008 | Scalable Shape Analysis for Systems Code. | Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2008 | Abstract Interpretation with Applications to Timing Validation. | Reinhard Wilhelm, Bjrn Wachter |
| 2008 | An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. | Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel |
| 2008 | Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. | Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby |
| 2008 | Heap Assumptions on Demand. | Andreas Podelski, Andrey Rybalchenko, Thomas Wies |
| 2008 | Computing Differential Invariants of Hybrid Systems as Fixedpoints. | Andr Platzer, Edmund M. Clarke |
| 2008 | Linear Arithmetic with Stars. | Ruzica Piskac, Viktor Kuncak |
| 2008 | Tutorial on Separation Logic (Invited Tutorial). | Peter W. O'Hearn |
| 2008 | Discriminative Model Checking. | Peter Niebert, Doron A. Peled, Amir Pnueli |
| 2008 | Enhancing Program Verification with Lemmas. | Huu Hai Nguyen, Wei-Ngan Chin |
| 2008 | Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. | Laura I. Meikle, Jacques D. Fleuriot |