default search action
21st CAV 2009: Grenoble, France
- Ahmed Bouajjani, Oded Maler:
Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science 5643, Springer 2009, ISBN 978-3-642-02657-7
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 A. 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 S. 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
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 A. 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
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é
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
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
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
PAT: Towards Flexible Verification under Fairness. 709-714 - Christoph M. Wintersteiger
A Concurrent Portfolio Approach to SMT Solving. 715-720
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-21 20:17 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: