The conference proceedings are available:
Computer Aided Verification29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I
Computer Aided Verification29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II
Montre: A Tool for Monitoring Timed Regular Expressions
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds
A Storm is Coming: A Modern Probabilistic Model Checker
On Multiphase-Linear Ranking Functions
Runtime Monitoring with Recovery of the SENT Communication Protocol
BoSy: An experimentation framework for Bounded Synthesis
Non-polynomial Worst-case Analysis of Recursive Programs
Proving linearizability using forward simulations
A Correct-by-Decision Solution for Simultaneous Place and Route
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems
MightyL: A Compositional Translation from MITL to Timed Automata
Markov Automata with Multiple Objectives
Quantitative Assume Guarantee Synthesis
Automated Resource Analysis with Coq Proof Objects
Towards Verifying Nonlinear Integer Arithmetic
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
Context-Sensitive Dynamic Partial Order Reduction
Cutoff Bounds for Consensus Algorithms
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes
Efficient Parallel Strategy Improvement for Parity Games
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks
Verified compilation of space-efficient reversible circuits
Lightweight Concurrency Verification With Views
Synchronization Synthesis for Network Programs
SMTCoq: A plug-in for integrating SMT solvers into Coq
STLInspector: STL Validation with Guarantees
Lagrangian Reachabililty
DryVR: Data-driven verification and compositional reasoning for automotive systems
GPUDrano: Detecting Uncoalesced Accesses in GPU Programs
Ascertaining Uncertainty for Efficient Exact Cache Analysis
Simulation-Equivalent Reachability of Large Linear Systems with Inputs
Classification and coverage-based falsification for embedded control systems
Repairing Decision-Making Programs under Uncertainty
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties
Compositional Model Checking with Incremental Counter-Example Construction
Scaling Up DPLL(T) String Solvers using Context-Dependent Rewriting
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
Logic-based Clustering and Learning for Time-Series Data
Abstract Interpretation with Unfoldings
On Expansion and Resolution in CEGAR based QBF solving
Data-Driven Synthesis of Full Probabilistic Programs
Automating Induction for Solving Horn Clauses
Runtime Verification of Temporal Properties over Out-of-order Data Streams
Verifying Equivalence of Spark Programs
A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT
Minimization of Symbolic Transducers
Value Iteration for Long-run Average Reward in Markov Decision Processes
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants
Network-wide Configuration Synthesis
Electrical Bug Localization During Post-Silicon Validation Enabled by Formal Methods
Model Counting for Recursively-Defined Strings
Learning a Static Analyzer from Data
Synthesis with Abstract Examples
Bounded Synthesis for Streett, Rabin, and CTL*