CAV 2017
61 papers
- A Correct-by-Decision Solution for Simultaneous Place and Route
- A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
- A Storm is Coming: A Modern Probabilistic Model Checker
- A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT
- Abstract Interpretation with Unfoldings
- Ascertaining Uncertainty for Efficient Exact Cache Analysis
- Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants
- Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds
- Automated Resource Analysis with Coq Proof Objects
- Automating Induction for Solving Horn Clauses
- BoSy: An Experimentation Framework for Bounded Synthesis
- Bounded Synthesis for Streett, Rabin, and \text CTL^*
- Classification and Coverage-Based Falsification for Embedded Control Systems
- Compositional Model Checking with Incremental Counter-Example Construction
- Context-Sensitive Dynamic Partial Order Reduction
- Cutoff Bounds for Consensus Algorithms
- Data-Driven Synthesis of Full Probabilistic Programs
- DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems
- E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods
- EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties
- Efficient Parallel Strategy Improvement for Parity Games
- Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes
- Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
- GPUDrano: Detecting Uncoalesced Accesses in GPU Programs
- Lagrangian Reachabililty
- Learning a Static Analyzer from Data
- Logical Clustering and Learning for Time-Series Data
- Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
- Markov Automata with Multiple Objectives
- Maximum Satisfiability in Software Analysis: Applications and Techniques
- MightyL: A Compositional Translation from MITL to Timed Automata
- Minimization of Symbolic Transducers
- Model Counting for Recursively-Defined Strings
- Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems
- Montre: A Tool for Monitoring Timed Regular Expressions
- Network-Wide Configuration Synthesis
- Non-polynomial Worst-Case Analysis of Recursive Programs
- On Expansion and Resolution in CEGAR Based QBF Solving
- On Multiphase-Linear Ranking Functions
- Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems
- Program Verification Under Weak Memory Consistency Using Separation Logic
- Proving Linearizability Using Forward Simulations
- Quantitative Assume Guarantee Synthesis
- Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
- Repairing Decision-Making Programs Under Uncertainty
- Runtime Monitoring with Recovery of the SENT Communication Protocol
- Runtime Verification of Temporal Properties over Out-of-Order Data Streams
- SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
- STLInspector: STL Validation with Guarantees
- Safety Verification of Deep Neural Networks
- Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification
- Simulation-Equivalent Reachability of Large Linear Systems with Inputs
- Starling: Lightweight Concurrency Verification with Views
- Synchronization Synthesis for Network Programs
- Syntax-Guided Optimal Synthesis for Chemical Reaction Networks
- Synthesis with Abstract Examples
- The Power of Symbolic Automata and Transducers
- Towards Verifying Nonlinear Integer Arithmetic
- Value Iteration for Long-Run Average Reward in Markov Decision Processes
- Verified Compilation of Space-Efficient Reversible Circuits
- Verifying Equivalence of Spark Programs