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

@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)

14 ×#model checking
11 ×#named
9 ×#automaton
6 ×#automation
6 ×#concurrent
6 ×#performance
6 ×#proving
6 ×#synthesis
6 ×#using
6 ×#verification

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, EÁ, 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.