Synchronous Parallelism in the Asbru Language

Proving Linearizability with Temporal Logic

erschienen 10.12.2008 in: Universität Augsburg, Technical Report 2008-11 Technical Report, Institute of Computer Science, University of Augsburg, December 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.

Downloads:

• technicalReport_asbruParallelSynchron_2008-11  -  (technicalReport_asbruParallelSynchron_2008-11.pdf, 0 KB)