CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishThe precise computation of abstractions is a bottleneck in many approaches to CEGAR-based verification. In this paper, we propose a novel approach, based on the use of structural information. Rather than computing the abstraction as a single, monolithic quantification, we provide a \emph{structure-aware} abstraction algorithm, based on two complementary steps. The first, high-level step exploits the structure of the system, and partitions the abstraction problem into the combination of several smaller abstraction problems. This is represented as a formula with quantifiers. The second, low-level step exploits the structure of the formula, in particular the occurrence of variables within the quantifiers, and applies a set of low-level rewriting rules aiming at further reducing the scope of quantifiers. We experimentally evaluate the approach on a substantial set of benchmarks, and show significant speed ups compared to monolithic abstraction algorithms.
| Titolo: | Structure-Aware Computation of Predicate Abstraction |
| Autori: | |
| Data di pubblicazione: | 2009 |
| Abstract: | The precise computation of abstractions is a bottleneck in many approaches to CEGAR-based verification. In this paper, we propose a novel approach, based on the use of structural information. Rather than computing the abstraction as a single, monolithic quantification, we provide a \emph{structure-aware} abstraction algorithm, based on two complementary steps. The first, high-level step exploits the structure of the system, and partitions the abstraction problem into the combination of several smaller abstraction problems. This is represented as a formula with quantifiers. The second, low-level step exploits the structure of the formula, in particular the occurrence of variables within the quantifiers, and applies a set of low-level rewriting rules aiming at further reducing the scope of quantifiers. We experimentally evaluate the approach on a substantial set of benchmarks, and show significant speed ups compared to monolithic abstraction algorithms. |
| Handle: | http://hdl.handle.net/11582/4980 |
| ISBN: | 9781424449668 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11582/4980
Copyright © 2021