Modular set-based analysis from contracts

Philippe Meunier*, Robert Bruce Findler, Matthias Felleisen

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

9 Scopus citations


In PLT Scheme, programs consist of modules with contracts. The latter describe the inputs and outputs of functions and objects via predicates. A run-time system enforces these predicates; if a predicate fails, the enforcer raises an exception that blames a specific module with an explanation of the fault. In this paper, we show how to use such module contracts to turn set-based analysis into a fully modular parameterized analysis. Using this analysis, a static debugger can indicate for any given contract check whether the corresponding predicate is always satisfied, partially satisfied, or (potentially) completely violated. The static debugger can also predict the source of potential errors, i.e., it is sound with respect to the blame assignment of the contract system.

Original languageEnglish (US)
Pages (from-to)218-231
Number of pages14
JournalACM SIGPLAN Notices
Issue number1
StatePublished - 2006


  • Modular Analysis
  • Runtime Contracts
  • Set-based Analysis
  • Static Debugging

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'Modular set-based analysis from contracts'. Together they form a unique fingerprint.

Cite this