loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems (VLSID'07)
Bangalore, India
January 06-January 10
ISBN: 0-7695-2762-0
Vishnu C. Vimjam, Virginia Tech
Michael S. Hsiao, Virginia Tech
Strengthening a property allows it to be falsified/verified at an earlier induction depth. In this paper, we propose new preprocessing techniques for explicitly identifying co-invariants for a given safety property which are then added to that property for faster verification. First, we employ a path-oriented decision making engine to quickly identify several states which have paths to states violating the property. Next, we generate a set of candidate co-invariants and propose an induction-based technique to learn true co-invariants among those candidates. All the learned co-invariants are minimized using resolution and added to the original property to strengthen it. Experiments show that the induction depth needed to prove many safety properties can be significantly reduced via our strengthening, thereby achieving more than an order of magnitude runtime improvements.
Citation:
Vishnu C. Vimjam, Michael S. Hsiao, "Explicit Safety Property Strengthening in SAT-based Induction," vlsid, pp.63-68, 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems (VLSID'07), 2007
Usage of this product signifies your acceptance of the Terms of Use.