Finding code that explodes under symbolic evaluation
Abstract
Solver-aided tools rely on symbolic evaluation to reduce programming tasks, such as verification and synthesis, to satisfiability queries. Many reusable symbolic evaluation engines are now available as part of solver-aided languages and frameworks, which have made it possible for a broad population of programmers to create and apply solver-aided tools to new domains. But to achieve results for real-world problems, programmers still need to write code that makes effective use of the underlying engine, and understand where their code needs careful design to elicit the best performance. This task is made difficult by the all-paths execution model of symbolic evaluators, which defies both human intuition and standard profiling techniques.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 24, 2018
- Source ID
- 10.1145/3276519
Entities
People
- Emina Torlak
- James Bornholt
Organizations
- Alfred P. Sloan Foundation
- Defense Advanced Research Projects Agency
- Intel Corporation
- Meta
- National Science Foundation
- University of Washington