21. CAV 2009: Grenoble, France

Invited Tutorials

• Rachid Guerraoui, Michal Kapalka:
  Transactional Memory: Glimmer of a Theory. 1-15
  
• 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
  
• Nikolaj Bjørner, Joe Hendrix:
  Linear Functional Fixed-points. 124-139
  
• 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
  
• Pavol Cerný, Rajeev Alur:
  Automated Analysis of Java Methods for Confidentiality. 173-187
  
• 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
  
• Oded Fuhrmann, Shlomo Hoory:
  On Extending Bounded Proofs to Inductive Proofs. 278-290
  
• Thomas Gawlitza, Helmut Seidl:
  Games through Nested Fixpoints. 291-305
  
• 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
  
• Warren A. Hunt Jr., Sol Swords:
  Centaur Technology Media Unit Verification. 353-367
  
• 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
  
• Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv:
  Generalizing DPLL to Richer Logics. 462-476
  
• 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
  
• Rupak Majumdar, Ru-Gang Xu:
  Reducing Test Inputs Using Information Partitions. 555-569
  
• 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
  
• Khalil Ghorbal, Eric Goubault, Sylvie Putot:
  The Zonotope Abstract Domain Taylor1+. 627-633
  
• Ashutosh Gupta, Andrey Rybalchenko:
  InvGen: An Efficient Invariant Generator. 634-640
  
• 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
  
• Minxue Pan, Lei Bu, Xuandong Li:
  TASS: Timing Analyzer of Scenario-Based Specifications. 689-695
  
• Michael Ryabtsev, Ofer Strichman:
  Translation Validation: From Simulink to C. 696-701
  
• 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