(1) developing an optimization algorithm with 10 constraints took one staff month with a theory that has eight object types, 30 predicates, 50 axioms and 20 pages. Highly modifiable. Adding a constraint typically took one day.
(2) Specification on a 43 state machine, 83 transitions, 40 state variables... and a theory with 150 predicates and functions. "in software engineering, inference methods are not intended to prove isolated deep theorems by reasoning from a few laws, but rather to prove lots of trivial theorems in a sea of axioms and facts.
(3) The theory of static Ada Arrays - 17 axioms. Ada Integers 60 axioms. Able to automatically analyse 30,000 lines of Ada code and enumerate all 200,000 feasible paths through 200 conditions. Took 10 DAYS on a SparcStation2. "synthesis technology should spawn good analysis technology"[because]"Good synthesis technology requires sophisticatedsoftware representation and analysis capabilities"
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]