Towards Distributed Software Model-Checking using Decision Diagrams
| Autor: | Fabrice Kordon, Souheib Baarir, Maximilien Colange, Yann Thierry-Mieg |
|---|---|
| Přispěvatelé: | Modélisation et Vérification (MoVe), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2013 |
| Předmět: |
Model checking
Theoretical computer science Computer science business.industry Programming language Binary decision diagram 0102 computer and information sciences 02 engineering and technology Data structure Symbolic computation computer.software_genre 01 natural sciences Symbolic data analysis Software 010201 computation theory & mathematics Symbolic trajectory evaluation 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO]Computer Science [cs] business Equivalence class computer |
| Zdroj: | 25th International Conference on Computer Aided Verification (CAV) 25th International Conference on Computer Aided Verification (CAV), Jul 2013, Saint-Petersbourg, Russia. pp.830-845, ⟨10.1007/978-3-642-39799-8_58⟩ Computer Aided Verification ISBN: 9783642397981 CAV |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|