Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2000
Springer
187views Hardware» more  CAV 2000»
11 years 9 months ago
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Di...
Poul Frederick Williams, Armin Biere, Edmund M. Cl...
CAV
2000
Springer
138views Hardware» more  CAV 2000»
11 years 9 months ago
Counterexample-Guided Abstraction Refinement
xample-Guided Abstraction Refinement for Symbolic Model Checking EDMUND CLARKE YUAN LU Carnegie Mellon University, Pittsburgh, Pennsylvania Broadcom Co., San Jose, California ORNA ...
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan ...
CAV
2000
Springer
108views Hardware» more  CAV 2000»
11 years 9 months ago
Boolean Satisfiability with Transitivity Constraints
Randal E. Bryant, Miroslav N. Velev
CAV
2000
Springer
125views Hardware» more  CAV 2000»
11 years 9 months ago
Efficient Reachability Analysis of Hierarchical Reactive Machines
Hierarchical state machines is a popular visual formalism for software specifications. To apply automated analysis to such specifications, the traditional approach is to compile th...
Rajeev Alur, Radu Grosu, Michael McDougall
CAV
2000
Springer
89views Hardware» more  CAV 2000»
11 years 10 months ago
Tuning SAT Checkers for Bounded Model Checking
Abstract. Bounded Model Checking based on SAT methods has recently been introduced as a complementary technique to BDD-based Symbolic Model Checking. The basic idea is to search fo...
Ofer Strichman
CAV
2000
Springer
141views Hardware» more  CAV 2000»
11 years 10 months ago
Binary Reachability Analysis of Discrete Pushdown Timed Automata
We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A con guration of a discrete pushdown timed automa...
Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard ...
CAV
2000
Springer
94views Hardware» more  CAV 2000»
11 years 10 months ago
IF: A Validation Environment for Timed Asynchronous Systems
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu...
CAV
2000
Springer
106views Hardware» more  CAV 2000»
11 years 10 months ago
Regular Model Checking
Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Ta...
CAV
2000
Springer
197views Hardware» more  CAV 2000»
11 years 10 months ago
Bounded Model Construction for Monadic Second-Order Logics
Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion . . . . . . . . . . . . . . . . . . . . . . . . . . 1 A. Pnueli Invited Address...
Abdelwaheb Ayari, David A. Basin
CAV
2000
Springer
97views Hardware» more  CAV 2000»
11 years 10 months ago
Detecting Errors Before Reaching Them
Abstract. Any formalmethodor tool is almostcertainlymoreoftenapplied in situationswheretheoutcomeis failure(acounterexample)rather than success (a correctness proof). We present a ...
Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. ...
books