@inproceedings{2b8d4097e2ab4707b5fb110178b06885,
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",
year = "2014",
doi = "10.1007/978-3-319-11936-6_16",
language = "English",
isbn = "978-3-319-11935-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "219--234",
editor = "F. Cassez and J.-F. Raskin",
booktitle = "Automated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014)",
address = "Germany",
note = "conference; 12th International Symposium on Automated Technology for Verification and Analysis; 2014-11-03; 2014-11-06 ; Conference date: 03-11-2014 Through 06-11-2014",
}