Liveness analysis for parameterised Boolean equation systems

Autor:	Keiren, J.J.A., Wesselink, J.W., Willemse, T.A.C., Cassez, F., Raskin, J.-F.
Přispěvatelé:	Formal System Analysis
Jazyk:	angličtina
Rok vydání:	2014
Předmět:	Discrete mathematics symbols.namesake Recursion Computer science Liveness symbols Applied mathematics Control flow graph Combinatorial explosion Boolean algebra Exponential function
Zdroj:	Automated Technology for Verification and Analysis ISBN: 9783319119359 ATVA Automated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014), 219-234 STARTPAGE=219;ENDPAGE=234;TITLE=Automated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014)
ISSN:	0302-9743
DOI:	10.1007/978-3-319-11936-6_16
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7701c4dda9cf58f18d834466310f27cd https://doi.org/10.1007/978-3-319-11936-6_16 Zobrazit plný text záznamu