Ahmed Bouajjani, Oded Maler
Proceedings of the 21st International Conference on Computer Aided Verification
CAV, 2009.

@proceedings{CAV-2009,
	address       = "Grenoble, France",
	doi           = "10.1007/978-3-642-02658-4",
	editor        = "Ahmed Bouajjani and Oded Maler",
	isbn          = "978-3-642-02657-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 21st International Conference on Computer Aided Verification}",
	volume        = 5643,
	year          = 2009,
}

Event page: http://www-cav2009.imag.fr/

Contents (60 items)

13 ×#named
9 ×#verification
7 ×#using
6 ×#concurrent
5 ×#modelling
5 ×#performance
5 ×#source code
4 ×#model checking
4 ×#proving
4 ×#smt

CAV-2009-GuerraouiK #memory management #transaction

Transactional Memory: Glimmer of a Theory (RG, MK), pp. 1–15.

CAV-2009-Kim #performance #verification

Mixed-Signal System Verification: A High-Speed Link Example (JK), p. 16.

CAV-2009-KrivineDB #maintenance #modelling #tutorial

Modelling Epigenetic Information Maintenance: A Kappa Tutorial (JK, VD, AB), pp. 17–32.

CAV-2009-Sifakis #component #realtime

Component-Based Construction of Real-Time Systems in BIP (JS), pp. 33–34.

CAV-2009-AbadiBC #modelling #protocol #proving #security

Models and Proofs of Protocol Security: A Progress Report (MA, BB, HCL), pp. 35–49.

CAV-2009-Benini #manycore #performance #predict #question

Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? (LB), p. 50.

CAV-2009-Gulwani #analysis #bound #complexity #named

SPEED: Symbolic Complexity Bound Analysis (SG), pp. 51–62.

CAV-2009-Strichman #equivalence #proving #source code #verification

Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.

CAV-2009-BaslerMWK #abstraction #concurrent

Symbolic Counter Abstraction for Concurrent Software (GB, MM, TW, DK), pp. 64–78.

CAV-2009-BasuBPS #distributed #model checking #scheduling

Priority Scheduling of Distributed Systems Based on Model Checking (AB, SB, DP, JS), pp. 79–93.

CAV-2009-BeerBCOT #using

Explaining Counterexamples Using Causality (IB, SBD, HC, AO, RJT), pp. 94–108.

CAV-2009-Ben-Amram #constraints #ranking #termination

Size-Change Termination, Monotonicity Constraints and Ranking Functions (AMBA), pp. 109–123.

CAV-2009-BjornerH #fixpoint #functional #linear

Linear Functional Fixed-points (NB, JH), pp. 124–139.

CAV-2009-BloemCHJ #quality #synthesis

Better Quality in Synthesis through Quantitative Objectives (RB, KC, TAH, BJ), pp. 140–156.

CAV-2009-BozgaHIKV #array #automation #integer #source code #verification

Automatic Verification of Integer Array Programs (MB, PH, RI, FK, TV), pp. 157–172.

CAV-2009-CernyA #analysis #automation #java

Automated Analysis of Java Methods for Confidentiality (PC, RA), pp. 173–187.

CAV-2009-CimattiRT #hybrid #requirements #validation

Requirements Validation for Hybrid Systems (AC, MR, ST), pp. 188–203.

CAV-2009-CosteHLS #composition #design #industrial #modelling #performance #predict #towards

Towards Performance Prediction of Compositional Models in Industrial GALS Designs (NC, HH, EL, WS), pp. 204–218.

CAV-2009-DangS #image #polynomial #using

Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion (TD, DS), pp. 219–232.

CAV-2009-DilligDA #integer #linear #proving

Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers (ID, TD, AA), pp. 233–247.

CAV-2009-FarzanMS

Meta-analysis for Atomicity Violations under Nested Locking (AF, PM, FS), pp. 248–262.

CAV-2009-FiliotJR #algorithm #ltl

An Antichain Algorithm for LTL Realizability (EF, NJ, JFR), pp. 263–277.

CAV-2009-FuhrmannH #bound #induction #on the #proving

On Extending Bounded Proofs to Inductive Proofs (OF, SH), pp. 278–290.

CAV-2009-GawlitzaS #fixpoint #game studies

Games through Nested Fixpoints (TG, HS), pp. 291–305.

CAV-2009-GeM #modulo theories #quantifier #satisfiability

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (YG, LMdM), pp. 306–320.

CAV-2009-GuerraouiHS #memory management #modelling #transaction

Software Transactional Memory on Relaxed Memory Models (RG, TAH, VS), pp. 321–336.

CAV-2009-HenzingerMW #abstraction #infinity #markov

Sliding Window Abstraction for Infinite Markov Chains (TAH, MM, VW), pp. 337–352.

CAV-2009-HuntS #verification

Centaur Technology Media Unit Verification (WAHJ, SS), pp. 353–367.

CAV-2009-Jacobs #generative #incremental #reasoning

Incremental Instance Generation in Local Reasoning (SJ), pp. 368–382.

CAV-2009-Jiang #composition #functional #quantifier

Quantifier Elimination via Functional Composition (JHRJ), pp. 383–397.

CAV-2009-KahlonWG #partial order #reduction

Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique (VK, CW, AG), pp. 398–413.

CAV-2009-KaivolaGNTWPSTFRN #execution #testing #validation #verification

Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation (RK, RG, NN, AT, JW, SP, AS, CT, VF, ER, AN), pp. 414–429.

CAV-2009-KanadeAIRSS #generative #modelling

Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models (AK, RA, FI, SR, SS, KCS), pp. 430–445.

CAV-2009-KitchenK #constraints #integer #markov #monte carlo

A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints (NK, AK), pp. 446–461.

CAV-2009-McMillanKS #logic

Generalizing DPLL to Richer Logics (KLM, AK, MS), pp. 462–476.

CAV-2009-TorreMP #bound #concurrent #reachability

Reducing Context-Bounded Concurrent Reachability to Sequential Reachability (SLT, PM, GP), pp. 477–492.

CAV-2009-LahiriQGVW

Intra-module Inference (SKL, SQ, JPG, JWV, TW), pp. 493–508.

CAV-2009-LahiriQR #concurrent #detection #fault #precise #smt #using

Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers (SKL, SQ, ZR), pp. 509–524.

CAV-2009-LammichMW #automaton #constraints #network #set

Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints (PL, MMO, AW), pp. 525–539.

CAV-2009-GuernicG #analysis #hybrid #reachability #using

Reachability Analysis of Hybrid Systems Using Support Functions (CLG, AG), pp. 540–554.

CAV-2009-MajumdarX #testing #using

Reducing Test Inputs Using Information Partitions (RM, RGX), pp. 555–569.

CAV-2009-Monniaux #float #linear #on the #using

On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure (DM), pp. 570–583.

CAV-2009-PerezRS #abstraction #declarative #network

Cardinality Abstraction for Declarative Networking Applications (JANP, AR, AS), pp. 584–598.

CAV-2009-VerdoolaegeJB #equivalence #source code #using

Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences (SV, GJ, MB), pp. 599–613.

CAV-2009-BensalemBNS #composition #concurrent #detection #named #verification

D-Finder: A Tool for Compositional Deadlock Detection and Verification (SB, MB, THN, JS), pp. 614–619.

CAV-2009-BouissouGPTV #named #source code

HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment (OB, EG, SP, KT, FV), pp. 620–626.

CAV-2009-GhorbalGP #abstract domain

The Zonotope Abstract Domain Taylor1+ (KG, EG, SP), pp. 627–633.

CAV-2009-GuptaR #generative #invariant #named #performance

InvGen: An Efficient Invariant Generator (AG, AR), pp. 634–640.

CAV-2009-HahnHWZ #infinity #markov #model checking #named

INFAMY: An Infinite-State Markov Model Checker (EMH, HH, BW, LZ), pp. 641–647.

CAV-2009-HalleV #contract #interface #web

Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep (SH, RV), pp. 648–653.

CAV-2009-HopkinsO #equivalence #higher-order #model checking #named

Homer: A Higher-Order Observational Equivalence Model checkER (DH, CHLO), pp. 654–660.

CAV-2009-JeannetM #abstract domain #library #named #static analysis

Apron: A Library of Numerical Abstract Domains for Static Analysis (BJ, AM), pp. 661–667.

CAV-2009-JhaLS #named #performance #smt

Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic (SJ, RL, SAS), pp. 668–674.

CAV-2009-JoshiNPS #concurrent #framework #named #source code #testing

CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs (PJ, MN, CSP, KS), pp. 675–681.

CAV-2009-LomuscioQR #model checking #multi #named #verification

MCMAS: A Model Checker for the Verification of Multi-Agent Systems (AL, HQ, FR), pp. 682–688.

CAV-2009-PanBL #named #specification

TASS: Timing Analyzer of Scenario-Based Specifications (MP, LB, XL), pp. 689–695.

CAV-2009-RyabtsevS #c #validation

Translation Validation: From Simulink to C (MR, OS), pp. 696–701.

CAV-2009-SrivastavaGF #named #smt #verification

VS3: SMT Solvers for Program Verification (SS, SG, JSF), pp. 702–708.

CAV-2009-SunLDP #flexibility #named #towards #verification

PAT: Towards Flexible Verification under Fairness (JS, YL, JSD, JP), pp. 709–714.

CAV-2009-WintersteigerHM #approach #concurrent #smt

A Concurrent Portfolio Approach to SMT Solving (CMW, YH, LMdM), pp. 715–720.