Liveness analysis for parameterised Boolean equation systems

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

9 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