FM
2003
Springer
14 years 4 months ago
2003
Springer
Incomplete, inaccurate, ambiguous, and volatile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods o...
FM
2003
Springer
14 years 4 months ago
2003
Springer
The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a correspond...
FATES
2003
Springer
14 years 4 months ago
2003
Springer
Most efforts to combine formal methods and software testing go in the direction of exploiting formal methods to solve testing problems, most commonly test case generation. Here we ...
CAV
2003
Springer
14 years 4 months ago
2003
Springer
CAV
2003
Springer
14 years 4 months ago
2003
Springer
CAV
2003
Springer
14 years 4 months ago
2003
Springer
Abstract. The theme of this paper is certifying software for state estimation of dynamic systems, which is an important problem found in spacecraft, aircraft, geophysical, and in m...
CAV
2003
Springer
14 years 4 months ago
2003
Springer
We show that the model checking problem for µ-calculus on graphs of bounded tree-width can be solved in time linear in the size of the system. The result is presented by first sh...
CAV
2003
Springer
14 years 4 months ago
2003
Springer
Abstract. We consider a fully SAT-based method of unbounded symbolic model checking based on computing Craig interpolants. In benchmark studies using a set of large industrial circ...
CAV
2003
Springer
14 years 4 months ago
2003
Springer
The paper considers the problem of checking abstraction between two finite-state fair discrete systems (FDS). In automata-theoretic terms this is trace inclusion between two nond...
CAV
2003
Springer
14 years 4 months ago
2003
Springer
ion and BDDs Complement SAT-based BMC in DiVer Aarti Gupta1, Malay Ganai1 , Chao Wang2, Zijiang Yang1, Pranav Ashar1 1 NEC Laboratories America, Princeton, NJ, U.S.A. 2 University ...