Liveness analysis for parameterised Boolean equation systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)

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 languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014)
EditorsF. Cassez, J.-F. Raskin
Place of PublicationBerlin
PublisherSpringer
Pages219-234
ISBN (Print)978-3-319-11935-9
DOIs
Publication statusPublished - 2014
Eventconference; 12th International Symposium on Automated Technology for Verification and Analysis; 2014-11-03; 2014-11-06 -
Duration: 3 Nov 20146 Nov 2014

Publication series

NameLecture Notes in Computer Science
Volume8837
ISSN (Print)0302-9743

Conference

Conferenceconference; 12th International Symposium on Automated Technology for Verification and Analysis; 2014-11-03; 2014-11-06
Period3/11/146/11/14
Other12th International Symposium on Automated Technology for Verification and Analysis

Fingerprint Dive into the research topics of 'Liveness analysis for parameterised Boolean equation systems'. Together they form a unique fingerprint.

  • Cite this

    Keiren, J. J. A., Wesselink, J. W., & Willemse, T. A. C. (2014). Liveness analysis for parameterised Boolean equation systems. In F. Cassez, & J-F. Raskin (Eds.), Automated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014) (pp. 219-234). (Lecture Notes in Computer Science; Vol. 8837). Berlin: Springer. https://doi.org/10.1007/978-3-319-11936-6_16