CAV 2016
58 papers
- A Decision Procedure for Sets, Binary Relations and Partial Functions
- A Practical Verification Framework for Preemptive OS Kernels
- A SAT-Based Counterexample Guided Method for Unbounded Synthesis
- A Simple Algorithm for Solving Qualitative Probabilistic Parity Games
- Array Folds Logic
- Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement
- Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
- Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution
- BDD-Based Boolean Functional Synthesis
- BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs
- BigraphER: Rewriting and Analysis Engine for Bigraphs
- Bounded Cycle Synthesis
- Combining Model Learning and Model Checking to Analyze TCP Implementations
- Compositional Synthesis of Reactive Controllers for Multi-agent Systems
- Counterexample Guided Abstraction Refinement for Stability Analysis
- Effectively Propositional Interpolants
- End-to-End Verification of Processors with ISA-Formal
- Fast, Flexible, and Minimal CTL Synthesis via SMT
- From Shape Analysis to Termination Analysis in Linear Time
- Hitting Families of Schedules for Asynchronous Programs
- Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
- Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers
- JayHorn: A Framework for Verifying Java programs
- Learning-Based Assume-Guarantee Regression Verification
- Limit-Deterministic Büchi Automata for Linear Temporal Logic
- Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
- Markov Chains and Unambiguous Büchi Automata
- Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
- PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
- PSI: Exact Symbolic Inference for Probabilistic Programs
- ParCoSS: Efficient Parallelized Compiled Symbolic Simulation
- Parsimonious, Simulation Based Verification of Linear Systems
- Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
- Probabilistic Automated Language Learning for Configuration Files
- Progressive Reasoning over Recursively-Defined Strings
- Property Directed Equivalence via Abstract Simulation
- Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances
- Qlose: Program Repair with Quantitative Objectives
- RV-Match: Practical Semantics-Based Program Analysis
- Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata
- Satisfiability Modulo Heap-Based Programs
- Slugs: Extensible GR(1) Synthesis
- Solving Parity Games via Priority Promotion
- Soufflé: On Synthesis of Program Analyzers
- Stateless Model Checking for POWER
- String Analysis via Automata Manipulation with Logic Circuit Representation
- Structural Synthesis for GXW Specifications
- Symbolic Optimal Reachability in Weighted Timed Automata
- Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits
- Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems
- Synthesizing Probabilistic Invariants via Doob's Decomposition
- Termination Analysis of Probabilistic Programs Through Positivstellensatz's
- The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach
- The Kind 2 Model Checker
- Trigger Selection Strategies to Stabilize Program Verifiers
- Under-Approximating Backward Reachable Sets by Polytopes
- Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses
- XSat: A Fast Floating-Point Satisfiability Solver