@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",
}