Proceedings of the 21st International Conference on Computer Aided Verification
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
DOI
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.