Sciweavers

SPIN
2005
Springer
14 years 4 months ago
An Incremental Heap Canonicalization Algorithm
Abstract. The most expensive operation in explicit state model checking is the hash computation required to store the explored states in a hash table. One way to reduce this comput...
Madanlal Musuvathi, David L. Dill
SPIN
2005
Springer
14 years 4 months ago
Model Checking Machine Code with the GNU Debugger
Embedded software verification is an important verification problem that requires the ability to reason about the timed semantics of concurrent behaviors at a low level of atomic...
Eric Mercer, Michael Jones
SPIN
2005
Springer
14 years 4 months ago
SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions
Anil Madhavapeddy, David Scott, Richard Sharp
SPIN
2005
Springer
14 years 4 months ago
Memory Efficient State Space Storage in Explicit Software Model Checking
Sami Evangelista, Jean-François Pradat-Peyr...
SPIN
2005
Springer
14 years 4 months ago
Etch: An Enhanced Type Checking Tool for Promela
We present ETCH, an enhanced type checking tool for the Promela language. This tool uses standard type checking in conjunction with constraint-based type inference to detect type e...
Alastair F. Donaldson, Simon J. Gay
SPIN
2005
Springer
14 years 4 months ago
Sound Transaction-Based Reduction Without Cycle Detection
Vladimir Levin, Robert Palmer, Shaz Qadeer, Sriram...
SPIN
2005
Springer
14 years 4 months ago
Repairing Structurally Complex Data
We present a novel algorithm for repairing structurally complex data. Given an assertion that represents desired structural integrity constraints and a structure that violates them...
Sarfraz Khurshid, Iván García, Yuk L...
SPIN
2005
Springer
14 years 4 months ago
Symbolic Model Checking for Asynchronous Boolean Programs
Abstract. Software model checking problems generally contain two different types of non-determinism: 1) non-deterministically chosen values; 2) the choice of interleaving among th...
Byron Cook, Daniel Kroening, Natasha Sharygina
SPIN
2005
Springer
14 years 4 months ago
Execution Generated Test Cases: How to Make Systems Code Crash Itself
Abstract. This paper presents a technique that uses code to automatically generate its own test cases at run-time by using a combination of symbolic and concrete (i.e., regular) ex...
Cristian Cadar, Dawson R. Engler