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...

• Type: Conference
• Year: 2009
• Where: PLDI
• Authors: Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato
• Keywords: Algorithms, PLDI 2009, Programming Languages, Recursive Boolean Program, fixed-point Calculus