Name
Abstract | ||
|---|---|---|
Symbolic data structures such as Decision Diagrams have proved successful for model-checking. For high-level specifications such as those used in programming languages, especially when manipulating pointers or arrays, building and evaluating the transition is a challenging problem that limits wider applicability of symbolic methods. We propose a new symbolic algorithm, EquivSplit, allowing an efficient and fully symbolic manipulation of transition relations on Data Decision Diagrams. It allows to work with equivalence classes of states rather than individual states. Experimental evidence on the concurrent software oriented benchmark BEEM shows that this approach is competitive. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-39799-8_58 | CAV |
Keywords | Field | DocType |
decision diagrams,concurrent software,symbolic method,benchmark beem,transition relation,data decision diagrams,challenging problem,symbolic data structure,decision diagram,symbolic manipulation,new symbolic algorithm | Data structure,Pointer (computer programming),Model checking,Programming language,Computer science,Binary decision diagram,Algorithm,Symbolic computation,Theoretical computer science,Software,Symbolic data analysis,Symbolic trajectory evaluation | Conference |
Citations | PageRank | References |
7 | 0.61 | 10 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maximilien Colange | 1 | 42 | 5.94 |
| Souheib Baarir | 2 | 35 | 10.01 |
| Fabrice Kordon | 3 | 603 | 61.72 |
| Yann Thierry-Mieg | 4 | 225 | 18.17 |