Automation of Premise Selection to Enable More Software Verification 

Presenter

Simran Lekhwani

Campus

UMass Amherst

Sponsor

Yuriy Brun, Department of Computer Science, UMass Amherst

Schedule

Session 2, 11:30 AM - 12:15 PM [Schedule by Time][Poster Grid for Time/Location]

Location

Poster Board A38, Campus Center Auditorium, Row 2 (A21-A40) [Poster Location Map]

Abstract

Verifying software functionality using proof synthesis is crucial but also time-consuming and labor-intensive, when performed manually. Interactive Theorem Provers, like Coq and Isabelle, try to help.  We aim to automate proof synthesis by augmenting an existing, search-based proof synthesis tool, Proverbot9001, with additional proof context. 

We devised a custom script that tokenizes proof goal and selects a list of twenty related lemmas based on the top keyword of the goal. We passed this list, combined with the local lemmas defined in the proof context, to Proverbot9001 as additional context. Our approach increased the number of theorems Proverbot9001 was able to prove completely automatically from 21 to 26, out of 89, a 5.6% improvement. 

Keywords

Software Verification, Software Engineering , Automation, Premise Selection

Research Area

Computer Science

SIMILAR ABSTRACTS (BY KEYWORD)