|
 ABSTRACT
We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a pipelined ALU circuit with over 101300 states.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
|
| |
2
|
|
 |
3
|
J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States
[doi> 10.1145/127601.127702]
|
| |
4
|
J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States
[doi> 10.1145/123186.123223]
|
| |
5
|
|
| |
6
|
|
| |
7
|
|
| |
8
|
|
| |
9
|
O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proc. 1990 IEEE Inter. Conf. on Comput.-Aided Design. IEEE Comp. Soc. Press, Nov. 1990.
|
| |
10
|
|
| |
11
|
|
| |
12
|
|
| |
13
|
Z. Har'E1 and R. P. Kurshan. The COSPAN user's guide. Technical Report 11211-871009-21TM, AT&T Bell Labs, 1987.
|
| |
14
|
|
| |
15
|
|
| |
16
|
J. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. Fifth Inter. Syrup. in Programming, 1981.
|
| |
17
|
|
| |
18
|
|
CITED BY 51
|
|
|
|
|
|
|
|
Massimiliano Chiodo , Thomas R. Shiple , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Automatic compositional minimization in CTL model checking, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.172-178, November 1992, Santa Clara, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
Constance Heitmeyer , James Kirby , Bruce Labaw, Applying the SCR requirements method to a weapons control panel: an experience report, Proceedings of the second workshop on Formal methods in software practice, p.92-102, March 04-05, 1998, Clearwater Beach, Florida, United States
|
|
|
|
|
|
|
|
|
Tarvo Raudvere , Ingo Sander , Ashish Kumar Singh , Axel Jantsch, Verification of design decisions in ForSyDe, Proceedings of the 1st IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, October 01-03, 2003, Newport Beach, CA, USA
|
|
|
Jörg Bormann , Jörg Lohse , Michael Payer , Gerd Venzl, Model checking in industrial hardware design, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.298-303, June 12-16, 1995, San Francisco, California, United States
|
|
|
|
|
|
Roderick Bloem , Kavita Ravi , Fabio Somenzi, Symbolic guided search for CTL model checking, Proceedings of the 37th conference on Design automation, p.29-34, June 05-09, 2000, Los Angeles, California, United States
|
|
|
|
|
|
Christoph Meinel , Fabio Somenzi , Thorsten Theobald, Linear sifting of decision diagrams, Proceedings of the 34th annual conference on Design automation, p.202-207, June 09-13, 1997, Anaheim, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Alberto L. Sangiovanni-Vincentelli , Patrick C. McGeer , Alexander Saldanha, Verification of electronic systems, Proceedings of the 33rd annual conference on Design automation, p.106-111, June 03-07, 1996, Las Vegas, Nevada, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
|
|
|
Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
|
|
|
|
|
|
|
|
|
Eric Verlind , Tilman Kolks , Gjalt de Jong , Bill Lin , Hugo De Man, A time abstraction method for efficient verification of communicating systems, Proceedings of the 31st annual conference on Design automation, p.609-614, June 06-10, 1994, San Diego, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.3