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.
|Name||Lecture Notes in Computer Science|
|Conference||conference; 12th International Symposium on Automated Technology for Verification and Analysis; 2014-11-03; 2014-11-06|
|Period||3/11/14 → 6/11/14|
|Other||12th International Symposium on Automated Technology for Verification and Analysis|