Dear Spiral user, We’re pleased to introduce Helix, https://helix.imperial.ac.uk/ Imperial’s new repository for research datasets. Please use Helix for all future dataset deposits. There is no change to Spiral -continue depositing as usual. For queries, contact the Research Data Management team at rdm-enquiries@imperial.ac.uk. Kind regards, the Spiral Team.
 
Holisitic specifications for robust programs - Coq model
Author(s)
Drossopoulou, Sophia
Noble, James
Mackay, Julian
Eisenbach, Susan
Type
Software / Code
Abstract
A Coq formalism of the core of the Chainmail specification language, along with an underlying language, Loo.

This Coq formalism has been developed as part of the associated paper: Holistic Specifications for Robust Programs (https://arxiv.org/abs/2002.08334), to be published at FASE 2020
Version
1
Date Issued
2020-02-21
Citation
2020
URI
DOI
Copyright Statement
https://creativecommons.org/licenses/by/4.0/legalcode
Subjects
Programming Languages
Software Verification
Programming Language Semantics