Verification State-Space Reduction Through Restricted Parsing Environments

Explore a presentation on reducing verification state-space through restricted parsing environments. Learn about the LangSec principles for constructing input-handling software and their potential to significantly reduce the size and complexity of verification tasks. Discover Crema, a sub-Turing programming language and restricted execution environment, and examine a case study comparing verification task sizes for Qmail SMTP parsing code fragments in native execution versus Crema. Delve into the application of these principles to reference monitor verification, and gain insights into future work in this field. The talk covers topics such as input parsing, open source, static analysis, formal tools, and contextual implementation, providing a comprehensive overview of state-space reduction techniques in software verification.