Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:00 - 18:15 at VMCAI - Model Checking Chair(s): James R. Wilcox

Modular approaches to verifying interprocedural programs involve learning summaries for individual procedures rather than verifying a monolithic program. Modern approaches based on use of Satisfiability Modulo Theory (SMT) solvers have made much progress in this direction. However, it is still challenging to handle mutual recursion and to derive adequate procedure summaries using scalable methods. We propose a novel modular verification algorithm that addresses these challenges by learning lemmas about the relationships among procedure summaries and by using bounded environments in SMT queries. We have implemented our algorithm in a tool called Clover and report on a detailed evaluation that shows that it outperforms existing automated tools on benchmark programs with mutual recursion while being competitive on standard benchmarks.

Mon 18 Jan

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

18:00 - 18:30
Model CheckingVMCAI at VMCAI
Chair(s): James R. Wilcox University of Washington
18:00
15m
Talk
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University
Media Attached
18:15
15m
Talk
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
VMCAI
Hongce Zhang Princeton University, Aarti Gupta Princeton University, Sharad Malik Princeton University
Media Attached