Liveness Analysis for Parameterised Boolean Equation Systems

J.J.A. Keiren, J.W. Wesselink, T.A.C. Willemse

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)219-234
JournalLecture Notes in Computer Science
Volume8837
DOIs
Publication statusPublished - 2014
EventAutomated Technology for Verification and Analysis -
Duration: 1 Jan 20141 Jan 2014

Fingerprint

Flow graphs
Liveness
Flow Graphs
Static analysis
Explosions
Fixed-point Equation
Acoustic waves
Static Analysis
First-order Logic
Explosion
Blow-up
Eliminate

Bibliographical note

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

Cite this

Keiren, J.J.A. ; Wesselink, J.W. ; Willemse, T.A.C. / Liveness Analysis for Parameterised Boolean Equation Systems. In: Lecture Notes in Computer Science. 2014 ; Vol. 8837. pp. 219-234.
@article{28bcb58dc02543548c5a0acec372cab5,
title = "Liveness Analysis for Parameterised Boolean Equation Systems",
abstract = "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.",
author = "J.J.A. Keiren and J.W. Wesselink and T.A.C. Willemse",
note = "Proceedings title: ATVA 2014 Publisher: Springer ISBN: 978-3-319-11935-9 Editors: F. Cassez, J.-F. Raskin",
year = "2014",
doi = "10.1007/978-3-319-11936-6_16",
language = "English",
volume = "8837",
pages = "219--234",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

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

In: Lecture Notes in Computer Science, Vol. 8837, 2014, p. 219-234.

Research output: Contribution to JournalArticleAcademicpeer-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 -