TY - GEN
T1 - Analyzing recursive programs using a fixed-point calculus
AU - La Torre, Salvatore
AU - Madhusudan, P.
AU - Parlato, Gennaro
N1 - ★ This research was supported NSF Grants CSR-EHCS(CPS)-0834810 and CNS-0917375. Sam Owre commented on earlier drafts of the paper, and the participants at the 2010 Workshop on Rewriting Logic and Applications, particularly José Meseguer and Peter Ölveczky, offered valuable feedback and advice.
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 -