Unbounded Procedure Summaries from Bounded Environments

Lauren Pick, Grigory Fedyukovich, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Proceedings
EditorsFritz Henglein, Sharon Shoham, Yakir Vizel
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages34
ISBN (Print)9783030670665
StatePublished - 2021
Event22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 - Copenhagen, Denmark
Duration: Jan 17 2021Jan 19 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12597 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Bounded environments
  • CHC solvers
  • Modular verification
  • Procedure summaries
  • Program verification


Dive into the research topics of 'Unbounded Procedure Summaries from Bounded Environments'. Together they form a unique fingerprint.

Cite this