CAV 2019: 31ST INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION
PROGRAM

Days: Sunday, July 14th Monday, July 15th Tuesday, July 16th Wednesday, July 17th Thursday, July 18th

Sunday, July 14th

View this program: with abstractssession overviewtalk overview

Monday, July 15th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 6: Automata and Timed Systems
10:30
Symbolic Register Automata (abstract)
10:50
Abstraction Refinement Algorithms for Timed Automata (abstract)
11:10
Fast algorithms for handling diagonal constraints in timed automata (abstract)
11:30
Safety and co-safety comparator automata for discounted-sum inclusion (abstract)
11:50
Clock Bound Repair for Timed Systems (abstract)
12:10
Automated Hypersafety Verification (abstract)
12:40-14:30Lunch Break
14:30-16:30 Session 8: Security and Hyperproperties
14:30
Verifying Hyperliveness (abstract)
14:50
Quantitative Mitigation of Timing Side Channels (abstract)
15:10
Property Directed Self Composition (abstract)
15:30
Security-Aware Synthesis Using Delayed-Action Games (abstract)
15:50
Automated Synthesis of Secure Platform Mappings (abstract)
16:30-17:00Coffee Break
Tuesday, July 16th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 11: Synthesis
10:30
Synthesizing Approximate Implementations for Unrealizable Specifications (abstract)
10:50
Quantified Invariants via Syntax-Guided-Synthesis (abstract)
11:10
Efficient Synthesis with Probabilistic Constraints (abstract)
11:30
Membership-based Synthesis of Linear Hybrid Automata (abstract)
11:50
Overfitting in Synthesis: Theory and Practice (abstract)
12:10
Proving Unrealizability for Syntax-Guided Synthesis (abstract)
12:30-13:00Lunch Break (catered)
14:30-15:10 Session 12: Model checking
14:30
BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings (abstract)
14:40
When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol (abstract)
14:50
Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (abstract)
15:00
Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C (abstract)
15:10-16:00 Session 13: Cyber-physical systems and machine learning
15:10
Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification (abstract)
15:30
StreamLAB: Stream-based Monitoring of Cyber-Physical Systems (abstract)
15:40
Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems (abstract)
15:50
The Marabou Framework for Verification and Analysis of Deep Neural Networks (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 14: Probabilistic systems, runtime techniques
16:30
Probabilistic Bisimulation for Parameterized Systems (abstract)
16:50
Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks (abstract)
17:10
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games (abstract)
17:30
Symbolic Monitoring against Specifications Parametric in Time and Data (abstract)
17:50
STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis (abstract)
Wednesday, July 17th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 16: Dynamical, Hybrid, and Reactive Systems
10:30
Local and Compositional Reasoning For Optimized Reactive Systems (abstract)
10:50
Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach (abstract)
11:10
Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis (abstract)
11:30
Temporal Stream Logic: Synthesis beyond the Bools (abstract)
11:50
Run-Time Optimization for Learned Controllers through Quantitative Games (abstract)
12:10
Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations (abstract)
12:30-14:30Lunch Break
14:30-16:00 Session 17: Logics, decision procedures, and solvers
14:30
Satisfiability Checking for Mission-Time LTL (abstract)
14:50
High-Level Abstractions for Simplifying Extended String Constraints in SMT (abstract)
15:10
Alternating Automata Modulo First Order Theories (abstract)
15:30
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (abstract)
15:40
CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (abstract)
15:50
Incremental Determinization for Quantifier Elimination and Functional Synthesis (abstract)
16:00-16:30Decision Procedures Coffee Break
16:30-18:00 Session 18: Numerical programs
16:30
Loop Summarization with Rational Vector Addition Systems (abstract)
16:50
Invertibility Conditions for Floating-Point Formulas (abstract)
17:10
Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (abstract)
17:30
Icing: Supporting Fast-math Style Optimizations in a Verified Compiler (abstract)
17:50
Sound Approximation of Programs with Elementary Functions (abstract)
Thursday, July 18th

View this program: with abstractssession overviewtalk overview

09:50-10:20Coffee Break
10:30-12:30 Session 21: Distributed Systems and Networks
Chair:
10:30
Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics (abstract)
10:50
Gradual Consistency Checking (abstract)
11:10
Checking Robustness Against Snapshot Isolation (abstract)
11:30
Efficient verification of network fault tolerance via counterexample-guided refinement (abstract)
11:50
On the Complexity of Checking Consistency for Replicated Data Types (abstract)
12:10
Communication-closed asynchronous protocols (abstract)
12:30-14:30Lunch Break
14:30-16:00 Session 22: Verification and Invariants
14:30
Interpolating Strong Induction (abstract)
14:50
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (abstract)
15:10
Inferring Inductive Invariants from Phase Structures (abstract)
15:30
Termination of Triangular Integer Loops is Decidable (abstract)
15:50
AliveInLean: A Verified LLVM Peephole Optimization Verifier (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 23: Concurrency
16:30
Automated Parameterized Verification of CRDTs (abstract)
16:50
What's wrong with on-the-fly partial order reduction (abstract)
17:10
Integrating Formal Schedulability Analysis into a Verifed OS Kernel (abstract)
17:30
Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS (abstract)
17:50
Violat: Generating Tests of Observational Refinement for Concurrent Objects (abstract)