Implementing systems in test wizards like Coq and demonstrating their accuracy with all the formal details has shown promise in providing extremely strong guarantees on critical software, ranging from compilers and operating systems to databases and web browsers. Unfortunately, these verifications demand such a heroic manual testing effort, even for a single system, that the approach has not been widely adopted.
We demonstrate a technique to remove the manual test burden to verify many properties within an entire class of applications, in our case, reactive systems, while only devoting comparable effort to manual verification of a single system. A crucial idea of our approach is to simultaneously design (1) a domain-specific language (DSL) to express reactive systems and their correction properties and (2) test automation that exploits the restricted language of both programs and properties to allow fully automatic automation, push-button verification.
We apply this information in a deeply integrated Coq DSL, called REFLEX, and illustrate the expressiveness of REFLEX by implementing and automatically verifying realistic systems that include a modern web browser, an SSH server, and a web server. Using REFLEX dramatically reduced the burden of proof: in similar earlier versions of our expertly written Coq benchmarks, the tests accounted for more than 80% of the code base; our versions do not require manual testing.
- Authors: Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock and Sorin Lerner
- Tags: Coq, Test Assistants, Reactive Systems, Formal Verification
- Length: 11
- Submitted by: BmoreDaniel
- Submission date: July 21, 2014
- Favorites: 5
- Times read: 3
