Liveness Analysis for Parameterised Boolean Equation Systems

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

doi:10.1007/978-3-319-11936-6_16

Liveness Analysis for Parameterised Boolean Equation Systems

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

Theoretical Computer Science

Research output: Contribution to Journal › Article › Academic › peer-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 language	English
Pages (from-to)	219-234
Journal	Lecture Notes in Computer Science
Volume	8837
DOIs	https://doi.org/10.1007/978-3-319-11936-6_16
Publication status	Published - 2014
Event	Automated Technology for Verification and Analysis - Duration: 1 Jan 2014 → 1 Jan 2014

Bibliographical note

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

Access to Document

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

Cite this

@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; Automated Technology for Verification and Analysis ; Conference date: 01-01-2014 Through 01-01-2014",

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",

}

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

T2 - Automated Technology for Verification and Analysis

Y2 - 1 January 2014 through 1 January 2014

ER -

Liveness Analysis for Parameterised Boolean Equation Systems

Abstract

Bibliographical note

Access to Document

Fingerprint

Cite this