Name
Abstract | ||
|---|---|---|
DynAlloy is an extension of the Alloy language to better de- scribe state change via actions and programs, in the style of dynamic logic. In this paper, we report on our experience in trying to provide ab- straction based mechanisms for improving DynAlloy specifications with respect to SAT based analysis. The technique we employ is based on predicate abstraction, but due to the context in which we make use of it, is subject to the following more specific improvements: (i) since DynAl- loy's analysis consists of checking partial correctness assertions against programs, we are only interested in the initial and final states of a com- putation, and therefore we can safely abstract away some intermediate states in the computation (generally, this kind of abstraction cannot be safely applied in model checking), (ii) since DynAlloy's analysis is in- herently bounded, we can safely rely on the sole use of a SAT solver for producing the abstractions, and (iii) since DynAlloy's basic operational unit is the atomic action, which can be used in different parts within a program, we can reuse the abstraction of an action in different parts of a program, which can accelerate the convergence in checking valid properties. We present the technique via a case study based on a translation of a JML annotated Java program into DynAlloy, accompanied by some preliminary experimental results showing some of the benefits of the technique. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-88194-0_14 | IEEE International Conference on Formal Engineering Methods |
Keywords | Field | DocType |
basic operational unit,different part,alloy language,jml annotated java program,model checking,predicate abstraction,dynalloy specifications,sole use,sat solver,atomic action,towards abstraction,dynalloy specification,dynamic logic | Model checking,Abstraction,Programming language,Predicate abstraction,Computer science,Boolean satisfiability problem,Correctness,Theoretical computer science,Dynamic logic (digital electronics),Computation tree,Propositional formula | Conference |
Volume | ISSN | Citations |
5256 | 0302-9743 | 1 |
PageRank | References | Authors |
0.36 | 21 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nazareno Aguirre | 1 | 159 | 21.79 |
| Marcelo F. Frias | 2 | 295 | 35.57 |
| Pablo Ponzio | 3 | 14 | 4.92 |
| Brian J. Cardiff | 4 | 1 | 0.36 |
| Juan P. Galeotti | 5 | 166 | 9.64 |
| Germán Regis | 6 | 21 | 7.29 |