Name
Abstract | ||
|---|---|---|
This paper is concerned with the synthesis of invariants in programs with arrays. More specifically, we consider properties concerning array contents up to a permutation. For instance, to prove a sorting procedure, one has to show that the result is sorted, but also that it is a permutation of the initial array. In order to analyze this kind of properties, we define an abstract interpretation working on multisets of values, and able to discover invariant equations about such multisets. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-11319-2_21 | VMCAI |
Keywords | Field | DocType |
invariant equation,initial array,abstract interpretation,array content,static analysis | Algebra,Abstract interpretation,Computer science,Static analysis,Permutation,Cyclic permutation,Algorithm,Implicit function,Theoretical computer science,Sorting,Invariant (mathematics) | Conference |
Volume | ISSN | ISBN |
5944 | 0302-9743 | 3-642-11318-4 |
Citations | PageRank | References |
5 | 0.46 | 24 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Valentin Perrelle | 1 | 5 | 0.46 |
| Nicolas Halbwachs | 2 | 3957 | 426.43 |