Explore property-based testing (PBT) and its integration with formal verification in this 24-minute ACM SIGPLAN conference talk. Learn how PBT can be used to reduce formal software verification effort and incrementally gain greater assurance in code correctness. Discover the integration of PBT into the verification framework of Cogent, a programming language with a certifying compiler for high-assurance systems components. Understand how structuring tests to mirror refinement proofs allows PBT and formal verification to work in tandem. Examine the benefits of this mutualistic approach for developers and explore techniques used in this style of PBT through two concrete examples. Follow the roadmap from introduction to conclusion, covering topics such as data refinement, PBT framework, and using PBT as a temporary substitute for verification.
Overview
Syllabus
Intro
Roadmap
Property-Based Testing (PBT)
Example: PBT
Verification Framework
Data Refinement
PBT Framework
The COGENT Case of PBT
Testing in Lieu of Verification (Temporarily)
PBT Provides Design Guidelines
Conclusion
Thank You
Taught by
ACM SIGPLAN
