SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
Abstract elided by the publisher.
2,069 papers · page 47 of 104
Validating Library Usage Interactively
Abstract elided by the publisher.
Software Model Checking for People Who Love Automata
Abstract elided by the publisher.
Lazy Abstractions for Timed Automata
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the gu…
Fully Automated Shape Analysis Based on Forest Automata
Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples of tree automata. In order to allow for representing complex heap graphs, the notion of FA allowed …
Effectively-Propositional Reasoning about Reachability in Linked Data Structures
Abstract elided by the publisher.
Importance Splitting for Statistical Model Checking Rare Properties
Abstract elided by the publisher.
PARTY Parameterized Synthesis of Token Rings
Abstract elided by the publisher.
Incremental, Inductive Coverability
We give an incremental, inductive (IC3) procedure to check coverability of well-structured transition systems. Our procedure generalizes the IC3 procedure for safety verification that has been successfully applied in finite-state hardware verification to infinite-state well-struc…
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e., reachability) properties. They combine two key ideas --- (a) concreteness: a counterexample in an under-approximation is a counterexample in the original program a…
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
A barrier certificate is an inductive invariant function which can be used for the safety verification of a hybrid system. Safety verification based on barrier certificate has the benefit of avoiding explicit computation of the exact reachable set which is usually intractable for…
First-Order Theorem Proving and Vampire
Abstract elided by the publisher.
Under-Approximating Loops in C Programs for Fast Counterexample Detection
Abstract elided by the publisher.
Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction
Abstract elided by the publisher.
CacBDD: A BDD Package with Dynamic Cache Management
Abstract elided by the publisher.
System Level Formal Verification via Model Checking Driven Simulation
Abstract elided by the publisher.
ILP Modulo Theories
We present Integer Linear Programming (ILP) Modulo Theories (IMT). An IMT instance is an Integer Linear Programming instance, where some symbols have interpretations in background theories. In previous work, the IMT approach has been applied to industrial synthesis and design pro…
Minimal Sets over Monotone Predicates in Boolean Formulae
Abstract elided by the publisher.
The TAMARIN Prover for the Symbolic Analysis of Security Protocols
Abstract elided by the publisher.
Multi-solver Support in Symbolic Execution
Abstract elided by the publisher.