Monahan, Rosemary and O'Donoghue, Diarmuid (2012) Case Based Specifications – reusing specifications, programs and proofs. Dagstuhl Reports, 2 (7). pp. 20-21. ISSN 2192-5283
Available under License Creative Commons Attribution Non-commercial Share Alike.
Download (54kB)
Abstract
Many software verification tools use the design-by-contract approach to annotate programs
with assertions so that tools, such as compilers, can generate the proof obligations required
to verify that a program satisfies its specification. Theorem provers and SMT solvers are
then used to, often automatically, discharge the proof obligations that have been generated.
| Item Type: | Article |
|---|---|
| Keywords: | Case Based Specifications; reusing specifications; programs and proofs; |
| Academic Unit: | Faculty of Science and Engineering > Computer Science |
| Item ID: | 4498 |
| Depositing User: | Dr. Diarmuid O'Donoghue |
| Date Deposited: | 16 Sep 2013 15:37 |
| Journal or Publication Title: | Dagstuhl Reports |
| Publisher: | Schloss Dagstuhl |
| Refereed: | Yes |
| Related URLs: | |
| Use Licence: | This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here |
Downloads
Downloads per month over past year
Share and Export
Share and Export