Hana Chockler, Georg Weissenbacher
Proceedings of the 30th International Conference on Computer Aided Verification, Part I
CAV (1), 2018.

@proceedings{CAV-p1-2018,
	doi           = "10.1007/978-3-319-96145-3",
	editor        = "Hana Chockler and Georg Weissenbacher",
	isbn          = "['978-3-319-96144-6', '978-3-319-96145-3']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 30th International Conference on Computer Aided Verification, Part I}",
	volume        = 10981,
	year          = 2018,
}

Contents (39 items)

CAV-2018-DreossiJS #learning #semantics

Semantic Adversarial Deep Learning (TD, SJ, SAS), pp. 3–26.

CAV-2018-Yahav #modelling #source code

From Programs to Interpretable Deep Models and Back (EY), pp. 27–37.

CAV-2018-Cook #reasoning #security #web #web service

Formal Reasoning About the Security of Amazon Web Services (BC), pp. 38–47.

CAV-2018-GrishchenkoMS #contract #static analysis #tool support

Foundations and Tools for the Static Analysis of Ethereum Smart Contracts (IG, MM, CS), pp. 51–78.

CAV-2018-KraglQ #concurrent #source code

Layered Concurrent Programs (BK, SQ), pp. 79–102.

CAV-2018-Satake0 #functional #higher-order #logic #source code

Propositional Dynamic Logic for Higher-Order Functional Programs (YS, HU0), pp. 105–123.

CAV-2018-FedyukovichZG #analysis #termination

Syntax-Guided Termination Analysis (GF, YZ, AG), pp. 124–143.

CAV-2018-FinkbeinerHT #model checking

Model Checking Quantitative Hyperproperties (BF, CH, HT), pp. 144–163.

CAV-2018-PickFG #relational #symmetry #verification

Exploiting Synchrony and Symmetry in Relational Verification (LP, GF, AG), pp. 164–182.

CAV-2018-CordeiroKKST #bound #bytecode #java #model checking #named #verification

JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (LCC, PK, DK, PS, MT), pp. 183–190.

CAV-2018-McMillan #abstraction #model checking

Eager Abstraction for Symbolic Model Checking (KLM), pp. 191–208.

CAV-2018-SinghPV #learning #performance #program analysis

Fast Numerical Program Analysis with Reinforcement Learning (GS, MP, MTV), pp. 211–229.

CAV-2018-BecchiZ #encoding

A Direct Encoding for NNC Polyhedra (AB, EZ), pp. 230–248.

CAV-2018-AkshayCGKS #functional #question #synthesis #what

What's Hard About Boolean Functional Synthesis? (SA, SC, SG, SK, SS), pp. 251–269.

CAV-2018-AbateDKKP #induction #modulo theories #synthesis

Counterexample Guided Inductive Synthesis Modulo Theories (AA, CD, PK, DK, EP), pp. 270–288.

CAV-2018-FinkbeinerHLST

Synthesizing Reactive Systems from Hyperproperties (BF, CH, PL, MS, LT), pp. 289–306.

CAV-2018-FremontS

Reactive Control Improvisation (DJF, SAS), pp. 307–326.

CAV-2018-AlbarghouthiH #constraints #proving #synthesis

Constraint-Based Synthesis of Coupling Proofs (AA, JH), pp. 327–346.

CAV-2018-FanMM0 #linear #specification #synthesis

Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics (CF, UM, SM, MV0), pp. 347–366.

CAV-2018-BansalNS #source code #specification #synthesis

Synthesis of Asynchronous Reactive Programs from Temporal Specifications (SB, KSN, YS), pp. 367–385.

CAV-2018-HuD #synthesis

Syntax-Guided Synthesis with Quantitative Syntactic Objectives (QH, LD), pp. 386–403.

CAV-2018-WangADM #abstraction #learning #synthesis

Learning Abstractions for Program Synthesis (XW0, GA, ID, KLM), pp. 407–426.

CAV-2018-ArgyrosD #automaton

The Learnability of Symbolic Automata (GA, LD), pp. 427–445.

CAV-2018-KongBH #approximate #set #using

Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes (HK, EB, TAH), pp. 449–467.

CAV-2018-FrehseGH

Space-Time Interpolants (GF, MG, TAH), pp. 468–486.

CAV-2018-EmmiE #consistency #monitoring

Monitoring Weak Consistency (ME, CE), pp. 487–506.

CAV-2018-FengKLXZ #automaton #monitoring #multi

Monitoring CTMCs by Multi-clock Timed Automata (YF, JPK, HL, BX, NZ), pp. 507–526.

CAV-2018-BonnelandJLMS #partial order #reduction

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (FMB, PGJ, KGL, MM, JS), pp. 527–546.

CAV-2018-BartocciBNR #finite #ltl #monitoring #semantics #specification

A Counting Semantics for Monitoring LTL Specifications over Finite Traces (EB, RB, DN, FR), pp. 547–564.

CAV-2018-KretinskyMSZ #automaton #ltl

Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (JK, TM, SS, CZ), pp. 567–577.

CAV-2018-MeyerSL #exclamation #named #synthesis

Strix: Explicit Reactive Synthesis Strikes Back! (PJM, SS, ML), pp. 578–586.

CAV-2018-NiemetzPWB

Btor2 , BtorMC and Boolector 3.0 (AN, MP, CW, AB), pp. 587–595.

CAV-2018-Eilers0 #named #python #verification

Nagini: A Static Verifier for Python (ME, PM0), pp. 596–603.

CAV-2018-BlondinEJ #analysis #named #protocol

Peregrine: A Tool for the Analysis of Population Protocols (MB, JE, SJ), pp. 604–611.

CAV-2018-CeskaMMSVV #approximate #automation #design #named

ADAC: Automated Design of Approximate Circuits (MC0, JM, VM, LS, ZV, TV), pp. 612–620.

CAV-2018-KelmendiKKW #algorithm #game studies #learning #probability

Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (EK, JK, JK, MW), pp. 623–642.

CAV-2018-QuatmannK

Sound Value Iteration (TQ, JPK), pp. 643–661.

CAV-2018-ZhouL #learning

Safety-Aware Apprenticeship Learning (WZ, WL), pp. 662–680.

CAV-2018-TangB #distance #markov #probability #similarity

Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (QT0, FvB), pp. 681–699.