You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Southampton » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Southampton

Return to search Previous output Next output

Output 0 of 0 in the submission

Output title

Analyzing recursive programs using a fixed-point calculus

Type

E - Conference contribution

DOI

10.1145/1543135.1542500

Name of conference/published proceedings

PLDI '09. Proceedings of the 2009 ACM SIGPLAN conference on Programming Language Design and Implementation

Volume number

Issue number

First page of article

211

ISSN of proceedings

Year of publication

2009

URL

http://www.eprints.soton.ac.uk/272457

Number of additional authors

Additional information

Significance of output:

<11>This paper proposes the first declarative framework, Getafix, that easies the development of model-checkers for sequential/concurrent programs based on fixedpoint calculus. Algorithms are defined through a high-level formalism that also allows specification of algorithmic aspects. Within this framework, we develop several model checkers for sequential and concurrent Boolean programs, using a BDD fixed-point engine as backend. This enables building model-checkers that are competitive with state-of-the-art tools. Getafix is the precursor of modern model checkers for general programs built on top of fixed-point engines such as QARMC (TU Munich-Germany), Eldarica (EPFL-Swiss), and Z3-fixedpoints (Microsoft research).

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract