Proceedings of the 24th 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

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

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

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.

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.