Amin Manna

Amin  Manna
MIT EECS Undergraduate Research and Innovation Scholar
Advisor: Armando Solar-Lezama
Department: Electrical Engineering and Computer Science
Areas of Research: Theory of Computer Science
Years: 2016-2017
abstract:

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 ‘proof by induction' that can be applied to prove a theorem. The holy grail of formal verification is creating a ‘push-button' verifier that can prove any theorem but this is a difficult goal. My work will focus on developing a ‘push-button' verifier for theorems specifically related to data structure invariants. Its conclusion will see increased adoption of formal proofs in the technology industry.
About:

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.