Isil Dillig, Serdar Tasiran
Proceedings of the 30st International Conference on Computer Aided Verification, Part I
CAV (1), 2019.

@proceedings{CAV-p1-2019,
	doi           = "10.1007/978-3-030-25540-4",
	editor        = "Isil Dillig and Serdar Tasiran",
	isbn          = "['978-3-030-25539-8', '978-3-030-25540-4']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 30st International Conference on Computer Aided Verification, Part I}",
	volume        = 11561,
	year          = 2019,
}

Contents (37 items)

CAV-2019-DAntoniFS0 #automaton

Symbolic Register Automata (LD, TF, MS, AS0), pp. 3–21.

CAV-2019-RoussanalySM #abstraction #algorithm #automaton #refinement

Abstraction Refinement Algorithms for Timed Automata (VR, OS, NM), pp. 22–40.

CAV-2019-Gastin0S #algorithm #automaton #constraints #performance

Fast Algorithms for Handling Diagonal Constraints in Timed Automata (PG, SM0, BS), pp. 41–59.

CAV-2019-BansalV #automaton #safety

Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion (SB, MYV), pp. 60–78.

CAV-2019-KolblLW #bound

Clock Bound Repair for Timed Systems (MK, SL, TW), pp. 79–96.

CAV-2019-LangeY #automaton #communication #interactive #verification

Verifying Asynchronous Interactions via Communicating Session Automata (JL, NY), pp. 97–117.

CAV-2019-CoenenFST #verification

Verifying Hyperliveness (NC, BF, CS, LT), pp. 121–139.

CAV-2019-Tizpaz-NiariC0

Quantitative Mitigation of Timing Side Channels (STN, PC, AT0), pp. 140–160.

CAV-2019-ShemerGSV #composition

Property Directed Self Composition (RS, AG, SS, YV), pp. 161–179.

CAV-2019-ElfarWP #game studies #synthesis #using

Security-Aware Synthesis Using Delayed-Action Games (ME, YW0, MP), pp. 180–199.

CAV-2019-FarzanV #automation #verification

Automated Hypersafety Verification (AF, AV), pp. 200–218.

CAV-2019-KangLT #automation #framework #platform #synthesis

Automated Synthesis of Secure Platform Mappings (EK, SL, ST), pp. 219–237.

CAV-2019-DimitrovaFT #approximate #implementation #specification

Synthesizing Approximate Implementations for Unrealizable Specifications (RD, BF, HT), pp. 241–258.

CAV-2019-FedyukovichPMG #invariant #quantifier #synthesis

Quantified Invariants via Syntax-Guided Synthesis (GF, SP, KM, AG), pp. 259–277.

CAV-2019-DrewsAD #constraints #performance #probability #synthesis

Efficient Synthesis with Probabilistic Constraints (SD, AA, LD), pp. 278–296.

CAV-2019-SotoHSZ #automaton #hybrid #linear #synthesis

Membership-Based Synthesis of Linear Hybrid Automata (MGS, TAH, CS0, LZ), pp. 297–314.

CAV-2019-PadhiMN0 #synthesis #theory and practice

Overfitting in Synthesis: Theory and Practice (SP, TDM, AVN, RS0), pp. 315–334.

CAV-2019-HuBCDR #proving #synthesis

Proving Unrealizability for Syntax-Guided Synthesis (QH, JB, JC, LD, TWR), pp. 335–352.

CAV-2019-GavrilenkoLFHM #analysis #encoding #memory management #modelling #smt

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings (NG, HPdL, FF, KH, RM0), pp. 355–365.

CAV-2019-DavisHK #fault #formal method #multi #protocol #proving #using

When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-agent Protocol (JAD, LRH, DBK), pp. 366–375.

CAV-2019-CimattiGMRT

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (AC, AG, EM, MR, ST), pp. 376–386.

CAV-2019-LauGMPS #c #concurrent #named #semantics

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C (SL, VBFG, KM, JPP, PS), pp. 387–397.

CAV-2019-ZhangHA #hybrid #multi

Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification (ZZ, IH, PA), pp. 401–420.

CAV-2019-FaymonvilleFSSS #cyber-physical #monitoring #named

StreamLAB: Stream-based Monitoring of Cyber-Physical Systems (PF, BF, MS, MS, MS, LT, HT), pp. 421–431.

CAV-2019-DreossiFGKRVS #analysis #design #named #tool support

VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems (TD, DJF, SG, EK, HR, MVC, SAS), pp. 432–442.

CAV-2019-KatzHIJLLSTWZDK #analysis #framework #network #verification

The Marabou Framework for Verification and Analysis of Deep Neural Networks (GK, DAH, DI, KJ, CL, RL, PS, ST, HW0, AZ, DLD, MJK, CWB), pp. 443–452.

CAV-2019-HongLMR #bisimulation #probability #protocol #verification

Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols) (CDH, AWL, RM, PR), pp. 455–474.

CAV-2019-CeskaK #abstraction #analysis #network

Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (MC0, JK), pp. 475–496.

CAV-2019-AshokKW #game studies #markov #model checking #probability #process #statistics

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games (PA, JK, MW), pp. 497–519.

CAV-2019-WagaAH #monitoring #parametricity #specification

Symbolic Monitoring Against Specifications Parametric in Time and Data (MW, ÉA, IH), pp. 520–539.

CAV-2019-NeupaneMM00 #analysis #approximate #infinity #model checking #named #probability

STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis (TN, CJM, CM, HZ0, ZZ0), pp. 540–549.

CAV-2019-JainM #composition #reasoning

Local and Compositional Reasoning for Optimized Reactive Systems (MJ, PM), pp. 553–571.

CAV-2019-Busatto-GastonM #approach #automaton #robust #synthesis

Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach (DBG, BM, PAR, OS), pp. 572–590.

CAV-2019-KimAS #flexibility #pipes and filters #robust #synthesis

Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis (ESK, MA, SAS), pp. 591–608.

CAV-2019-Finkbeiner0PS #logic #synthesis

Temporal Stream Logic: Synthesis Beyond the Bools (BF, FK0, RP, MS), pp. 609–629.

CAV-2019-AvniBCHKP #game studies #optimisation #runtime

Run-Time Optimization for Learned Controllers Through Quantitative Games (GA, RB, KC, TAH, BK, SP), pp. 630–649.

CAV-2019-FengCZF0 #bound #difference #equation #verification

Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations (SF, MC, NZ, MF, BX0), pp. 650–669.