Accepted papers

Montre: A Tool for Monitoring Timed Regular ExpressionsDogan Ulus
Automated Recurrence Analysis for Almost-Linear Expected-Runtime BoundsKrishnendu ChatterjeeHongfei FuAniket Murhekar
A Storm is Coming: A Modern Probabilistic Model CheckerChristian DehnertSebastian JungesJoost-Pieter KatoenMatthias Volk
On Multiphase-Linear Ranking FunctionsAmir M. Ben-AmramSamir Genaim
Runtime Monitoring with Recovery of the SENT Communication ProtocolKonstantin SelyuninStefan JaksicThang NguyenChristian ReidlUdo HafnerEzio BartocciDejan NickovicRadu Grosu
BoSy: An experimentation framework for Bounded SynthesisPeter FaymonvilleBernd FinkbeinerLeander Tentrup
Non-polynomial Worst-case Analysis of Recursive ProgramsKrishnendu ChatterjeeHongfei FuAmir Kafshdar Goharshady
Proving linearizability using forward simulationsAhmed BouajjaniMichael EmmiConstantin EneaSuha Orhun Mutluergil
A Correct-by-Decision Solution for Simultaneous Place and RouteAlexander Nadel
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical SystemsNikola BenešLuboš BrimMartin DemkoSamuel PastvaDavid Šafránek
MightyL: A Compositional Translation from MITL to Timed AutomataThomas BrihayeGilles GeeraertsHsi-Ming HoBenjamin Monmege
Markov Automata with Multiple ObjectivesTim QuatmannSebastian JungesJoost-Pieter Katoen
Quantitative Assume Guarantee SynthesisShaull AlmagorOrna KupfermanJan Oliver RingertYaron Velner
Automated Resource Analysis with Coq Proof ObjectsQuentin CarbonneauxJan HoffmannThomas RepsZhong Shao
Towards Verifying Nonlinear Integer ArithmeticVincent LiewPaul Beame
A Decidable Fragment in Separation Logic with Inductive Predicates and ArithmeticQuang Loc LeTatsuta MakotoJun SunWei-Ngan Chin
Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systemsMarie FortinAnca MuschollIgor Walukiewicz
Context-Sensitive Dynamic Partial Order ReductionElvira AlbertPuri ArenasMaria Garcia de la BandaMiguel Gomez-ZamalloaPeter Stuckey
Cutoff Bounds for Consensus AlgorithmsOgnjen MaricChristoph SprengerDavid Basin
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision ProcessesChristel BaierJoachim KleinLinda LeuschnerDavid ParkerSascha Wunderlich
Efficient Parallel Strategy Improvement for Parity GamesJohn Fearnley
Syntax-Guided Optimal Synthesis for Chemical Reaction NetworksLuca CardelliMilan CeskaMartin FranzleMarta KwiatkowskaLuca LaurentiNicola PaolettiMax Whitby
Verified compilation of space-efficient reversible circuitsMatthew AmyMartin RoettelerKrysta Svore
Lightweight Concurrency Verification With ViewsMatthew WindsorMike DoddsMatthew J ParkinsonBen Simner
Synchronization Synthesis for Network ProgramsJedidiah McClurgHossein HojjatPavol Cerny
SMTCoq: A plug-in for integrating SMT solvers into CoqBurak EkiciAlain MebsoutCesare TinelliChantal KellerGuy KatzAndrew ReynoldsClark Barrett
STLInspector: STL Validation with GuaranteesHendrik RöhmThomas HeinzEva Charlotte Mayer
Lagrangian ReachabililtyJacek CyrankaMd Ariful IslamGreg ByrnePaul L. JonesScott A. SmolkaRadu Grosu
DryVR: Data-driven verification and compositional reasoning for automotive systemsChuchu FanBolun QiSayan MitraMahesh Viswanathan
GPUDrano: Detecting Uncoalesced Accesses in GPU ProgramsRajeev AlurJoseph DeviettiOmar Navarro LeijaNimit Singhania
Ascertaining Uncertainty for Efficient Exact Cache AnalysisClaire MaizaDavid MonniauxJan ReinekeValentin Touzeau
Simulation-Equivalent Reachability of Large Linear Systems with InputsStanley BakParasara Sridhar Duggirala
Classification and coverage-based falsification for embedded control systemsArvind S AdimoolamThao DangAlexandre DonzeJames KapinskiXiaoqing Jin
Repairing Decision-Making Programs under UncertaintyAws AlbarghouthiLoris D’AntoniSamuel Drews
Reluplex: An Efficient SMT Solver for Verifying Deep Neural NetworksGuy KatzClark BarrettDavid DillKyle JulianMykel Kochenderfer
EAHyper: Satisfiability, Implication, and Equivalence Checking of HyperpropertiesBernd FinkbeinerChristopher HahnMarvin Stenger
Compositional Model Checking with Incremental Counter-Example ConstructionAnton WijsThomas Neele
Scaling Up DPLL(T) String Solvers using Context-Dependent RewritingAndrew ReynoldsMaverick WooClark BarrettDavid BrumleyTianyi LiangCesare Tinelli
Look for the Proof to Find the Program: Decorated-Component-Based Program SynthesisAdria GasconAshish TiwariBrent CarmerUmang Mathur
Logic-based Clustering and Learning for Time-Series DataMarcell Vazquez-ChanlatteJyotirmoy DeshmukhXiaoqing JinSanjit A. Seshia
Abstract Interpretation with UnfoldingsMarcelo SousaCésar RodríguezVijay D’SilvaDaniel Kroening
On Expansion and Resolution in CEGAR based QBF solvingLeander Tentrup
Data-Driven Synthesis of Full Probabilistic ProgramsSarah ChasinsPhitchaya Mangpo Phothilimthana
Automating Induction for Solving Horn ClausesHiroshi UnnoSho ToriiHiroki Sakamoto
Runtime Verification of Temporal Properties over Out-of-order Data StreamsDavid BasinFelix KlaedtkeEugen Zalinescu
Verifying Equivalence of Spark ProgramsShelly GrossmanSara CohenShachar ItzhakyNoam RinetzkyMooly Sagiv
A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMTSylvain ConchonMohamed IguernlalaKailiang JiGuillaume MelquiondClément Fumex
Minimization of Symbolic TransducersOlli SaarikiviMargus Veanes
Value Iteration for Long-run Average Reward in Markov Decision ProcessesPranav AshokKrishnendu ChatterjeePrzemyslaw DacaJan KřetínskýTobias Meggendorfer
Finding Fix Locations for CFL-Reachability Analyses via Minimum CutsAndrei Marian DanManu SridharanSatish ChandraJean-Baptiste JeanninMartin Vechev
Automated Formal Synthesis of Digital Controllers for State-Space Physical PlantsAlessandro AbateIury BessaDario CattaruzzaLucas CordeiroCristina DavidPascal KesseliDaniel KroeningElizabeth Polgreen
Network-wide Configuration SynthesisAhmed El-HassanyPetar TsankovLaurent VanbeverMartin Vechev
Electrical Bug Localization During Post-Silicon Validation Enabled by Formal MethodsEshan SinghClark BarrettSubhasish Mitra
Model Counting for Recursively-Defined StringsMinh-Thai TrinhDuc-Hiep ChuJoxan Jaffar
Learning a Static Analyzer from DataPavol BielikVeselin RaychevMartin Vechev
Synthesis with Abstract ExamplesDana Drachsler CohenSharon ShohamEran Yahav
Bounded Synthesis for Streett, Rabin, and CTL*Ayrat KhalimovRoderick Bloem