### Abstract

Original language | English |
---|---|

Pages (from-to) | 219-234 |

Journal | Lecture Notes in Computer Science |

Volume | 8837 |

DOIs | |

Publication status | Published - 2014 |

Event | Automated Technology for Verification and Analysis - Duration: 1 Jan 2014 → 1 Jan 2014 |

### Fingerprint

### Bibliographical note

Proceedings title: ATVA 2014Publisher: Springer

ISBN: 978-3-319-11935-9

Editors: F. Cassez, J.-F. Raskin

### Cite this

*Lecture Notes in Computer Science*,

*8837*, 219-234. https://doi.org/10.1007/978-3-319-11936-6_16

}

*Lecture Notes in Computer Science*, vol. 8837, pp. 219-234. https://doi.org/10.1007/978-3-319-11936-6_16

**Liveness Analysis for Parameterised Boolean Equation Systems.** / Keiren, J.J.A.; Wesselink, J.W.; Willemse, T.A.C.

Research output: Contribution to Journal › Article › Academic › peer-review

TY - JOUR

T1 - Liveness Analysis for Parameterised Boolean Equation Systems

AU - Keiren, J.J.A.

AU - Wesselink, J.W.

AU - Willemse, T.A.C.

N1 - Proceedings title: ATVA 2014 Publisher: Springer ISBN: 978-3-319-11935-9 Editors: F. Cassez, J.-F. Raskin

PY - 2014

Y1 - 2014

N2 - We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show that a naive approach to constructing a control flow graph, needed for the analysis, may suffer from an exponential blow-up, and we define an approximate analysis that avoids this problem. The effectiveness of our techniques is evaluated using a number of case studies.

AB - We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show that a naive approach to constructing a control flow graph, needed for the analysis, may suffer from an exponential blow-up, and we define an approximate analysis that avoids this problem. The effectiveness of our techniques is evaluated using a number of case studies.

U2 - 10.1007/978-3-319-11936-6_16

DO - 10.1007/978-3-319-11936-6_16

M3 - Article

VL - 8837

SP - 219

EP - 234

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -