### 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 language | English (US) |
---|---|

Title of host publication | PLDI'09 - Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation |

Pages | 211-222 |

Number of pages | 12 |

DOIs | |

State | Published - Nov 30 2009 |

Event | 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'09 - Dublin, Ireland Duration: Jun 15 2009 → Jun 20 2009 |

### Publication series

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

### Other

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

Country | Ireland |

City | Dublin |

Period | 6/15/09 → 6/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

*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