Tools Based on Model Checking

The SLAM tool ( developed at Microsoft Research has been used to verify device drivers successfully.

The BLAST tool (, developed at the EPFL in Switzerland, the University of California at San Diego and at Los Angeles, and Simon Fraser University, also gives good results for low-level system code.

Both tools use a technique called predicate abstraction to reduce the verification of C program properties to the following subproblems:

• Automatically finding a proof for a number of relatively simple theorems, using available techniques and even tools, produced in the field of automatic theorem proving

• Verifying the accessibility properties of a finite state system, for which techniques have been refined over the years in the field of model checking

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook

Post a comment