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

Natasha Sharygina, Helmut Veith
Proceedings of the 25th International Conference on Computer Aided Verification
CAV, 2013.

TEST
DBLP
Scholar
DOI
Full names Links ISxN
@proceedings{CAV-2013,
	address       = "Saint Petersburg, Russia",
	doi           = "10.1007/978-3-642-39799-8",
	editor        = "Natasha Sharygina and Helmut Veith",
	isbn          = "978-3-642-39798-1",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 25th International Conference on Computer Aided Verification}",
	volume        = 8044,
	year          = 2013,
}

Event page: http://cav2013.forsyte.at/

Contents (72 items)

CAV-2013-KovacsV #first-order #proving #theorem proving
First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
CAV-2013-HeizmannHP #automaton #model checking #people
Software Model Checking for People Who Love Automata (MH, JH, AP), pp. 36–52.
CAV-2013-PalikarevaC #execution #multi #symbolic computation
Multi-solver Support in Symbolic Execution (HP, CC), pp. 53–68.
CAV-2013-PauleveAK #approximate #automaton #network #reachability #scalability #set
Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks (LP, GA, HK), pp. 69–84.
CAV-2013-ClaessenFIPW #model checking #network #reachability #set
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets (KC, JF, SI, NP, QW), pp. 85–100.
CAV-2013-ReiterBCN #named
TTP: Tool for Tumor Progression (JGR, IB, KC, MAN), pp. 101–106.
CAV-2013-BrimCDS #model checking #parametricity #probability #using
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking (LB, MC, SD, DS), pp. 107–123.
CAV-2013-EsparzaGM #verification
Parameterized Verification of Asynchronous Shared-Memory Systems (JE, PG, RM), pp. 124–140.
CAV-2013-AlglaveKT #bound #concurrent #model checking #partial order #performance
Partial Orders for Efficient Bounded Model Checking of Concurrent Software (JA, DK, MT), pp. 141–157.
CAV-2013-KloosMNP #incremental #induction
Incremental, Inductive Coverability (JK, RM, FN, RP), pp. 158–173.
CAV-2013-DragoiGH #automation #concurrent #proving
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates (CD, AG, TAH), pp. 174–190.
CAV-2013-FarzanK #bound #named #parallel #static analysis
Duet: Static Analysis for Unbounded Parallelism (AF, ZK), pp. 191–196.
CAV-2013-ArmoniFJ #approach
SVA and PSL Local Variables — A Practical Approach (RA, DF, NJ), pp. 197–212.
CAV-2013-BraibantC #hardware #synthesis #verification
Formal Verification of Hardware Synthesis (TB, AC), pp. 213–228.
CAV-2013-LvSX #named
CacBDD: A BDD Package with Dynamic Cache Management (GL, KS, YX), pp. 229–234.
CAV-2013-BinghamBEG #concurrent #distributed #model checking
Distributed Explicit State Model Checking of Deadlock Freedom (BDB, JDB, JE, MRG), pp. 235–241.
CAV-2013-KongHSHG #generative #hybrid #safety #verification
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems (HK, FH, XS, WNNH, MG), pp. 242–257.
CAV-2013-ChenAS #hybrid
Flow*: An Analyzer for Non-linear Hybrid Systems (XC, , SS), pp. 258–263.
CAV-2013-DonzeFM #monitoring #performance #robust
Efficient Robust Monitoring for STL (AD, TF, OM), pp. 264–279.
CAV-2013-PrabhakarS #abstraction #hybrid #model checking
Abstraction Based Model-Checking of Stability of Hybrid Systems (PP, MGS), pp. 280–295.
CAV-2013-ManciniMMMMT #model checking #simulation #verification
System Level Formal Verification via Model Checking Driven Simulation (TM, FM, AM, IM, FM, ET), pp. 296–312.
CAV-2013-AlbarghouthiM
Beautiful Interpolants (AA, KLM), pp. 313–329.
CAV-2013-VizelRN #generative #performance
Efficient Generation of Small Interpolants in CNF (YV, VR, AN), pp. 330–346.
CAV-2013-RummerHK #verification
Disjunctive Interpolants for Horn-Clause Verification (PR, HH, VK), pp. 347–363.
CAV-2013-DaiXZ #generative #programming
Generating Non-linear Interpolants by Semidefinite Programming (LD, BX, NZ), pp. 364–380.
CAV-2013-KroeningLW #approximate #c #detection #performance #source code
Under-Approximating Loops in C Programs for Fast Counterexample Detection (DK, ML, GW), pp. 381–396.
CAV-2013-GantyG #proving #termination
Proving Termination Starting from the End (PG, SG), pp. 397–412.
CAV-2013-BrockschmidtCF #proving #termination
Better Termination Proving through Cooperation (MB, BC, CF), pp. 413–429.
CAV-2013-AdlerEV #ambiguity #equivalence
Relative Equivalence in the Presence of Ambiguity (OA, CE, TV), pp. 430–446.
CAV-2013-ChagantyLNR #learning #relational #smt #using
Combining Relational Learning with SMT Solvers Using CEGAR (ATC, AL, AVN, SKR), pp. 447–462.
CAV-2013-EsparzaLNNSS #execution #ltl #model checking
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
CAV-2013-AlmagorAK #automation #generative #quality #specification
Automatic Generation of Quality Specifications (SA, GA, OK), pp. 479–494.
CAV-2013-StewartEY #automaton #bound #model checking #polynomial #probability
Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata (AS, KE, MY), pp. 495–510.
CAV-2013-ChakarovS #probability #program analysis
Probabilistic Program Analysis with Martingales (AC, SS), pp. 511–526.
CAV-2013-PuggelliLSS #nondeterminism #polynomial #verification
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties (AP, WL, ALSV, SAS), pp. 527–542.
CAV-2013-ChatterjeeL #algorithm #markov #performance #process
Faster Algorithms for Markov Decision Processes with Low Treewidth (KC, JL), pp. 543–558.
CAV-2013-ChatterjeeGK #automaton #ltl #model checking #probability #synthesis
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis (KC, AG, JK), pp. 559–575.
CAV-2013-JegourelLS #model checking #statistics
Importance Splitting for Statistical Model Checking Rare Properties (CJ, AL, SS), pp. 576–591.
CAV-2013-Marques-SilvaJB #set
Minimal Sets over Monotone Predicates in Boolean Formulae (JMS, MJ, AB), pp. 592–607.
CAV-2013-ChakrabortyMV #generative #satisfiability #scalability
A Scalable and Nearly Uniform Generator of SAT Witnesses (SC, KSM, MYV), pp. 608–623.
CAV-2013-DAntoniV #equivalence #finite #transducer
Equivalence of Extended Symbolic Finite Transducers (LD, MV), pp. 624–639.
CAV-2013-ReynoldsTGK #finite #smt
Finite Model Finding in SMT (AR, CT, AG, SK), pp. 640–655.
CAV-2013-ChengRS #constraints #named #polynomial
JBernstein: A Validity Checker for Generalized Polynomial Constraints (CHC, HR, NS), pp. 656–661.
CAV-2013-ManoliosP #modulo theories
ILP Modulo Theories (PM, VP), pp. 662–677.
CAV-2013-UhlerD #automation #named #query #smt #symbolic computation
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries (RU, ND), pp. 678–683.
CAV-2013-DilligD #abduction #named
Explain: A Tool for Performing Abductive Inference (ID, TD), pp. 684–689.
CAV-2013-ChothiaKN #information management
A Tool for Estimating Information Leakage (TC, YK, CN), pp. 690–695.
CAV-2013-MeierSCB #analysis #protocol #proving #security
The TAMARIN Prover for the Symbolic Analysis of Security Protocols (SM, BS, CC, DAB), pp. 696–701.
CAV-2013-BiondiLTW #imperative #named #security
QUAIL: A Quantitative Security Analyzer for Imperative Code (FB, AL, LMT, AW), pp. 702–707.
CAV-2013-ChevalCP #how #privacy
Lengths May Break Privacy — Or How to Check for Equivalences with Length (VC, VC, AP), pp. 708–723.
CAV-2013-SosnovichGN #network #protocol #security #using
Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems (AS, OG, GN), pp. 724–739.
CAV-2013-HolikLRSV #analysis #automation #automaton
Fully Automated Shape Analysis Based on Forest Automata (LH, OL, AR, JS, TV), pp. 740–755.
CAV-2013-ItzhakyBINS #data type #effectiveness #linked data #open data #reachability #reasoning
Effectively-Propositional Reasoning about Reachability in Linked Data Structures (SI, AB, NI, AN, MS), pp. 756–772.
CAV-2013-PiskacWZ #automation #logic #smt #using
Automating Separation Logic Using SMT (RP, TW, DZ), pp. 773–789.
CAV-2013-HaaseIOP #graph #logic #named #reasoning
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic (CH, SI, JO, MJP), pp. 790–795.
CAV-2013-HarrisJLJ #library #validation
Validating Library Usage Interactively (WRH, GJ, SL, SJ), pp. 796–812.
CAV-2013-0001LMN #data type #invariant #learning #linear #quantifier
Learning Universally Quantified Invariants of Linear Data Structures (PG, CL, PM, DN), pp. 813–829.
CAV-2013-ColangeBKT #diagrams #distributed #model checking #towards #using
Towards Distributed Software Model-Checking Using Decision Diagrams (MC, SB, FK, YTM), pp. 830–845.
CAV-2013-KomuravelliGCC #abstraction #automation #bound #model checking #smt
Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.
CAV-2013-BarnatBHHKLRSW #c #c++ #model checking #parallel #source code #thread
DiVinE 3.0 — An Explicit-State Model Checker for Multithreaded C & C++ Programs (JB, LB, VH, JH, JK, ML, PR, VS, JW), pp. 863–868.
CAV-2013-BeyenePR #horn clause #quantifier
Solving Existentially Quantified Horn Clauses (TAB, CP, AR), pp. 869–882.
CAV-2013-TsaiTH #automaton #game studies #logic
GOAL for Games, ω-Automata, and Logics (MHT, YKT, YSH), pp. 883–889.
CAV-2013-Brenguier #concurrent #game studies #named #nash
PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games (RB), pp. 890–895.
CAV-2013-EssenJ #program repair
Program Repair without Regret (CvE, BJ), pp. 896–911.
CAV-2013-WonischSW #proving #source code
Programs from Proofs — A PCC Alternative (DW, AS, HW), pp. 912–927.
CAV-2013-KhalimovJB #synthesis
PARTY Parameterized Synthesis of Token Rings (AK, SJ, RB), pp. 928–933.
CAV-2013-AlbarghouthiGK #recursion #synthesis
Recursive Program Synthesis (AA, SG, ZK), pp. 934–950.
CAV-2013-CernyHRRT #concurrent #performance #semantics #synthesis
Efficient Synthesis for Concurrency by Semantics-Preserving Transformations (PC, TAH, AR, LR, TT), pp. 951–967.
CAV-2013-LaarmanODLP #abstraction #automaton #manycore #using
Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction (AL, MCO, AED, KGL, JvdP), pp. 968–983.
CAV-2013-AndreLSDL #concurrent #named #parametricity #realtime #synthesis
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems (ÉA, YL, JS, JSD, SWL), pp. 984–989.
CAV-2013-HerbreteauSW #abstraction #automaton #lazy evaluation
Lazy Abstractions for Timed Automata (FH, BS, IW), pp. 990–1005.
CAV-2013-Sankur #analysis #automaton #named #robust
Shrinktech: A Tool for the Robustness Analysis of Timed Automata (OS), pp. 1006–1012.

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.