Name
Abstract | ||
|---|---|---|
Formal verification of safety and liveness properties of systems with a dynamically changing, unbounded number of interlinked
processes and infinite-domain local data is challenging due to the two sources of infiniteness. The existing state abstraction-based
approaches Data Type Reduction and Environment Abstraction each address one aspect, but the former doesn’t support infinite-domain
local data and the latter doesn’t support links and is restricted to particular properties.
The contribution of this paper is a combination of both which is obtained by first stating them in the framework of Canonical
Abstraction. This new use of Canonical Abstraction, originally designed and used for the analysis of programs with heap-allocated
data structures, furthermore unveils a formal connection between the two rather ad-hoc techniques.
|
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-69738-1_13 | VMCAI |
Keywords | Field | DocType |
data structure,data type,formal verification | Abstraction,Computer science,Theoretical computer science,Data type,Formal verification,Liveness | Conference |
Citations | PageRank | References |
11 | 0.60 | 23 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Björn Wachter | 1 | 326 | 20.09 |
| Bernd Westphal | 2 | 77 | 6.02 |