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: Applying Formal Methods to Cryptographic Protocol Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 C. Meadows Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 J. Marques-Silva, K. Sakallah Invited Tutorial: Verification of Infinite-State and Parameterized Systems . 4 P.A. Abdulla, B. Jonsson Regular Papers action Algorithm for the Verification of Generalized C-Slow Designs 5 J. Baumgartner, A. Tripp, A. Aziz, V. Singhal, F. Andersen Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits 20 T. Heyman, D. Geist, O. Grumberg, A. Schuster An Automata-Theoretic Approach to Reaso...

• Type: Conference
• Year: 2000
• Where: CAV
• Authors: Abdelwaheb Ayari, David A. Basin
• Keywords: Boolean Satisfiability, CAV 2000, Hardware, Pnueli Invited Address, Reachability Analysis