Proof automation for functional correctness in separation logic
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 15113378
- Type
- D - Journal article
- DOI
-
10.1093/logcom/exu032
- Title of journal
- Journal of Logic and Computation
- Article number
- -
- First page
- 641
- Volume
- 26
- Issue
- 2
- ISSN
- 0955-792X
- Open access status
- Out of scope for open access requirements
- Month of publication
- May
- Year of publication
- 2014
- 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)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper presents a novel approach to verifying the correctness of pointer programs that involve iteration and recursion. The novelty of the work lies in the tight integration of program analysis (shape analysis) and automated reasoning techniques (proof planning/theorem proving). At the heart of the approach is term synthesis, a technique that enables us to automatically generate missing knowledge, i.e. preconditions, loop and frame invariants, which are typically seen as requiring user interaction. The feasibility of the work was carried out via a Platform Grant (EP/N014758/1), and subsequently developed via a responsive mode grant (second author PI on grants).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -