CAV 2013
72 papers
- A Fully Verified Executable LTL Model Checker
- A Scalable and Nearly Uniform Generator of SAT Witnesses
- A Tool for Estimating Information Leakage
- Abstraction Based Model-Checking of Stability of Hybrid Systems
- Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
- Automatic Abstraction in SMT-Based Unbounded Software Model Checking
- Automatic Generation of Quality Specifications
- Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
- Automating Separation Logic Using SMT
- Beautiful Interpolants
- Better Termination Proving through Cooperation
- CacBDD: A BDD Package with Dynamic Cache Management
- Combining Relational Learning with SMT Solvers Using CEGAR
- DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs
- Disjunctive Interpolants for Horn-Clause Verification
- Distributed Explicit State Model Checking of Deadlock Freedom
- Duet: Static Analysis for Unbounded Parallelism
- Effectively-Propositional Reasoning about Reachability in Linked Data Structures
- Efficient Generation of Small Interpolants in CNF
- Efficient Robust Monitoring for STL
- Efficient Synthesis for Concurrency by Semantics-Preserving Transformations
- Equivalence of Extended Symbolic Finite Transducers
- Explain: A Tool for Performing Abductive Inference
- Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking
- Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
- Faster Algorithms for Markov Decision Processes with Low Treewidth
- Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems
- Finite Model Finding in SMT
- First-Order Theorem Proving and Vampire
- Flow*: An Analyzer for Non-linear Hybrid Systems
- Formal Verification of Hardware Synthesis
- Fully Automated Shape Analysis Based on Forest Automata
- GOAL for Games, Omega-Automata, and Logics
- Generating Non-linear Interpolants by Semidefinite Programming
- ILP Modulo Theories
- Importance Splitting for Statistical Model Checking Rare Properties
- Incremental, Inductive Coverability
- JBernstein: A Validity Checker for Generalized Polynomial Constraints
- Lazy Abstractions for Timed Automata
- Learning Universally Quantified Invariants of Linear Data Structures
- Lengths May Break Privacy - Or How to Check for Equivalences with Length
- Minimal Sets over Monotone Predicates in Boolean Formulae
- Model-Checking Signal Transduction Networks through Decreasing Reachability Sets
- Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction
- Multi-solver Support in Symbolic Execution
- PARTY Parameterized Synthesis of Token Rings
- PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games
- PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems
- Parameterized Verification of Asynchronous Shared-Memory Systems
- Partial Orders for Efficient Bounded Model Checking of Concurrent Software
- Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
- Probabilistic Program Analysis with Martingales
- Program Repair without Regret
- Programs from Proofs - A PCC Alternative
- Proving Termination Starting from the End
- QUAIL: A Quantitative Security Analyzer for Imperative Code
- Recursive Program Synthesis
- Relative Equivalence in the Presence of Ambiguity
- SVA and PSL Local Variables - A Practical Approach
- SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
- Shrinktech: A Tool for the Robustness Analysis of Timed Automata
- Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries
- Software Model Checking for People Who Love Automata
- Solving Existentially Quantified Horn Clauses
- System Level Formal Verification via Model Checking Driven Simulation
- TTP: Tool for Tumor Progression
- The TAMARIN Prover for the Symbolic Analysis of Security Protocols
- Towards Distributed Software Model-Checking Using Decision Diagrams
- Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks
- Under-Approximating Loops in C Programs for Fast Counterexample Detection
- Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata
- Validating Library Usage Interactively