Model Checking Boolean Programs (b/w print)
Usually printed in 3 - 5 business days
A successful approach to push the boundaries of Modelchecking is predicate abstraction. With this method, an abstraction of a program in a high-level programming language is constructed using predicates and represented as a Boolean program. It is analyzed by a dedicated checker to determine if an error state is reachable. Boolean program verification remains, despite the reduced state space, the bottleneck within the automated abstraction-refinement loop.
This book introduces techniques for efficient reachability analysis of sequential and concurrent Boolean programs. We improve on known summarization algorithms for sequential Boolean programs and propose over-approximations of procedure calls. For non-recursive concurrent Boolean programs, we introduce a transformation to a representation , which exploits the symmetry inherent in replicated programs. This allows exact verification of an unbounded number of threads.
Details
- Publication Date
- Aug 7, 2010
- Language
- English
- ISBN
- 9780557639786
- Category
- Computers & Technology
- Copyright
- All Rights Reserved - Standard Copyright License
- Contributors
- By (author): Gérard Basler
Specifications
- Pages
- 156
- Binding
- Perfect Bound
- Interior Color
- Black & White
- Dimensions
- Crown Quarto (7.44 x 9.68 in / 189 x 246 mm)