TY - GEN

T1 - Analyzing recursive programs using a fixed-point calculus

AU - La Torre, Salvatore

AU - Madhusudan, P.

AU - Parlato, Gennaro

PY - 2009

Y1 - 2009

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

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

KW - Abstraction

KW - Logic

KW - Model-checking

KW - Recursive systems

KW - Software verification

KW - μ-calculus

UR - http://www.scopus.com/inward/record.url?scp=70450260585&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70450260585&partnerID=8YFLogxK

U2 - 10.1145/1542476.1542500

DO - 10.1145/1542476.1542500

M3 - Conference contribution

AN - SCOPUS:70450260585

SN - 9781605583921

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 211

EP - 222

BT - PLDI'09 - Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation

T2 - 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'09

Y2 - 15 June 2009 through 20 June 2009

ER -