Abstract

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.

Original languageEnglish
Title of host publicationModels, Mindsets, Meta: The What, the How, and the Why Not?
Number of pages9
PublisherSpringer
Publication date2019
Pages27-35
ISBN (Print)978-3-030-22347-2
ISBN (Electronic)978-3-030-22348-9
DOIs
Publication statusPublished - 2019
SeriesLecture Notes in Computer Science
Volume11200
ISSN0302-9743

Fingerprint

Spreadsheets
Model checking
Parallel programming
Scalability
Derivatives

Cite this

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? (pp. 27-35). Springer. Lecture Notes in Computer Science, Vol.. 11200 https://doi.org/10.1007/978-3-030-22348-9_3
Bøgholm, Thomas ; Larsen, Kim Guldstrand ; Muniz, Marco ; Thomsen, Bent ; Thomsen, Lone Leth. / Analyzing spreadsheets for parallel execution via model checking. Models, Mindsets, Meta: The What, the How, and the Why Not?. Springer, 2019. pp. 27-35 (Lecture Notes in Computer Science, Vol. 11200).
@inbook{57efc9b4b21240ec8e17505c2fb2151f,
title = "Analyzing spreadsheets for parallel execution via model checking",
abstract = "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.",
author = "Thomas B{\o}gholm and Larsen, {Kim Guldstrand} and Marco Muniz and Bent Thomsen and Thomsen, {Lone Leth}",
year = "2019",
doi = "10.1007/978-3-030-22348-9_3",
language = "English",
isbn = "978-3-030-22347-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "27--35",
booktitle = "Models, Mindsets, Meta: The What, the How, and the Why Not?",
address = "Germany",

}

Bøgholm, T, Larsen, KG, Muniz, M, Thomsen, B & Thomsen, LL 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

Analyzing spreadsheets for parallel execution via model checking. / Bøgholm, Thomas; Larsen, Kim Guldstrand; Muniz, Marco; Thomsen, Bent; Thomsen, Lone Leth.

Models, Mindsets, Meta: The What, the How, and the Why Not?. Springer, 2019. p. 27-35 (Lecture Notes in Computer Science, Vol. 11200).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

TY - CHAP

T1 - Analyzing spreadsheets for parallel execution via model checking

AU - Bøgholm, Thomas

AU - Larsen, Kim Guldstrand

AU - Muniz, Marco

AU - Thomsen, Bent

AU - Thomsen, Lone Leth

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-22348-9_3

DO - 10.1007/978-3-030-22348-9_3

M3 - Book chapter

SN - 978-3-030-22347-2

T3 - Lecture Notes in Computer Science

SP - 27

EP - 35

BT - Models, Mindsets, Meta: The What, the How, and the Why Not?

PB - Springer

ER -

Bøgholm T, Larsen KG, Muniz M, Thomsen B, Thomsen LL. Analyzing spreadsheets for parallel execution via model checking. In Models, Mindsets, Meta: The What, the How, and the Why Not?. Springer. 2019. p. 27-35. (Lecture Notes in Computer Science, Vol. 11200). https://doi.org/10.1007/978-3-030-22348-9_3