CAV 2019
67 papers
- Abstraction Refinement Algorithms for Timed Automata
- AliveInLean: A Verified LLVM Peephole Optimization Verifier
- Alternating Automata Modulo First Order Theories
- Automated Hypersafety Verification
- Automated Parameterized Verification of CRDTs
- Automated Synthesis of Secure Platform Mappings
- BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
- Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
- Checking Robustness Against Snapshot Isolation
- Clock Bound Repair for Timed Systems
- Communication-Closed Asynchronous Protocols
- Efficient Synthesis with Probabilistic Constraints
- Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement
- Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
- Fast Algorithms for Handling Diagonal Constraints in Timed Automata
- Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis
- Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
- Gradual Consistency Checking
- High-Level Abstractions for Simplifying Extended String Constraints in SMT
- Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler
- Incremental Determinization for Quantifier Elimination and Functional Synthesis
- Inferring Inductive Invariants from Phase Structures
- Integrating Formal Schedulability Analysis into a Verified OS Kernel
- Interpolating Strong Induction
- Invertibility Conditions for Floating-Point Formulas
- Local and Compositional Reasoning for Optimized Reactive Systems
- Loop Summarization with Rational Vector Addition Systems
- Membership-Based Synthesis of Linear Hybrid Automata
- Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification
- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
- On the Complexity of Checking Consistency for Replicated Data Types
- Overfitting in Synthesis: Theory and Practice
- PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
- Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols)
- Property Directed Self Composition
- Proving Unrealizability for Syntax-Guided Synthesis
- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
- Quantified Invariants via Syntax-Guided Synthesis
- Quantitative Mitigation of Timing Side Channels
- Reachability Analysis for AWS-Based Networks
- Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS
- Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
- Run-Time Optimization for Learned Controllers Through Quantitative Games
- STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis
- Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion
- Satisfiability Checking for Mission-Time LTL
- SecCSL: Security Concurrent Separation Logic
- Security-Aware Synthesis Using Delayed-Action Games
- Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks
- Sound Approximation of Programs with Elementary Functions
- StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
- Symbolic Monitoring Against Specifications Parametric in Time and Data
- Symbolic Register Automata
- Synthesizing Approximate Implementations for Unrealizable Specifications
- Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations
- Temporal Stream Logic: Synthesis Beyond the Bools
- Termination of Triangular Integer Loops is Decidable
- The Marabou Framework for Verification and Analysis of Deep Neural Networks
- VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
- Verifying Asynchronous Interactions via Communicating Session Automata
- Verifying Hyperliveness
- Violat: Generating Tests of Observational Refinement for Concurrent Objects
- What's Wrong with On-the-Fly Partial Order Reduction
- When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-agent Protocol
- cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis