12.6 Accelerating Verification through Transformation and Abstraction
Date:
Thu, 2009-04-23Time:
16:00 - 17:30Location / Room:
Uranie, Level 3Moderators:
D Borrione, TIMA Laboratory, FR
R Bloem, TU Graz, AT
Formal verification is a computationally intractable problem, though through recent advances it has become an essential tool for the EDA community. This session includes three papers introducing techniques to enhance the scalability of formal verification algorithms through simplifying transformations. The fourth proposes a technique to enhance the quality of the verification process.
| 1600 | SPECULATIVE REDUCTION-BASED SCALABLE REDUNDANCY IDENTIFICATION H Mony and J Baumgartner, IBM Corporation, US A Mishchenko and R Brayton, UC Berkeley, US |
| 1630 | SCALABLE LIVENESS CHECKING VIA PROPERTY-PRESERVING TRANSFORMATIONS J Baumgartner and H Mony, IBM Corporation, US |
| 1700 (S) | SPEEDING UP MODEL CHECKING EXPLOITING EXPLICIT AND HIDDEN VERIFICATION CONSTRAINTS G Cabodi, P Camurati, L Garcia, M Murciano, S Nocco and S Quer, Politecnico di Torino, IT |
| 1715 (S) | STRENGTHENING PROPERTIES USING ABSTRACTION REFINEMENT M Purandare, ETH Zurich, CH T Wahl and D Kroening, Oxford U, UK |
