Write a Blog >>
ICSE 2021
Mon 17 May - Sat 5 June 2021
Wed 26 May 2021 18:15 - 18:45 at Demonstration Room - 2.2. Verification Chair(s): Francisco Servant

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.

Conference Day
Wed 26 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:15 - 18:45
2.2. VerificationDEMO - Demonstrations at Demonstration Room
Chair(s): Francisco ServantVirginia 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
30m
Demonstration
Metrinome: Path Complexity Predicts Symbolic Execution Path ExplosionDemonstration
DEMO - Demonstrations
Gabriel BesslerHarvey Mudd College, Josh CordovaHarvey Mudd College, Shaheen Cullen-BaratlooHarvey Mudd College, Sofiane DissemHarvey Mudd College, Emily LuScripps College, Ibrahim AbughararhHarvey Mudd College, Sofia DevinHarvey Mudd College, Lucas BangHarvey Mudd College
Pre-print Media Attached
18:15
30m
Demonstration
Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep LearningDemonstration
DEMO - Demonstrations
Pengyu NieUniversity of Texas at Austin, Karl PalmskogKTH Royal Institute of Technology, Junyi Jessy LiUniversity of Texas at Austin, USA, Milos GligoricUniversity of Texas at Austin
Pre-print Media Attached
18:15
30m
Demonstration
NEUROSPF: A Tool For the Symbolic Analysis of Neural NetworksDemonstration
DEMO - Demonstrations
Muhammad UsmanUniversity of Texas at Austin, USA, Yannic NollerNational University of Singapore, Corina S. PasareanuCarnegie Mellon University Silicon Valley, NASA Ames Research Center, Youcheng SunQueen's University Belfast, UK, Divya GopinathNASA Ames (KBR Inc.)
Pre-print Media Attached