Werner Damm, Holger Hermanns
Proceedings of the 19th International Conference on Computer Aided Verification
CAV, 2007.

@proceedings{CAV-2007,
	address       = "Berlin, Germany",
	editor        = "Werner Damm and Holger Hermanns",
	isbn          = "978-3-540-73367-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 19th International Conference on Computer Aided Verification}",
	volume        = 4590,
	year          = 2007,
}

Event page: http://www.cav2007.org/

Contents (54 items)

15 ×#verification
9 ×#named
8 ×#abstraction
8 ×#analysis
5 ×#model checking
4 ×#hybrid
4 ×#satisfiability
4 ×#source code
3 ×#bound
3 ×#composition

CAV-2007-Cook #automation #proving #termination

Automatically Proving Program Termination (BC), p. 1.

CAV-2007-Russinoff #approach #verification

A Mathematical Approach to RTL Verification (DMR), p. 2.

CAV-2007-Kropf #debugging #development #formal method #industrial #question

Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? (TK), p. 3.

CAV-2007-BeyerHS #algorithm #interface #synthesis

Algorithms for Interface Synthesis (DB, TAH, VS), pp. 4–19.

CAV-2007-MouraDS #modulo theories #satisfiability #tutorial

A Tutorial on Satisfiability Modulo Theories (LMdM, BD, NS), pp. 20–36.

CAV-2007-LeavensKP #behaviour #composition #functional #java #ml #specification #tutorial #verification

A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java (GTL, JRK, EP), p. 37.

CAV-2007-Franzle #hybrid #verification

Verification of Hybrid Systems (MF), p. 38.

CAV-2007-SinhaC #composition #lazy evaluation #learning #satisfiability #using #verification

SAT-Based Compositional Verification Using Lazy Learning (NS, EMC), pp. 39–54.

CAV-2007-CohenN #proving #safety

Local Proofs for Global Safety Properties (AC, KSN), pp. 55–67.

CAV-2007-GopanR #analysis #library #low level #summary

Low-Level Library Analysis and Summarization (DG, TWR), pp. 68–81.

CAV-2007-ChakiSV #bound #verification

Verification Across Intellectual Property Boundaries (SC, CS, HV), pp. 82–94.

CAV-2007-MalerNP #bound #on the

On Synthesizing Controllers from Bounded-Response Properties (OM, DN, AP), pp. 95–107.

CAV-2007-AlfaroF #algorithm #game studies

An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games (LdA, MF), pp. 108–120.

CAV-2007-BehrmannCDFLL #exclamation #game studies #named

UPPAAL-Tiga: Time for Playing Games! (GB, AC, AD, EF, KGL, DL), pp. 121–125.

CAV-2007-OuimetL #realtime #simulation #specification #tool support #verification

The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems (MO, KL), pp. 126–130.

CAV-2007-JonssonS #model checking

Systematic Acceleration in Regular Model Checking (BJ, MS), pp. 131–144.

CAV-2007-AbdullaDR #infinity #process #verification

Parameterized Verification of Infinite-State Processes with Global Conditions (PAA, GD, AR), pp. 145–157.

CAV-2007-GaravelMLS #analysis #distributed #process

CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes (HG, RM, FL, WS), pp. 158–163.

CAV-2007-SuwimonteerabuthBSE #java #named #source code #testing

jMoped: A Test Environment for Java Programs (DS, FB, SS, JE), pp. 164–167.

CAV-2007-CharltonH #analysis #model checking #named #plugin

Hector: Software Model Checking with Cooperating Analysis Plugins (NC, MH), pp. 168–172.

CAV-2007-FilliatreM #deduction #framework #platform #verification #why

The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (JCF, CM), pp. 173–177.

CAV-2007-BerdineCCDOWY #analysis #data type

Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.

CAV-2007-JhalaM #abstraction #array #proving

Array Abstractions from Proofs (RJ, KLM), pp. 193–206.

CAV-2007-BouajjaniFQ #analysis #bound #parallel #source code #thread

Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures (AB, SF, SQ), pp. 207–220.

CAV-2007-BogudlovLRS #analysis #parametricity

Revamping TVLA: Making Parametric Shape Analysis Competitive (IB, TLA, TWR, MS), pp. 221–225.

CAV-2007-KahlonYSG #concurrent #detection #performance #source code

Fast and Accurate Static Data-Race Detection for Concurrent Programs (VK, YY, SS, AG), pp. 226–239.

CAV-2007-ChenR #parametricity #slicing

Parametric and Sliced Causality (FC, GR), pp. 240–253.

CAV-2007-PatinST #named #parallel #recursion #source code #thread #verification

Spade: Verification of Multithreaded Dynamic and Recursive Programs (GP, MS, TT), pp. 254–257.

CAV-2007-JobstmannGWB #named #synthesis

Anzu: A Tool for Property Synthesis (BJ, SJG, MW, RB), pp. 258–262.

CAV-2007-BloemCPRT #analysis #formal method #named #requirements

RAT: A Tool for the Formal Analysis of Requirements (RB, RC, IP, MR, AT), pp. 263–267.

CAV-2007-EzekielLC #generative

Parallelising Symbolic State-Space Generators (JE, GL, GC), pp. 268–280.

CAV-2007-BarnatBS #detection #performance

I/O Efficient Accepting Cycle Detection (JB, LB, PS), pp. 281–293.

CAV-2007-BrummayerB #c #named #satisfiability

C32SAT: Checking C Expressions (RB, AB), pp. 294–297.

CAV-2007-BarrettT

CVC3 (CB, CT), pp. 298–302.

CAV-2007-ManoliosSV #analysis #named

BAT: The Bit-Level Analysis Tool (PM, SKS, DV), pp. 303–306.

CAV-2007-BeckerDEK #constraints #integer #linear #named

LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals (BB, CD, JE, FK), pp. 307–310.

CAV-2007-KatoenKLW #abstraction #markov

Three-Valued Abstraction for Continuous-Time Markov Chains (JPK, DK, ML, VW), pp. 311–324.

CAV-2007-AlfaroR #abstraction #markov #process

Magnifying-Lens Abstraction for Markov Decision Processes (LdA, PR), pp. 325–338.

CAV-2007-MatsliahS #approximate #encryption #model checking #random

Underapproximation for Model-Checking Based on Random Cryptographic Constructions (AM, OS), pp. 339–351.

CAV-2007-WangYGI #precise #reachability #using

Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra (CW, ZY, AG, FI), pp. 352–365.

CAV-2007-BabicH #abstraction #verification

Structural Abstraction of Software Verification Conditions (DB, AJH), pp. 366–378.

CAV-2007-GulwaniT #abstract domain #bytecode #low level

An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software (SG, AT), pp. 379–392.

CAV-2007-Wahl #adaptation #reduction #symmetry

Adaptive Symmetry Reduction (TW), pp. 393–405.

CAV-2007-KupfermanPV #liveness

From Liveness to Promptness (OK, NP, MYV), pp. 406–419.

CAV-2007-GuptaMF #automation #composition #generative #verification

Automated Assumption Generation for Compositional Verification (AG, KLM, ZF), pp. 420–432.

CAV-2007-Segelken #abstraction #automaton #hybrid #linear #model checking #modelling

Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models (MS), pp. 433–448.

CAV-2007-NahhalD #hybrid #test coverage

Test Coverage for Continuous and Hybrid Systems (TN, TD), pp. 449–462.

CAV-2007-PlakuKV #hybrid #verification

Hybrid Systems: From Verification to Falsification (EP, LEK, MYV), pp. 463–476.

CAV-2007-AmitRRSY #abstraction #comparison #verification

Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.

CAV-2007-BallKS #abstraction

Leaping Loops in the Presence of Abstraction (TB, OK, MS), pp. 491–503.

CAV-2007-BeyerHT #configuration management #convergence #model checking #program analysis #verification

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (DB, TAH, GT), pp. 504–518.

CAV-2007-GaneshD #array

A Decision Procedure for Bit-Vectors and Arrays (VG, DLD), pp. 519–531.

CAV-2007-CimattiRST #abstraction #logic #satisfiability

Boolean Abstraction for Temporal Logic Satisfiability (AC, MR, VS, ST), pp. 532–546.

CAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt #verification

A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.