Table of Contentsdaniel jackson static analysis symposium ·santa barbara · june 2k my green eggs and ham plan of talk an example kernel: type decls kernel: expressions kernel: formulas shorthands more shorthands sample model: intentional naming intentional naming tree representation strategy alloy model: state alloy model: constraints checking assertions results counterexample time & effort other modelling experiences why modelling improves designs how analyzer works architecture example translation scheme translation tricks how (not) to delete specifying delete hacking delete (1) hacking delete (2) step 1: unroll control flow graph step 2: encode control flow step 3: encode dataflow frame conditions sample results promising? summary related work PPT Slide |
Author: Daniel Jackson
Email: dnj@lcs.mit.edu Home Page: http://sdg.lcs.mit.edu/~dnj |