Data · dataset · 2020
Source code for the symbolic TopHat execution engine
Listed in DANS Data Station Physical and Technical Sciences
Source code accompanying the paper: Naus, N., Steenvoorden, T.J. & Klinik, M.A.A. (2019).
Description
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, 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.
Read the rest (4 more)
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.
Links
Where it is published
- Dataverse dataset page phys-techsciences.datastations.nl/dataset.xhtml?persistentId=doi%3A10.17026%2FDANS-ZUB-XAC3 ↗
landing page · from phys techsciences datastations nl
- DOI doi.org/10.17026/dans-zub-xac3 ↗
DOI / persistent id · from phys techsciences datastations nl
Catalogue records · 1
- Dataverse API phys-techsciences.datastations.nl/api/datasets/:persistentId/?persistentId=doi%3A10.17026%2FDANS… ↗
metadata API · from phys techsciences datastations nl
Topics
- Stated by source
- Computer and Information Science
- Inferred from text
- Software engineering 75%
Provenance · 1 source records, 8 field assertions
| Source | Key | Last seen | Raw |
|---|---|---|---|
| DANS Data Station Physical and Technical Sciences | doi:10.17026/DANS-ZUB-XAC3 | 11 d ago | JSON v1 |
| Field | Assertion | Extractor | Evidence |
|---|---|---|---|
| concepts[field].anzsrc:group:4612 | enrichment · phys techsciences datastations nl | taxonomy-embedding@1.1.0 | title+keywords+description (75%) |
| concepts[field].dataverse_subject:computer-and-information-science | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 | /subjects |
| created_date | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 | |
| description | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 | /description |
| publication_date | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 | |
| title | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 | /name |
| updated_date | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 | |
| version_label | source · phys techsciences datastations nl | connector:phys_techsciences_datastations_nl@1.0.0 |