Computer Aided Verification, CAV 2017


Title/Authors Title Research Artifacts
[?] A research artifact is any by-product of a research project that is not directly included in the published research paper. In Computer Science research this is often source code and data sets, but it could also be media, documentation, inputs to proof assistants, shell-scripts to run experiments, etc.
Details

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

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

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Simulation-Equivalent Reachability of Large Linear Systems with Inputs

Stanley Bak, Parasara Sridhar Duggirala

Simulation-Equivalent Reachability of Large Linear Systems with Inputs

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Classification and Coverage-Based Falsification for Embedded Control Systems

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

Classification and Coverage-Based Falsification for Embedded Control Systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Synthesis with Abstract Examples

Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav

Synthesis with Abstract Examples

Details
Discussion Comments: 0
Verification: Authors have not verified information

The Power of Symbolic Automata and Transducers

Loris D'Antoni, Margus Veanes

The Power of Symbolic Automata and Transducers

Details
Discussion Comments: 0
Verification: Authors have not verified information

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds

Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Lagrangian Reachabililty

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

Lagrangian Reachabililty

Details
Discussion Comments: 0
Verification: Authors have not verified information

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

Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer

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

Details
Discussion Comments: 0
Verification: Authors have not verified information

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

Runtime Monitoring with Recovery of the SENT Communication Protocol

Details
Discussion Comments: 0
Verification: Authors have not verified information

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

David A. Basin, Felix Klaedtke, Eugen Zalinescu

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

Details
Discussion Comments: 0
Verification: Authors have not verified information

Safety Verification of Deep Neural Networks

Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu

Safety Verification of Deep Neural Networks

Details
Discussion Comments: 0
Verification: Authors have not verified information

Context-Sensitive Dynamic Partial Order Reduction

Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Peter J. Stuckey

Context-Sensitive Dynamic Partial Order Reduction

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

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

Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan

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

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments: DryVR is an open source tool for verification of hybrid systems with black-box components
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

MightyL: A Compositional Translation from MITL to Timed Automata

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

MightyL: A Compositional Translation from MITL to Timed Automata

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Repairing Decision-Making Programs Under Uncertainty

Aws Albarghouthi, Loris D'Antoni, Samuel Drews

Repairing Decision-Making Programs Under Uncertainty

Details
Discussion Comments: 0
Verification: Authors have not verified information

Markov Automata with Multiple Objectives

Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen

Markov Automata with Multiple Objectives

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Logical Clustering and Learning for Time-Series Data

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

Logical Clustering and Learning for Time-Series Data

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Program Verification Under Weak Memory Consistency Using Separation Logic

Viktor Vafeiadis

Program Verification Under Weak Memory Consistency Using Separation Logic

Details
Discussion Comments: 0
Verification: Author has not verified information

GPUDrano: Detecting Uncoalesced Accesses in GPU Programs

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

GPUDrano: Detecting Uncoalesced Accesses in GPU Programs

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Data-Driven Synthesis of Full Probabilistic Programs

Sarah Chasins, Phitchaya Mangpo Phothilimthana

Data-Driven Synthesis of Full Probabilistic Programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Montre: A Tool for Monitoring Timed Regular Expressions

Dogan Ulus

Montre: A Tool for Monitoring Timed Regular Expressions

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Author has not verified information

STLInspector: STL Validation with Guarantees

Hendrik Roehm, Thomas Heinz, Eva Charlotte Mayer

STLInspector: STL Validation with Guarantees

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

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

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

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

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Maximum Satisfiability in Software Analysis: Applications and Techniques

Xujie Si, Xin Zhang, Radu Grigore, Mayur Naik

Maximum Satisfiability in Software Analysis: Applications and Techniques

Details
Discussion Comments: 0
Verification: Authors have not verified information

Starling: Lightweight Concurrency Verification with Views

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

Starling: Lightweight Concurrency Verification with Views

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

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

Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek

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

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

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

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

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

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Learning a Static Analyzer from Data

Pavol Bielik, Veselin Raychev, Martin T. Vechev

Learning a Static Analyzer from Data

Details
Discussion Comments: 0
Verification: Authors have not verified information

Compositional Model Checking with Incremental Counter-Example Construction

Anton Wijs, Thomas Neele

Compositional Model Checking with Incremental Counter-Example Construction

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

Luca Cardelli, Milan Ceska, Martin Fränzle, Marta Z. Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

Details
Discussion Comments: 0
Verification: Authors have not verified information

Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems

Marie Fortin, Anca Muscholl, Igor Walukiewicz

Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Details
Discussion Comments: 0
Verification: Authors have not verified information

Model Counting for Recursively-Defined Strings

Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar

Model Counting for Recursively-Defined Strings

Details
Discussion Comments: 0
Verification: Authors have not verified information

On Multiphase-Linear Ranking Functions

Amir M. Ben-Amram, Samir Genaim

On Multiphase-Linear Ranking Functions

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Automating Induction for Solving Horn Clauses

Hiroshi Unno, Sho Torii, Hiroki Sakamoto

Automating Induction for Solving Horn Clauses

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Cutoff Bounds for Consensus Algorithms

Ognjen Maric, Christoph Sprenger, David A. Basin

Cutoff Bounds for Consensus Algorithms

Details
Discussion Comments: 0
Verification: Authors have not verified information

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT

Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Verifying Equivalence of Spark Programs

Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv

Verifying Equivalence of Spark Programs

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Quantitative Assume Guarantee Synthesis

Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner

Quantitative Assume Guarantee Synthesis

Details
Discussion Comments: 0
Verification: Authors have not verified information

BoSy: An Experimentation Framework for Bounded Synthesis

Peter Faymonville, Bernd Finkbeiner, Leander Tentrup

BoSy: An Experimentation Framework for Bounded Synthesis

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Efficient Parallel Strategy Improvement for Parity Games

John Fearnley

Efficient Parallel Strategy Improvement for Parity Games

Details
Discussion Comments: 0
Verification: Author has not verified information

Non-polynomial Worst-Case Analysis of Recursive Programs

Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady

Non-polynomial Worst-Case Analysis of Recursive Programs

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Towards Verifying Nonlinear Integer Arithmetic

Paul Beame, Vincent Liew

Towards Verifying Nonlinear Integer Arithmetic

Details
Discussion Comments: 0
Verification: Authors have not verified information

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification

Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger

EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Synchronization Synthesis for Network Programs

Jedidiah McClurg, Hossein Hojjat, Pavol Cerný

Synchronization Synthesis for Network Programs

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis

Adrià Gascón, Ashish Tiwari, Brent Carmer, Umang Mathur

Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Verified Compilation of Space-Efficient Reversible Circuits

Matthew Amy, Martin Roetteler, Krysta M. Svore

Verified Compilation of Space-Efficient Reversible Circuits

Details
Discussion Comments: 0
Verification: Authors have not verified information

Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts

Andrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin T. Vechev

Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts

Details
Discussion Comments: 0
Verification: Authors have not verified information

Ascertaining Uncertainty for Efficient Exact Cache Analysis

Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke

Ascertaining Uncertainty for Efficient Exact Cache Analysis

Details
Discussion Comments: 0
Verification: Authors have not verified information

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Minimization of Symbolic Transducers

Olli Saarikivi, Margus Veanes

Minimization of Symbolic Transducers

Details
Discussion Comments: 0
Verification: Authors have not verified information

A Storm is Coming: A Modern Probabilistic Model Checker

Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk

A Storm is Coming: A Modern Probabilistic Model Checker

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods

Eshan Singh, Clark W. Barrett, Subhasish Mitra

E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

A Correct-by-Decision Solution for Simultaneous Place and Route

Alexander Nadel

A Correct-by-Decision Solution for Simultaneous Place and Route

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Author has verified information

Proving Linearizability Using Forward Simulations

Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil

Proving Linearizability Using Forward Simulations

Details
Discussion Comments: 0
Verification: Authors have not verified information

Abstract Interpretation with Unfoldings

Marcelo Sousa, César Rodríguez, Vijay D'Silva, Daniel Kroening

Abstract Interpretation with Unfoldings

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Automated Resource Analysis with Coq Proof Objects

Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao

Automated Resource Analysis with Coq Proof Objects

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Not able to share produced artifacts
Verification: Authors have verified information

Bounded Synthesis for Streett, Rabin, and \text CTL^*

Ayrat Khalimov, Roderick Bloem

Bounded Synthesis for Streett, Rabin, and \text CTL^*

Details
Discussion Comments: 0
Verification: Authors have not verified information

On Expansion and Resolution in CEGAR Based QBF Solving

Leander Tentrup

On Expansion and Resolution in CEGAR Based QBF Solving

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Author has not verified information

Network-Wide Configuration Synthesis

Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin T. Vechev

Network-Wide Configuration Synthesis

Details
Discussion Comments: 0
Verification: Authors have not verified information