Swarat Chaudhuri, Azadeh Farzan
Proceedings of the 28th International Conference on Computer Aided Verification, Part I
CAV (1), 2016.

@proceedings{CAV-p1-2016,
	doi           = "10.1007/978-3-319-41528-4",
	editor        = "Swarat Chaudhuri and Azadeh Farzan",
	isbn          = "978-3-319-41527-7",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 28th International Conference on Computer Aided Verification, Part I}",
	volume        = 9779,
	year          = 2016,
}

Contents (29 items)

CAV-2016-ChatterjeeFG #analysis #probability #source code #termination

Termination Analysis of Probabilistic Programs Through Positivstellensatz's (KC, HF0, AKG), pp. 3–22.

CAV-2016-BaierK0K0W #ambiguity #automaton #markov

Markov Chains and Unambiguous Büchi Automata (CB, SK, JK0, SK, DM0, JW0), pp. 23–42.

CAV-2016-BartheEFH #composition #invariant #probability

Synthesizing Probabilistic Invariants via Doob's Decomposition (GB, TE, LMFF, JH), pp. 43–61.

CAV-2016-GehrMV #named #probability #source code

PSI: Exact Symbolic Inference for Probabilistic Programs (TG, SM, MTV), pp. 62–83.

CAV-2016-NgoLJ #modelling #named #probability #runtime #verification

PSCV: A Runtime Verification Tool for Probabilistic SystemC Models (VCN, AL, VJ), pp. 84–91.

CAV-2016-ChengHR #specification #synthesis

Structural Synthesis for GXW Specifications (CHC, YH, HR), pp. 95–117.

CAV-2016-FinkbeinerK #bound #synthesis

Bounded Cycle Synthesis (BF, FK0), pp. 118–135.

CAV-2016-KlenzeBH #flexibility #performance #smt #synthesis

Fast, Flexible, and Minimal CTL Synthesis via SMT (TK, SB, AJH), pp. 136–156.

CAV-2016-BloemBJ #distributed #self #synthesis

Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems (RB, NBS, SJ), pp. 157–176.

CAV-2016-CristiaR #set

A Decision Procedure for Sets, Binary Relations and Partial Functions (MC, GR), pp. 179–198.

CAV-2016-NiemetzPB #modulo theories #precise #satisfiability

Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (AN, MP, AB), pp. 199–217.

CAV-2016-TrinhCJ #reasoning #recursion #string

Progressive Reasoning over Recursively-Defined Strings (MTT, DHC, JJ), pp. 218–240.

CAV-2016-WangTLYJ #analysis #automaton #logic #representation #string

String Analysis via Automata Manipulation with Logic Circuit Representation (HEW, TLT, CHL, FY, JHRJ), pp. 241–260.

CAV-2016-KafleGM #abstract interpretation #automaton #finite #horn clause #named #using #verification

Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata (BK, JPG, JFM), pp. 261–268.

CAV-2016-DanielCGTM #abstraction #infinity

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations (JD, AC, AG, ST, SM), pp. 271–291.

CAV-2016-DooleyS #proving

Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances (MD, FS), pp. 292–309.

CAV-2016-HeMW #verification

Learning-Based Assume-Guarantee Regression Verification (FH0, SM, BYW), pp. 310–328.

CAV-2016-ElkaderGPS #automation #composition #reasoning #refinement

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement (KAE, OG, CSP, SS), pp. 329–351.

CAV-2016-KahsaiRSS #framework #java #named #source code #verification

JayHorn: A Framework for Verifying Java programs (TK, PR, HS, MS), pp. 352–358.

CAV-2016-LeinoP #verification

Trigger Selection Strategies to Stabilize Program Verifiers (KRML, CPC), pp. 361–381.

CAV-2016-LeSC #satisfiability #source code

Satisfiability Modulo Heap-Based Programs (QLL, JS0, WNC), pp. 382–404.

CAV-2016-MuellerSS #automation #execution #symbolic computation #using #verification

Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution (PM, MS, AJS), pp. 405–425.

CAV-2016-ManevichDR #analysis #linear #termination

From Shape Analysis to Termination Analysis in Linear Time (RM, BD, NR), pp. 426–446.

CAV-2016-GuthHSR #named #program analysis #semantics

RV-Match: Practical Semantics-Based Program Analysis (DG, CH, MS, GR), pp. 447–453.

CAV-2016-XueSE #approximate #set

Under-Approximating Backward Reachable Sets by Polytopes (BX0, ZS, AE), pp. 457–476.

CAV-2016-Duggirala0 #linear #simulation #verification

Parsimonious, Simulation Based Verification of Linear Systems (PSD, MV0), pp. 477–494.

CAV-2016-PrabhakarS #abstraction #analysis #refinement

Counterexample Guided Abstraction Refinement for Stability Analysis (PP, MGS), pp. 495–512.

CAV-2016-BouyerCM #automaton #reachability

Symbolic Optimal Reachability in Weighted Timed Automata (PB, MC, NM), pp. 513–530.

CAV-2016-FanQM0D #analysis #automation #hybrid #modelling #reachability

Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2 (CF, BQ, SM, MV0, PSD), pp. 531–538.