Analyzing spreadsheets for parallel execution via model checking
| Autor: | Marco Muñiz, Lone Leth Thomsen, Bent Thomsen, Thomas Bøgholm, Kim Guldstrand Larsen |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: | |
| Zdroj: | Bøgholm, T, Larsen, K G, Muniz, M, Thomsen, B & Thomsen, L L 2019, Analyzing spreadsheets for parallel execution via model checking . in Models, Mindsets, Meta: The What, the How, and the Why Not? . Springer, Lecture Notes in Computer Science, vol. 11200, pp. 27-35 . https://doi.org/10.1007/978-3-030-22348-9_3 Lecture Notes in Computer Science ISBN: 9783030223472 Models, Mindsets, Meta |
| DOI: | 10.1007/978-3-030-22348-9_3 |
| Popis: | In this paper we briefly report on work in the Popular Parallel Programming (P3) project where we follow in the footsteps of Bernhard Steffen using the idea of program analysis via model checking and abstract interpretation. The programs we analyze are spreadsheet programs, which for long have been identified as an ideal programming model for parallel execution. We translate spreadsheet programs into Timed Automata Models, which may be analyzed by the Uppaal model checker and its derivatives, with the purpose of finding schedules for parallel execution. In this paper we mainly focus on the techniques and scalability issues of various variants of Uppaal, but also report briefly on the performance results achieved through the parallelization. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|