Analyzing spreadsheets for parallel execution via model checking

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

2 Citations (Scopus)


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
Publication date2019
ISBN (Print)978-3-030-22347-2
ISBN (Electronic)978-3-030-22348-9
Publication statusPublished - 2019
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Analyzing spreadsheets for parallel execution via model checking'. Together they form a unique fingerprint.

Cite this