Building program construction and verification tools from algebraic principles
- Submitting institution
-
The University of Sheffield
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2428
- Type
- D - Journal article
- DOI
-
10.1007/s00165-015-0343-1
- Title of journal
- Formal Aspects of Computing
- Article number
- -
- First page
- 265
- Volume
- 28
- Issue
- 2
- ISSN
- 0934-5043
- Open access status
- Out of scope for open access requirements
- Month of publication
- November
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
I - Verification
- Citation count
- 4
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Presents a novel compositional framework for designing program construction and verification tools with interactive proof assistants. Precursor won SEFM 2015 best paper award. Generalised and adapted to verify pointer programs with separation algebras, concurrent programs with rely-guarantee algebras and hybrid programs with differential dynamic algebras (doi.org/10.1007/978-3-319-19797-5_7, doi.org/10.1007/978-3-319-48989-6_19, doi.org/10.1007/978-3-319-06410-9_6, doi.org/10.1007/978-3-030-43520-2_11 and three PhD theses). Led to research collaborations with Data61 and ANU, Australia and CMU, US, and strongly influenced the design of verification tools, including Isabelle/UTP at York (e.g. https://www.sciencedirect.com/science/article/pii/S0167642320301192). Used to teach program verification to MSc students.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -