« Eliminating wordiness | Main | background reading in concurrency theory »
January 20, 2004
MAGIC: model checking for C
[MAGIC Tutorial, MAGIC home] Of particular interest in comparison with our own forthcoming model checker for C.
Uses predicate abstraction to see if the implementation conforms to a specification. You write the impl.ementation in C, and then the specification is a labeled transition system written in extended FSP notation. The extension is that you can add actions that represent returning an integer value (or void).
Library calls can be handled by allowing stubs that either replace or ignore library calls. This is handy for two reasons: first, you can deal with libraries for which you do not have the source code. second, it is the same work you'd have to do to implement compositional reasoning. So you either get compositional reasoing or ignoring of libraries for free.
Concurrency is managed by listing the names of all concurrent processes in the specification file.
Posted by jones at January 20, 2004 12:51 PM
Comments
Post a comment
Thanks for signing in, . Now you can comment. (sign out)
(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)