Analyzing recursive programs using a fixed-point calculus

Salvatore La Torre, P. Madhusudan, Gennaro Parlato

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

Abstract

We show that recursive programs where variables range over finite domains can be effectively and efficiently analyzed by describing the analysis algorithm using a formula in a fixed-point calculus. In contrast with programming in traditional languages, a fixed-point calculus serves as a high-level programming language to easily, correctly, and succinctly describe model-checking algorithms. While there have been declarative high-level formalisms that have been proposed earlier for analysis problems (e.g., Datalog), the fixed-point calculus we propose has the salient feature that it also allows algorithmic aspects to be specified. We exhibit two classes of algorithms of symbolic (BDD-based) algorithms written using this framework - one for checking for errors in sequential recursive Boolean programs, and the other to check for errors reachable within a bounded number of context-switches in a concurrent recursive Boolean program. Our formal-ization of these otherwise complex algorithms is extremely simple, and spans just a page of fixed-point formulae. Moreover, we implement these algorithms in a tool called GETAFIX which expresses algorithms as fixed-point formulae and evaluates them efficiently using a symbolic fixed-point solver called MUCKE. The resulting model-checking tools are surprisingly efficient and are competitive in performance with mature existing tools that have been fine-tuned for these problems.

Original languageEnglish (US)
Title of host publicationPLDI'09 - Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages211-222
Number of pages12
DOIs
StatePublished - Nov 30 2009
Event2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'09 - Dublin, Ireland
Duration: Jun 15 2009Jun 20 2009

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'09
CountryIreland
CityDublin
Period6/15/096/20/09

Keywords

  • Abstraction
  • Logic
  • Model-checking
  • Recursive systems
  • Software verification
  • μ-calculus

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Analyzing recursive programs using a fixed-point calculus'. Together they form a unique fingerprint.

  • Cite this

    La Torre, S., Madhusudan, P., & Parlato, G. (2009). Analyzing recursive programs using a fixed-point calculus. In PLDI'09 - Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 211-222). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/1542476.1542500