Daniel Kröning, Corina S. Pasareanu
Proceedings of the 27th International Conference on Computer Aided Verification, Part II
CAV, 2015.

@proceedings{CAV-p2-2015,
	address       = "San Francisco, California, USA",
	doi           = "10.1007/978-3-319-21668-3",
	editor        = "Daniel Kröning and Corina S. Pasareanu",
	isbn          = "978-3-319-21667-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 27th International Conference on Computer Aided Verification, Part II}",
	volume        = 9207,
	year          = 2015,
}

Event page: http://i-cav.org/2015/

Contents (26 items)

4 ×#automation
4 ×#synthesis
4 ×#using
3 ×#smt
3 ×#verification
2 ×#abstraction
2 ×#composition
2 ×#deduction
2 ×#distributed
2 ×#multi

CAV-2015-ZhuPJ #named #proving #smt

Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.

CAV-2015-ErezN #automation #bound #graph #smt #using

Finding Bounded Path in Graph Using SMT for Automatic Clock Routing (AE, AN), pp. 20–36.

CAV-2015-ChristH

Cutting the Mix (JC, JH), pp. 37–52.

CAV-2015-ManoliosPP #framework #modulo theories #programming

The Inez Mathematical Programming Modulo Theories Framework (PM, JP, VP), pp. 53–69.

CAV-2015-BacchusK #satisfiability #set #using

Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets (FB, GK), pp. 70–86.

CAV-2015-BansalR0BW

Deciding Local Theory Extensions via E-matching (KB, AR, TK, CWB, TW), pp. 87–105.

CAV-2015-VijayaraghavanC #composition #deduction #design #hardware #multi #verification

Modular Deductive Verification of Multiprocessor Hardware Designs (MV, AC, A, ND), pp. 109–127.

CAV-2015-ChakrabortyKSGH #evaluation

Word-Level Symbolic Trajectory Evaluation (SC, ZK, CJHS, RG, TH, DC, RM), pp. 128–143.

CAV-2015-Leslie-HurdCF #verification

Verifying Linearizability of Intel® Software Guard Extensions (RLH, DC, MF), pp. 144–160.

CAV-2015-AlurCR #synthesis #unification

Synthesis Through Unification (RA, PC, AR), pp. 163–179.

CAV-2015-CernyCHRRST #scheduling #synthesis #using

From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis (PC, EMC, TAH, AR, LR, RS, TT), pp. 180–197.

CAV-2015-ReynoldsDKTB #quantifier #smt #synthesis

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.

CAV-2015-KneussKK #deduction #program repair

Deductive Program Repair (EK, MK, VK), pp. 217–233.

CAV-2015-DeshmukhMP #consistency #metric #using

Quantifying Conformance Using the Skorokhod Metric (JVD, RM, VSP), pp. 234–250.

CAV-2015-BrenguierR #game studies #multi

Pareto Curves of Multidimensional Mean-Payoff Games (RB, JFR), pp. 251–267.

CAV-2015-DSilvaU #termination

Conflict-Driven Conditional Termination (VD, CU), pp. 271–286.

CAV-2015-KuwaharaSU0 #abstraction #functional #higher-order #source code #termination

Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs (TK, RS, HU, NK), pp. 287–303.

CAV-2015-Ben-AmramG #complexity #ranking

Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions (AMBA, SG), pp. 304–321.

CAV-2015-FerrereMNU

Measuring with Timed Patterns (TF, OM, DN, DU), pp. 322–337.

CAV-2015-ZouFZM #automation #difference #equation #safety #verification

Automatic Verification of Stability and Safety for Delay Differential Equations (LZ, MF, NZ, PNM), pp. 338–355.

CAV-2015-AkazakiH #hybrid #robust

Time Robustness in MTL and Expressivity in Hybrid System Falsification (TA, IH), pp. 356–374.

CAV-2015-JeonQSF #adaptation #parallel #synthesis

Adaptive Concretization for Parallel Program Synthesis (JJ, XQ, ASL, JSF), pp. 377–394.

CAV-2015-AlurRSTU #automation #distributed #protocol #symmetry

Automatic Completion of Distributed Protocols with Symmetry (RA, MR, CS, ST, AU), pp. 395–412.

CAV-2015-ManskyGZ #axiom #memory management #modelling #specification

An Axiomatic Specification for Sequential Memory Models (WM, DG, SZ), pp. 413–428.

CAV-2015-DesaiSQBE #abstraction #approximate #distributed

Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems (AD, SAS, SQ, DB, JCE), pp. 429–448.

CAV-2015-HawblitzelPQT #automation #composition #concurrent #reasoning #refinement #source code

Automated and Modular Refinement Reasoning for Concurrent Programs (CH, EP, SQ, ST), pp. 449–465.