P. Madhusudan, Sanjit A. Seshia
Proceedings of the 24th International Conference on Computer Aided Verification
CAV, 2012.

@proceedings{CAV-2012,
	address       = "Berkeley, California, USA",
	doi           = "10.1007/978-3-642-31424-7",
	editor        = "P. Madhusudan and Sanjit A. Seshia",
	isbn          = "978-3-642-31423-0",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 24th International Conference on Computer Aided Verification}",
	volume        = 7358,
	year          = 2012,
}

Event page: http://cav12.cs.illinois.edu/

Contents (64 items)

16 ×#named
10 ×#source code
8 ×#verification
7 ×#model checking
5 ×#abstraction
5 ×#analysis
5 ×#synthesis
4 ×#automaton
4 ×#parallel
4 ×#probability

CAV-2012-Thomas #challenge #synthesis

Synthesis and Some of Its Challenges (WT), p. 1.

CAV-2012-Dill #biology #model checking

Model Checking Cell Biology (DLD), p. 2.

CAV-2012-BodikT #constraints #source code #theorem proving

Synthesizing Programs with Constraint Solvers (RB, ET), p. 3.

CAV-2012-Bradley #incremental #induction #verification

IC3 and beyond: Incremental, Inductive Verification (ARB), p. 4.

CAV-2012-Myers #search-based #verification

Formal Verification of Genetic Circuits (CJM), p. 5.

CAV-2012-Moskal #bound #c #infinity #verification

From C to Infinity and Back: Unbounded Auto-active Verification with VCC (MM), p. 6.

CAV-2012-KretinskyE #automaton #ltl

Deterministic Automata for the (F, G)-Fragment of LTL (JK, JE), pp. 7–22.

CAV-2012-BrazdilCKN #game studies #multi #performance #synthesis

Efficient Controller Synthesis for Consumption Games with Multiple Resource Types (TB, KC, AK, PN), pp. 23–38.

CAV-2012-Ehlers #ltl #synthesis

ACTL ∩ LTL Synthesis (RE), pp. 39–54.

CAV-2012-ChenW #incremental #learning

Learning Boolean Functions Incrementally (YFC, BYW), pp. 55–70.

CAV-2012-SharmaNA #classification

Interpolants as Classifiers (RS, AVN, AA), pp. 71–87.

CAV-2012-LeeWY #algorithm #analysis #learning #termination

Termination Analysis with Algorithmic Learning (WL, BYW, KY), pp. 88–104.

CAV-2012-BrockschmidtMOG #automation #java #proving #source code #termination

Automated Termination Proofs for Java Programs with Cyclic Data (MB, RM, CO, JG), pp. 105–122.

CAV-2012-EsparzaGK #probability #proving #source code #termination #using

Proving Termination of Probabilistic Programs Using Patterns (JE, AG, SK), pp. 123–138.

CAV-2012-Venet #analysis #difference #invariant #linear #scalability

The Gauge Domain: Scalable Analysis of Linear Inequality Invariants (AV), pp. 139–154.

CAV-2012-BerdineCIW #abstraction #analysis

Diagnosing Abstraction Failure for Separation Logic-Based Analyses (JB, AC, SI, CMW), pp. 155–173.

CAV-2012-ThakurR #symbolic computation

A Method for Symbolic Computation of Abstract Operations (AVT, TWR), pp. 174–192.

CAV-2012-RolliniSS #model checking

Leveraging Interpolant Strength in Model Checking (SFR, OS, NS), pp. 193–209.

CAV-2012-AtigBEL #detection #parallel #source code #thread

Detecting Fair Non-termination in Multithreaded Programs (MFA, AB, ME, AL), pp. 210–226.

CAV-2012-KahlonW #concurrent #source code

Lock Removal for Concurrent Trace Programs (VK, CW), pp. 227–242.

CAV-2012-SchellhornWD #algorithm #how

How to Prove Algorithms Linearisable (GS, HW, JD), pp. 243–259.

CAV-2012-HagueL #analysis #bound #parallel #source code #thread

Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters (MH, AWL), pp. 260–276.

CAV-2012-CimattiG #model checking

Software Model Checking via IC3 (AC, AG), pp. 277–293.

CAV-2012-GuetGHMS #markov #search-based

Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits (CCG, AG, TAH, MM, AS), pp. 294–309.

CAV-2012-KomuravelliPC #abstraction #probability #refinement

Assume-Guarantee Abstraction Refinement for Probabilistic Systems (AK, CSP, EMC), pp. 310–326.

CAV-2012-JegourelLS #model checking #optimisation #parametricity #statistics

Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking (CJ, AL, SS), pp. 327–342.

CAV-2012-ZutshiST #abstraction #relational

Timed Relational Abstractions for Sampled Data Control Systems (AZ, SS, AT), pp. 343–361.

CAV-2012-MajumdarZ #approximate #modelling

Approximately Bisimilar Symbolic Models for Digital Control Systems (RM, MZ), pp. 362–377.

CAV-2012-CimattiCLNRRST #industrial #validation #verification

Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System (AC, RC, AL, IN, TR, MR, AS, AT), pp. 378–393.

CAV-2012-DilligDMA #smt

Minimum Satisfying Assignments for SMT (ID, TD, KLM, AA), pp. 394–409.

CAV-2012-HanJ #satisfiability

When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way (CSH, JHRJ), pp. 410–426.

CAV-2012-LalQL #modulo theories #reachability

A Solver for Reachability Modulo Theories (AL, SQ, SKL), pp. 427–443.

CAV-2012-GuhaNA #automaton #bisimulation #decidability #on the

On Decidability of Prebisimulation for Timed Automata (SG, CN, SAK), pp. 444–461.

CAV-2012-HasuoS #hybrid #standard #static analysis

Exercises in Nonstandard Static Analysis of Hybrid Systems (IH, KS), pp. 462–478.

CAV-2012-BogomolovFGLPW #analysis #distance #reachability

A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx (SB, GF, RG, HL, AP, MW), pp. 479–494.

CAV-2012-Mador-HaimMSMAOAMSW #axiom #memory management #multi

An Axiomatic Memory Model for POWER Multiprocessors (SMH, LM, SS, KM, JA, SO, RA, MMKM, PS, DW), pp. 495–512.

CAV-2012-PaulaHN #debugging #named #nondeterminism

nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces (FMdP, AJH, AN), pp. 513–531.

CAV-2012-HassanBS #incremental #induction #model checking

Incremental, Inductive CTL Model Checking (ZH, ARB, FS), pp. 532–547.

CAV-2012-FredriksonJJRPSY #abstraction #performance #policy #refinement #runtime #using

Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement (MF, RJ, SJ, TWR, PAP, HS, VY), pp. 548–563.

CAV-2012-KopfMO #automation #quantifier

Automatic Quantification of Cache Side-Channels (BK, LM, MO), pp. 564–580.

CAV-2012-HarrisJR #automaton #game studies #programming #safety

Secure Programming via Visibly Pushdown Safety Games (WRH, SJ, TWR), pp. 581–598.

CAV-2012-SinhaSCS

Alternate and Learn: Finding Witnesses without Looking All over (NS, NS, SC, MS), pp. 599–615.

CAV-2012-ChuJ #reduction #safety #symmetry #verification

A Complete Method for Symmetry Reduction in Safety Verification (DHC, JJ), pp. 616–633.

CAV-2012-SinghG

Synthesizing Number Transformations from Input-Output Examples (RS, SG), pp. 634–651.

CAV-2012-BohyBFJR #ltl #synthesis

Acacia+, a Tool for LTL Synthesis (AB, VB, EF, NJ, JFR), pp. 652–657.

CAV-2012-ChengGRBK #automation #industrial #named #synthesis

MGSyn: Automatic Synthesis for Industrial Automation (CHC, MG, HR, CB, AK), pp. 658–664.

CAV-2012-DriscollTR #automaton #library #named

OpenNWA: A Nested-Word Automaton Library (ED, AVT, TWR), pp. 665–671.

CAV-2012-AlbarghouthiLGC #framework #named #verification

Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification (AA, YL, AG, MC), pp. 672–678.

CAV-2012-AlbertiBGRS #abstraction #array #named #smt

SAFARI: SMT-Based Abstraction for Arrays with Interpolants (FA, RB, SG, SR, NS), pp. 679–685.

CAV-2012-BenqueBCCFIPTV #biology #modelling #named #network #visual notation

Bma: Visual Tool for Modeling and Analyzing Biological Networks (DB, SB, CC, BC, JF, SI, NP, AST, MYV), pp. 686–692.

CAV-2012-KieferMOWW #named #probability #source code

APEX: An Analyzer for Open Probabilistic Programs (SK, ASM, JO, BW, JW), pp. 693–698.

CAV-2012-ArmstrongGLOPRW

Recent Developments in FDR (PJA, MG, GL, JO, HP, AWR, JW), pp. 699–704.

CAV-2012-SongSLD #model checking #probability #realtime

A Model Checker for Hierarchical Probabilistic Real-Time Systems (SS, JS, YL, JSD), pp. 705–711.

CAV-2012-LahiriHKR #imperative #named #semantics #source code

SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs (SKL, CH, MK, HR), pp. 712–717.

CAV-2012-ConchonGKMZ #model checking #named #parallel #smt

Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems — Tool Paper (SC, AG, SK, AM, FZ), pp. 718–724.

CAV-2012-Tiwari #relational

HybridSAL Relational Abstracter (AT), pp. 725–731.

CAV-2012-ChaudhuriS #named #optimisation #source code

Euler: A System for Numerical Optimization of Programs (SC, ASL), pp. 732–737.

CAV-2012-SinghS #named #programming

SPT: Storyboard Programming Tool (RS, ASL), pp. 738–743.

CAV-2012-RondonBKJ #c #named #verification

CSolve: Verifying C with Liquid Types (PMR, AB, MK, RJ), pp. 744–750.

CAV-2012-Schwartz-NarbonneLAM #debugging #named #parallel #source code

passert: A Tool for Debugging Parallel Programs (DSN, FL, DIA, SM), pp. 751–757.

CAV-2012-JaffarMNS #execution #named #symbolic computation #verification

TRACER: A Symbolic Execution Tool for Verification (JJ, VM, JAN, AES), pp. 758–766.

CAV-2012-ArltS #detection #java #named

Joogie: Infeasible Code Detection for Java (SA, MS), pp. 767–773.

CAV-2012-HopkinsMO #equivalence #higher-order #ml #named

Hector: An Equivalence Checker for a Higher-Order Fragment of ML (DH, ASM, CHLO), pp. 774–780.

CAV-2012-0002AH #ml

Resource Aware ML (JH, KA, MH), pp. 781–786.