Abstract
Source code accompanying the paper:
Naus, N., Steenvoorden, T.J. & Klinik, M.A.A. (2019). A symbolic execution semantics for TopHat. In J. Stutterheim (Ed.), IFL'19: The 31st Symposium on Implementationand Application of Functional Languages, National University of Singapore, 25th – 27th September 2019 (pp. 15-44). S.l.: ACM
DESCRIPTION
This repo contains a symbolic execution engine for [TopHat](https://github.com/timjs/tophat),
a formalisation of Task-Oriented Programming.
The code here is a deep embedding of the entire TopHat language,
including the underlying lambda calculus,
on which TopHat is built.
CONTENTS
- src: contains the source code of symbolic TopHat
- package.yaml, stack.yaml: project files for compiling with stack
- test: output of the Flight and Tax test workflows, see the paper for
documentation on them.
- More information on how to compile and run this program can be found in README.txt
SHORT SUMMARY
Task-Oriented Programming (TOP) is a programming paradigm that allows declarative specification of workflows. TOP is typically used in domains where functional correctness is essential, and where failure can have financial or strategical consequences. In this paper we aim to make formal verification of software written in TOP easier. Currently, only testing is used to verify that programs behave as intended. We use symbolic execution to guarantee that no aberrant behaviour can occur. In previous work we presented TopHat, a formal language that implements the core aspects of TOP. In this paper we develop a symbolic execution semantics for TopHat. Symbolic execution allows to prove that a given property holds for all possible execution paths of TopHat programs.
We show that the symbolic execution semantics is consistent with the original TopHat semantics, by proving soundness and completeness. We present an implementation of the symbolic execution semantics in Haskell. By running example programs, we validate our approach. This work represents a step forward in the formal verification of TOP software.
