11/05/2024
By Eswarasanthosh Kumar Mamillapalli
The Richard A. Miner School of Computer and Information Sciences invites you to attend a Master’s thesis defense by Eswarasanthosh Kumar Mamillapalli on: “A Debugging System for Language-parameterized Proofs."
Date: Wednesday, Nov. 20, 2024
Time : 3 p.m. to 4 p.m.
Location: DAN 321 and via Zoom
Committee:
Matteo Cimini (advisor), Miner School of Computer and Information Sciences, UMass Lowell
Anitha Gollamudi, Miner School of Computer and Information Sciences, UMass Lowell
Paul Downen, Miner School of Computer and Information Sciences, UMass Lowell
Abstract
Programming language verification aims at ensuring that the programming language being used has safety properties. As a consequence, all programs written in that programming language have that safety guarantee. Language-parameterized proofs can express proofs of language properties in a way that does not apply just to one language but, rather, to a class of languages. The advantage of using these proofs is that they can be used to establish the results for newly created languages. Lang-n-Prove is a tool that takes a language-parameterized proof and a language definition as input and produces mechanized proofs for a proof assistant. When a language-parameterized proof is incorrect, the tool blames a proof instruction in the Abella code, but that is not helpful for the user. In this thesis, we develop a debugging system that not only indicates the proof instruction that failed in the original language-parameterized proof but also strives to describe the context in which such proof instruction has failed. We have implemented our debugger within the Lang-n-Prove tool, and we illustrate its application to several examples of debugging scenarios. Our debugging system offers informative error messages.