SpaceSearch: a library for building and verifying solver-aided tools
Abstract
Many verification tools build on automated solvers. These tools reduce problems in a specific application domain (e.g., compiler optimization validation) to queries that can be discharged with a highly optimized solver. But the correctness of the reductions themselves is rarely verified in practice, limiting the confidence that the solver's output establishes the desired domain-level property.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 29, 2017
- Source ID
- 10.1145/3110269
Entities
People
- Emina Torlak
- Konstantin Weitz
- Michael D. Ernst
- Stefan Heule
- Steven Lyubomirsky
- Zachary Tatlock
Organizations
- Air Force Research Laboratory
- Defense Advanced Research Projects Agency
- Stanford University
- United States Air Force
- University of Washington