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
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 |
URI: | |
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 |
Repository Staff Only(login required)
Item control page |
Downloads
Downloads per month over past year