Program Model Checking : A Practitioner's Guide
- Pasareanu, Corina S.
- March 2008.
- Physical Description:
- 1 electronic document
- Additional Creators:
- Mansouri-Samani, Masoud, Brat, Guillaume P., Markosian, Lawrence Z., Mehlitz, Peter C., Visser, Willem C., Penix, John J., and Pressburger, Thomas T.
- hdl.handle.net , Connect to this object online.
- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
- Program model checking is a verification technology that uses state-space exploration to evaluate large numbers of potential program executions. Program model checking provides improved coverage over testing by systematically evaluating all possible test inputs and all possible interleavings of threads in a multithreaded system. Model-checking algorithms use several classes of optimizations to reduce the time and memory requirements for analysis, as well as heuristics for meaningful analysis of partial areas of the state space Our goal in this guidebook is to assemble, distill, and demonstrate emerging best practices for applying program model checking. We offer it as a starting point and introduction for those who want to apply model checking to software verification and validation. The guidebook will not discuss any specific tool in great detail, but we provide references for specific tools.
- Other Subject(s):
- NASA Technical Reports Server (NTRS) Collection.
- Document ID: 20080015887.
- Copyright, Distribution as joint owner in the copyright.
View MARC record | catkey: 15999908