Sciweavers

Share
PLDI
2009
ACM

Analyzing recursive programs using a fixed-point calculus

10 years 2 months ago
Analyzing recursive programs using a fixed-point calculus
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 fixedpoint 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 contextswitches in a concurrent recursive Boolean program. Our formalization of these otherwise complex algorith...
Salvatore La Torre, Parthasarathy Madhusudan, Genn
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where PLDI
Authors Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato
Comments (0)
books