Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep LearningDemonstration
Naming conventions are an important concern in large verification projects using proof assistants, such as Coq. In particular, lemma names are used by proof engineers to effectively understand and modify Coq code. However, providing accurate and informative lemma names is a complex task, which is currently often carried out manually. Even when lemma naming is automated using rule-based tools, generated names may fail to adhere to important conventions not specified explicitly. We demonstrate a toolchain, dubbed Roosterize, which automatically suggests lemma names in Coq projects. Roosterize leverages a neural network model trained on existing Coq code, thus avoiding manual specification of naming conventions. To allow proof engineers to conveniently access suggestions from Roosterize during Coq project development, we integrated the toolchain into the popular Visual Studio Code editor. Our evaluation shows that Roosterize substantially outperforms strong baselines for suggesting lemma names and is useful in practice. The demo video for Roosterize can be viewed at: https://youtu.be/HZ5ac7Q14rc.
Wed 26 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:15 - 18:45 | 2.2. VerificationDEMO - Demonstrations at Demonstration Room Chair(s): Francisco Servant Virginia Tech Each demo makes a 1-minute presentation (displayed in the Demo room). At the end of each presentation, a breakout room will be created for each demo. Attendees will be able to join and discuss with the authors. | ||
18:15 30mDemonstration | Metrinome: Path Complexity Predicts Symbolic Execution Path ExplosionDemonstration DEMO - Demonstrations Gabriel Bessler Harvey Mudd College, Josh Cordova Harvey Mudd College, Shaheen Cullen-Baratloo Harvey Mudd College, Sofiane Dissem Harvey Mudd College, Emily Lu Scripps College, Ibrahim Abughararh Harvey Mudd College, Sofia Devin Harvey Mudd College, Lucas Bang Harvey Mudd College Pre-print Media Attached | ||
18:15 30mDemonstration | Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep LearningDemonstration DEMO - Demonstrations Pengyu Nie University of Texas at Austin, Karl Palmskog KTH Royal Institute of Technology, Junyi Jessy Li University of Texas at Austin, USA, Milos Gligoric University of Texas at Austin Pre-print Media Attached | ||
18:15 30mDemonstration | NEUROSPF: A Tool For the Symbolic Analysis of Neural NetworksDemonstration DEMO - Demonstrations Muhammad Usman University of Texas at Austin, USA, Yannic Noller National University of Singapore, Corina S. Pasareanu Carnegie Mellon University Silicon Valley, NASA Ames Research Center, Youcheng Sun Queen's University Belfast, UK, Divya Gopinath NASA Ames (KBR Inc.) Pre-print Media Attached |