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
}
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 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 -