Sciweavers

Share
CAV
2006
Springer
133views Hardware» more  CAV 2006»
8 years 11 months ago
Antichains: A New Algorithm for Checking Universality of Finite Automata
We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction...
Martin De Wulf, Laurent Doyen, Thomas A. Henzinger...
CAV
2006
Springer
125views Hardware» more  CAV 2006»
8 years 11 months ago
cascade: C Assertion Checker and Deductive Engine
We present a tool, called CAsCaDE, to check assertions in C programs as part of a multi-stage verification strategy. CAsCaDE takes as input a C program and a control file (the outp...
Nikhil Sethi, Clark Barrett
CAV
2006
Springer
120views Hardware» more  CAV 2006»
8 years 11 months ago
Model Checking Multithreaded Programs with Asynchronous Atomic Methods
Abstract. In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchron...
Koushik Sen, Mahesh Viswanathan
CAV
2006
Springer
209views Hardware» more  CAV 2006»
8 years 11 months ago
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools
CUTE, a Concolic Unit Testing Engine for C and Java, is a tool to systematically and automatically test sequential C programs (including pointers) and concurrent Java programs. CUT...
Koushik Sen, Gul Agha
CAV
2006
Springer
164views Hardware» more  CAV 2006»
8 years 11 months ago
Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis
The relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen's interval algebra (or Allen's temporal logic,...
Grigore Rosu, Saddek Bensalem
CAV
2006
Springer
157views Hardware» more  CAV 2006»
8 years 11 months ago
Lazy Abstraction with Interpolants
traction with Interpolants K. L. McMillan Cadence Berkeley Labs Abstract. We describe a model checker for infinite-state sequential proased on Craig interpolation and the lazy abst...
Kenneth L. McMillan
CAV
2006
Springer
146views Hardware» more  CAV 2006»
8 years 11 months ago
Termination Analysis with Calling Context Graphs
We introduce calling context graphs and various static and theorem proving based analyses that together provide a powerful method for proving termination of programs written in fea...
Panagiotis Manolios, Daron Vroon
CAV
2006
Springer
101views Hardware» more  CAV 2006»
8 years 11 months ago
Abstraction for Shape Analysis with Fast and Precise Transformers
Tal Lev-Ami, Neil Immerman, Shmuel Sagiv
CAV
2006
Springer
110views Hardware» more  CAV 2006»
8 years 11 months ago
Improving Pushdown System Model Checking
Abstract. In this paper, we reduce pushdown system (PDS) model checking to a graphtheoretic problem, and apply a fast graph algorithm to improve the running time for model checking...
Akash Lal, Thomas W. Reps
books