Proofs from Tests

Beckman, Nori, Rajamani, Simmons

program verification proof testing software engineering

@conference{beckman:ssta-2008,
  title={Proofs from Tests},
  author={Nels E. Beckman and Aditya V. Nori and Sriram K. Rajamani and
            Robert J. Simmons},
  booktitle={International Symposium on Software Testing and Analysis},
  pages={3--13},
  year={2008},
  organization={{ACM}}
}

Want to show that a program correctly implements some specification

• A safety condition

Use tests to refine a model of the program until it is shown that the requirement is not violated

Light-weight symbolic execution to do test generation

• Simultaneous perform program testing and program abstraction
  • Tests "underapproximate" program, abstraction "overapproximates"

Cannot call theorem prover repeatedly, it's just too costly a computation

Directed testing

May not terminate

Verification tools use abstraction to manage loops, but don't handle aliases well Testing tools handle aliases well, but not loops

Uses CIL infrastructure, F# programming language, Z3 theorem prover

• L. de Moura and N. Bjorner. Z3: An efficient smt solver. In TACAS '08: Tools and Algorithms for the Construction and Analysis of Systems, 2008