Skip to main content

Unbounded Procedure Summaries from Bounded Environments

Author(s): Pick, Lauren; Fedyukovich, Grigory; Gupta, Aarti

To refer to this page use:
Abstract: 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.
Publication Date: 2021
Citation: Pick, Lauren, Grigory Fedyukovich, and Aarti Gupta. "Unbounded Procedure Summaries from Bounded Environments." In International Conference on Verification, Model Checking, and Abstract Interpretation (2021): pp. 291-324. doi:10.1007/978-3-030-67067-2_14
DOI: 10.1007/978-3-030-67067-2_14
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 291 - 324
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Verification, Model Checking, and Abstract Interpretation
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.