CAV 2009
60 papers
- A Concurrent Portfolio Approach to SMT Solving
- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints
- An Antichain Algorithm for LTL Realizability
- Apron: A Library of Numerical Abstract Domains for Static Analysis
- Automated Analysis of Java Methods for Confidentiality
- Automatic Verification of Integer Array Programs
- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
- Better Quality in Synthesis through Quantitative Objectives
- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep
- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs
- Cardinality Abstraction for Declarative Networking Applications
- Centaur Technology Media Unit Verification
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Component-Based Construction of Real-Time Systems in BIP
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- D-Finder: A Tool for Compositional Deadlock Detection and Verification
- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
- Explaining Counterexamples Using Causality
- Games through Nested Fixpoints
- Generalizing DPLL to Richer Logics
- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
- Homer: A Higher-Order Observational Equivalence Model checkER
- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment
- INFAMY: An Infinite-State Markov Model Checker
- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion
- Incremental Instance Generation in Local Reasoning
- Intra-module Inference
- InvGen: An Efficient Invariant Generator
- Linear Functional Fixed-points
- MCMAS: A Model Checker for the Verification of Multi-Agent Systems
- Meta-analysis for Atomicity Violations under Nested Locking
- Mixed-Signal System Verification: A High-Speed Link Example
- Modelling Epigenetic Information Maintenance: A Kappa Tutorial
- Models and Proofs of Protocol Security: A Progress Report
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
- On Extending Bounded Proofs to Inductive Proofs
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
- PAT: Towards Flexible Verification under Fairness
- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?
- Priority Scheduling of Distributed Systems Based on Model Checking
- Quantifier Elimination via Functional Composition
- Reachability Analysis of Hybrid Systems Using Support Functions
- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
- Reducing Test Inputs Using Information Partitions
- Regression Verification: Proving the Equivalence of Similar Programs
- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation
- Requirements Validation for Hybrid Systems
- SPEED: Symbolic Complexity Bound Analysis
- Size-Change Termination, Monotonicity Constraints and Ranking Functions
- Sliding Window Abstraction for Infinite Markov Chains
- Software Transactional Memory on Relaxed Memory Models
- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
- Symbolic Counter Abstraction for Concurrent Software
- TASS: Timing Analyzer of Scenario-Based Specifications
- The Zonotope Abstract Domain Taylor1+
- Towards Performance Prediction of Compositional Models in Industrial GALS Designs
- Transactional Memory: Glimmer of a Theory
- Translation Validation: From Simulink to C
- VS3: SMT Solvers for Program Verification