Reference counting is a widely-used resource management idiom which maintains a count of references to each resource by incrementing the count upon an acquisition, and decrementing...
Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Ma...
Abstract. Directed model checking is a well-established technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by in...
Martin Wehrle, Sebastian Kupferschmid, Andreas Pod...
TAPAS is a suite of libraries dedicated to FO (R, Z, +, ≤). The suite provides (1) the application programming interface GENEPI for this logic with encapsulations of many classic...
Abstract. In this paper we prove that the transitive closure of a nondeterministic octagonal relation using integer counters can be expressed in Presburger arithmetic. The direct c...
Analysis of execution traces plays a fundamental role in many program analysis approaches. Execution traces are frequently parametric, i.e., they contain events with parameter bind...
Abstract. This paper presents algorithms and data structures that exploit a compositional and hierarchical specification to enable more efficient symbolic modelchecking. We encod...
Software testing is an essential process to improve software quality in practice. Researchers have proposed several techniques to automate parts of this process. In particular, sym...
Dries Vanoverberghe, Nikolai Tillmann, Frank Piess...
In the past, several attempts have been made to deal with the state space explosion problem by equipping a depth-first search (DFS) algorithm with a state cache, or by avoiding co...