Synchronous Parallelism in the Asbru Language
Michael Balser, Wolfgang Reif, Jonathan Schmitt · 2008
In this paper we present a flexible mechanism for symbolic execution of synchronous parallel programs. The synchronous parallel operator we use allows for techniques like modular reasoning and abstraction of single components. Furthermore, symbolic execution provides intuitive proofs. The operator is included into the interactive higher order theorem prover KIV. We show how to apply our approach using the Asbru medical planning language as an example. This language decomposes medical treatments into many components, which are then executed synchronous parallel. This work is a joint work that has been partially funded by the DFG program INOPSYS II, under contract number Re 828/6-3 and the European Commission’s IST program Protocure II, under contract number IST-FP6-508794.