Foundational Verification of Running-Time Bounds for Interactive Programs

The field of formal methods has a rich history of practical application in verification of the correctness of software. Existing verification tooling operates at a wide range of rigor, from proving relatively weak properties via traditional static analysis to powerful theorem provers that can express very precise specifications. It is sometimes desirable to prove properties about programs that make reference to not just semantic behavior but also to other metaproperties of the program’s execution, such as runtime or I/O histories. There is also a wide variety of existing tooling for proving bounds on program runtime. However, there is no prior work on a maximally rigorous verification system that can prove predicates involving all of semantic behavior, runtime, and I/O. Our contribution is exactly that – we extend the existing Bedrock2 framework, which implements a C-like systems language within a powerful proof engine together with a verified compiler capable of expressing arbitrary proof conditions involving behavior and I/O, and augment it to add the capacity to reason about runtime as well. As a capstone proof of concept, we apply the new metrics machinery to an IoT lightbulb controller (already verified with respect to the previous framework) and produce a new specification with time bounds based on arrival of network packets.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2025

Author dc:creator

• Tockman, Andrew

Advisor dc:contributor.advisor

• Chlipala, Adam

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright retained by author(s)

Licence dc:rights.uri

• https://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/162994

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/162994