21. CAV 2009: Grenoble, France
Ahmed Bouajjani, Oded Maler (Eds.): Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Springer 2009 Lecture Notes in Computer Science ISBN 978-3-642-02657-7
Invited Tutorials
- Jaeha Kim: Mixed-Signal System Verification: A High-Speed Link Example. 16
- Jean Krivine, Vincent Danos, Arndt Benecke: Modelling Epigenetic Information Maintenance: A Kappa Tutorial. 17-32
- Joseph Sifakis: Component-Based Construction of Real-Time Systems in BIP. 33-34
Invited Talks
- Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh: Models and Proofs of Protocol Security: A Progress Report. 35-49
- Luca Benini: Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?. 50
- Sumit Gulwani: SPEED: Symbolic Complexity Bound Analysis. 51-62
- Ofer Strichman: Regression Verification: Proving the Equivalence of Similar Programs. 63
Regular Papers
- Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening: Symbolic Counter Abstraction for Concurrent Software. 64-78
- Ananda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis: Priority Scheduling of Distributed Systems Based on Model Checking. 79-93
- Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler: Explaining Counterexamples Using Causality. 94-108
- Amir M. Ben-Amram: Size-Change Termination, Monotonicity Constraints and Ranking Functions. 109-123
- Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann: Better Quality in Synthesis through Quantitative Objectives. 140-156
- Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecný, Tomás Vojnar: Automatic Verification of Integer Array Programs. 157-172
- Alessandro Cimatti, Marco Roveri, Stefano Tonetta: Requirements Validation for Hybrid Systems. 188-203
- Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe: Towards Performance Prediction of Compositional Models in Industrial GALS Designs. 204-218
- Thao Dang, David Salinas: Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. 219-232
- Isil Dillig, Thomas Dillig, Alex Aiken: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. 233-247
- Azadeh Farzan, P. Madhusudan, Francesco Sorrentino: Meta-analysis for Atomicity Violations under Nested Locking. 248-262
- Emmanuel Filiot, Naiyong Jin, Jean-François Raskin: An Antichain Algorithm for LTL Realizability. 263-277
- Yeting Ge, Leonardo Mendonça de Moura: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. 306-320
- Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh: Software Transactional Memory on Relaxed Memory Models. 321-336
- Thomas A. Henzinger, Maria Mateescu, Verena Wolf: Sliding Window Abstraction for Infinite Markov Chains. 337-352
- Swen Jacobs: Incremental Instance Generation in Local Reasoning. 368-382
- Jie-Hong R. Jiang: Quantifier Elimination via Functional Composition. 383-397
- Vineet Kahlon, Chao Wang, Aarti Gupta: Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. 398-413
- Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. 414-429
- Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, K. C. Shashidhar: Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. 430-445
- Nathan Kitchen, Andreas Kuehlmann: A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints. 446-461
- Salvatore La Torre, P. Madhusudan, Gennaro Parlato: Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. 477-492
- Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies: Intra-module Inference. 493-508
- Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric: Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. 509-524
- Peter Lammich, Markus Müller-Olm, Alexander Wenner: Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. 525-539
- Colas Le Guernic, Antoine Girard: Reachability Analysis of Hybrid Systems Using Support Functions. 540-554
- David Monniaux: On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. 570-583
- Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh: Cardinality Abstraction for Declarative Networking Applications. 584-598
- Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe: Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences. 599-613
Tool Papers
- Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis: D-Finder: A Tool for Compositional Deadlock Detection and Verification. 614-619
- Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, Franck Védrine: HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment. 620-626
- Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang: INFAMY: An Infinite-State Markov Model Checker. 641-647
- Sylvain Hallé, Roger Villemaire: Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep. 648-653
- David Hopkins, C.-H. Luke Ong: Homer: A Higher-Order Observational Equivalence Model checkER. 654-660
- Bertrand Jeannet, Antoine Miné: Apron: A Library of Numerical Abstract Domains for Static Analysis. 661-667
- Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia: Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. 668-674
- Pallavi Joshi, Mayur Naik, Chang-Seo Park, Koushik Sen: CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs. 675-681
- Alessio Lomuscio, Hongyang Qu, Franco Raimondi: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. 682-688
- Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster: VS3: SMT Solvers for Program Verification. 702-708
- Jun Sun, Yang Liu, Jin Song Dong, Jun Pang: PAT: Towards Flexible Verification under Fairness. 709-714
- Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura: A Concurrent Portfolio Approach to SMT Solving. 715-720
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T214307 by the dblp team