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

This paper presents Metrinome, a tool for performing automatic path complexity analysis of C functions. The path complexity of a function is an expression that describes the number of paths through the function up to a given execution depth. Metrinome constructs the control flow graph (CFG) of a C function using LLVM utilities, analyzes that CFG using algebraic graph theory and analytic combinatorics, and produces a closed-form expression for the path complexity as well as the asymptotic path complexity of the function. Our experiments show that path complexity predicts the growth rate of the number of execution paths that Klee, a popular symbolic execution tool, is able to cover within a given exploration depth. Metrinome is open-source, available as a Docker image for immediate use, and all of our experiments and data are available in our repository and included in our Docker image.

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 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
30m
Demonstration
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
30m
Demonstration
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
30m
Demonstration
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