FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
We present a general approach for verifying safety properties of Lustre programs automatically. Key aspects of the approach are the choice of an expressive first-order logic in wh...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
Performing synthesis and verification in isolation has two undesirable consequences: (1) verification runs the risk of becoming intractable, and (2) strong sequential optimization...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
The quality of formal specifications and the circuits they are written for can be evaluated through checks such as vacuity and coverage. Both checks involve mutations to the specif...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
We describe a general approach for defining new temporal specification languages, and adopting existing languages, for SystemC. We define the concept of "underlying trace"...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
A message flow is a sequence of messages sent among processors during the execution of a protocol, usually illustrated with something like a message sequence chart. Protocol design...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
We present a method for verifying information flow properties of software programs using inductive assertions and theorem proving. Given a program annotated with information flow a...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
Abstract-- We consider the problem of optimal netlist simplification in the presence of constraints. Because constraints restrict the reachable states of a netlist, they may enhanc...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solv...
FMCAD
2008
Springer
14 years 2 months ago
2008
Springer
Parameterized model checking refers to any method that extends traditional, finite-state model checking to handle systems arbitrary number of processes. One popular approach to thi...