Toward special-purpose program verification
Paul Eggert · 1990
Program verification has seen little practical, automated use.How can its good ideas be revived in a practical setting?One way is to lower its sights: instead of checking that a program matches its specification, one can perform less ambitious but more feasible checking.Much recent work has lowered sights by checking only specifications and not programs.By characterizing software failures by their detection method, we have decided instead to try checking only programs and not specifications.Our goal is to integrate run-time checking into a compiler, so that programs never commit common run-time faults like following bad pointers or violating array boundaries.