CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
The relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen's interval algebra (or Allen's temporal logic,...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...
CAV
2006
Springer
13 years 8 months ago
2006
Springer
CAV
2006
Springer
13 years 8 months ago
2006
Springer
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...