MIT Department of Electrical Engineering & Computer Science
Using Relations and Symmetry to Find Bugs in Software Specifications
Daniel Jackson
Carnegie Mellon University
Wednesday, March 19, 1997
4:00 PM (3:45 refreshments)
Room NE43-518
EECS Special Seminar
Abstract
I'll explain a technique I have developed for finding flaws in
specifications of software systems. The intended behaviour of the system is
cast in a simple but expressive relational language, along with some claims
that certain properties hold. This description is then subjected to an
automatic analysis that enumerates all cases within a finite bound, in an
attempt to find counterexamples that demonstrate how the specification
fails to satisfy properties.
In general, the problem is intractable, but by exploiting symmetries in the
relation values that constitute the data structures of the state, it is
possible to prune the search for counterexamples dramatically, so that
large spaces can be covered in a reasonable time.
URL of this page:
http://www-eecs.mit.edu/AY96-97/events/26.html
Created: Mar 12, 1997
|
Modified: Jun 24, 1997
This announcement is from the MIT EECS 1996-97 archive.
|
Current events
To MIT EECS home page
|
Your comments
and inquiries are welcome.
