Witnessability of Undecidable Problems
Abstract
Many problems in programming language theory and formal methods are undecidable, so they cannot be solved precisely. Practical techniques for dealing with undecidable problems are often based on decidable approximations. Undecidability implies that those approximations are always imprecise. Typically, practitioners use heuristics and ad hoc reasoning to identify imprecision issues and improve approximations, but there is a lack of computability-theoretic foundations about whether those efforts can succeed.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 09, 2023
- Source ID
- 10.1145/3571227
Entities
People
- Qirun Zhang
- Shuo Ding
Organizations
- Defense Advanced Research Projects Agency
- Georgia Tech
- National Science Foundation