Increasing Automation in Verification of Realworld System Code
In a world dominated by technology there is an increasing need for software transparency and correctness. The industry standard is to write test cases that verify the correctness of code in most cases but an alternative is formal verification; which refers to the writing of formal proofs about desirable invariants. Theorem provers such as Coq define tactics like ° °°Sproof by induction’ that can be applied to prove a theorem. The holy grail of formal verification is creating a ° °°Spush-button’ verifier that can prove any theorem but this is a difficult goal. My work will focus on developing a ° °°Spush-button’ verifier for theorems specifically related to data structure invariants. Its conclusion will see increased adoption of formal proofs in the technology industry.

I am studying pure computer science at MIT and have participated in the design and implementation of many software systems implemented in various coding languages. The construct of language both computer and natural fascinates me and indeed this is why I am also concentrating in Linguistics. I am excited to apply the same rigorous analysis to computer languages and I look forward to learning that in this SuperUROP.