Skip to main content
main-content

About this book

The two-volume set LNCS 10426 and LNCS 10427 constitutes the refereed proceedings of the 29th International Conference on Computer Aided Verification, CAV 2017, held in Heidelberg, Germany, in July 2017.

The total of 50 full and 7 short papers presented together with 5 keynotes and tutorials in the proceedings was carefully reviewed and selected from 191 submissions.

The CAV conference series is dedicated to the advancement of the theory and practice of computer-aided formal analysis of hardware and software systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation.

Table of Contents

Frontmatter

Invited Contributions

Frontmatter

2017 | OriginalPaper | Chapter

Safety Verification of Deep Neural Networks

Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu

2017 | OriginalPaper | Chapter

Program Verification Under Weak Memory Consistency Using Separation Logic

Viktor Vafeiadis

2017 | OriginalPaper | Chapter

The Power of Symbolic Automata and Transducers

Loris D’Antoni, Margus Veanes

2017 | OriginalPaper | Chapter

Maximum Satisfiability in Software Analysis: Applications and Techniques

Xujie Si, Xin Zhang, Radu Grigore, Mayur Naik

Probabilistic Systems

Frontmatter

2017 | OriginalPaper | Chapter

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer

2017 | OriginalPaper | Chapter

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds

Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar

2017 | OriginalPaper | Chapter

Markov Automata with Multiple Objectives

Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen

2017 | OriginalPaper | Chapter

Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes

Christel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich

2017 | OriginalPaper | Chapter

Repairing Decision-Making Programs Under Uncertainty

Aws Albarghouthi, Loris D’Antoni, Samuel Drews

2017 | OriginalPaper | Chapter

Value Iteration for Long-Run Average Reward in Markov Decision Processes

Pranav Ashok, Krishnendu Chatterjee, Przemysław Daca, Jan Křetínský, Tobias Meggendorfer

Data Driven Techniques

Frontmatter

2017 | OriginalPaper | Chapter

STLInspector: STL Validation with Guarantees

Hendrik Roehm, Thomas Heinz, Eva Charlotte Mayer

2017 | OriginalPaper | Chapter

Learning a Static Analyzer from Data

Pavol Bielik, Veselin Raychev, Martin Vechev

2017 | OriginalPaper | Chapter

Synthesis with Abstract Examples

Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav

2017 | OriginalPaper | Chapter

Data-Driven Synthesis of Full Probabilistic Programs

Sarah Chasins, Phitchaya Mangpo Phothilimthana

2017 | OriginalPaper | Chapter

Logical Clustering and Learning for Time-Series Data

Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia

Runtime Verification

Frontmatter

2017 | OriginalPaper | Chapter

Montre: A Tool for Monitoring Timed Regular Expressions

Dogan Ulus

2017 | OriginalPaper | Chapter

Runtime Monitoring with Recovery of the SENT Communication Protocol

Konstantin Selyunin, Stefan Jaksic, Thang Nguyen, Christian Reidl, Udo Hafner, Ezio Bartocci, Dejan Nickovic, Radu Grosu

2017 | OriginalPaper | Chapter

Runtime Verification of Temporal Properties over Out-of-Order Data Streams

David Basin, Felix Klaedtke, Eugen Zălinescu

Cyber-Physical Systems

Frontmatter

2017 | OriginalPaper | Chapter

Lagrangian Reachabililty

Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul Jones, Scott A. Smolka, Radu Grosu

2017 | OriginalPaper | Chapter

Simulation-Equivalent Reachability of Large Linear Systems with Inputs

Stanley Bak, Parasara Sridhar Duggirala

2017 | OriginalPaper | Chapter

MightyL: A Compositional Translation from MITL to Timed Automata

Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege

2017 | OriginalPaper | Chapter

DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems

Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan

2017 | OriginalPaper | Chapter

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen

2017 | OriginalPaper | Chapter

Classification and Coverage-Based Falsification for Embedded Control Systems

Arvind Adimoolam, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin

Concurrency

Frontmatter

2017 | OriginalPaper | Chapter

GPUDrano: Detecting Uncoalesced Accesses in GPU Programs

Rajeev Alur, Joseph Devietti, Omar S. Navarro Leija, Nimit Singhania

2017 | OriginalPaper | Chapter

Context-Sensitive Dynamic Partial Order Reduction

Elvira Albert, Puri Arenas, María García de la Banda, Miguel Gómez-Zamalloa, Peter J. Stuckey

2017 | OriginalPaper | Chapter

Starling: Lightweight Concurrency Verification with Views

Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson

2017 | OriginalPaper | Chapter

Compositional Model Checking with Incremental Counter-Example Construction

Anton Wijs, Thomas Neele

2017 | OriginalPaper | Chapter

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems

Nikola Beneš, Luboš Brim, Martin Demko, Samuel Pastva, David Šafránek

Backmatter

Additional information

Premium Partner

Neuer Inhalt
image credits