Name
Abstract | ||
|---|---|---|
We propose a mechanised strategy to turn an infinite CSPZ process (formed of CSP and Z constructs) into one suitable for model checking. This strategy integrates two theories which allow us to consider the infiniteness of CSPZ as two separate problems: data independence for handling the behavioural aspect and abstract interpretation for handling the data structure aspect. A distinguishing feature of our approach to abstract interpretation is the generation of the abstract domains based on a symbolic execution of the process. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-45614-7_10 | FME |
Keywords | Field | DocType |
distinguishing feature,abstract domain,Mechanical Abstraction,model checking,abstract interpretation,infinite CSPZ process,data structure aspect,behavioural aspect,CSPZ Processes,data independence,Z construct,mechanised strategy | Constraint satisfaction,Data structure,Abstraction,Programming language,Model checking,Computer science,Abstract interpretation,Theoretical computer science,Symbolic execution,Group method of data handling,Data independence | Conference |
ISBN | Citations | PageRank |
3-540-43928-5 | 2 | 0.41 |
References | Authors | |
17 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexandre Cabral Mota | 1 | 199 | 18.27 |
| Paulo Borba | 2 | 1088 | 68.71 |
| Augusto Sampaio | 3 | 30 | 5.48 |