Papers /

Beckman-SSTA 2008

Reading

Outdoors

Games

Hobbies

LEGO

Food

Code

Events

Nook

sidebar

Beckman-SSTA 2008

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
Recent Changes (All) | Edit SideBar Page last modified on March 04, 2010, at 08:47 AM Edit Page | Page History