shape analysis with SAT Daniel Jackson & Mandana Vaziri Software Design Group, MIT LCS Schloss Ringberg February 21, 2000

3/20/00


Click here to start


Table of Contents

shape analysis with SAT Daniel Jackson & Mandana Vaziri Software Design Group, MIT LCS Schloss Ringberg February 21, 2000

why software model checking?

how would model checking differ for software?

progress so far

BART railway problem

sample alloy model

alcoa: alloy constraint analyzer

analyzing code

example

programming language

formula language

modelling state

sequential composition

translation scheme

translation rules

from formula to counterexample

null derefs (1)

null derefs (2)

example in full

jumps

a small experiment

sample specs

what next?

related work

conclusion

Author: Daniel Jackson

Email: dnj@lcs.mit.edu

Home Page: http://sdg.lcs.mit.edu/~dnj

Download presentation source