Sciweavers

FMCAD
2004
Springer
13 years 10 months ago
Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking
Lubos Brim, Ivana Cerná, Pavel Moravec 0002...
FMCAD
2004
Springer
13 years 10 months ago
Extending Extended Vacuity
Arie Gurfinkel, Marsha Chechik
FMCAD
2004
Springer
13 years 10 months ago
Integrating Reasoning About Ordinal Arithmetic into ACL2
Abstract. Termination poses one of the main challenges for mechanically verifying infinite state systems. In this paper, we develop a powerful and extensible framework based on th...
Panagiotis Manolios, Daron Vroon
FMCAD
2004
Springer
13 years 10 months ago
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States
Most symbolic model checkers are based on either Binary Decision Diagrams (BDDs), which may grow exponentially large, or Satisfiability (SAT) solvers, whose time requirements rapi...
Mohammad Awedh, Fabio Somenzi
FMCAD
2004
Springer
13 years 10 months ago
Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs
Late changes in silicon design (ECO) is a common although undesired practice. The need for ECO exists even in high-level design flows since bugs may occur in the specifications, ...
Laurent Arditi, Gérard Berry, Michael Kishi...
FMCAD
2004
Springer
13 years 10 months ago
Simple Bounded LTL Model Checking
We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the formula and the length of the bound. The resulting CNF-fo...
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A...