Complexity verification using guided theorem enumeration
Abstract
Determining if a given program satisfies a given bound on the amount of resources that it may use is a fundamental problem with critical practical applications. Conventional automatic verifiers for safety properties cannot be applied to address this problem directly because such verifiers target properties expressed in decidable theories; however, many practical bounds are expressed in nonlinear theories, which are undecidable.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 01, 2017
- Source ID
- 10.1145/3093333.3009864
Entities
People
- Akhilesh Srikanth
- Burak Sahin
- William R. Harris
Organizations
- Defense Advanced Research Projects Agency
- Georgia Tech
- National Science Foundation