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 | |
Publication status | Published - 2014 |
Event | Automated Technology for Verification and Analysis - Duration: 1 Jan 2014 → 1 Jan 2014 |
Bibliographical note
Proceedings title: ATVA 2014Publisher: Springer
ISBN: 978-3-319-11935-9
Editors: F. Cassez, J.-F. Raskin