Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
2013 (English)In: Interactive Theorem Proving: ITP 2013, Springer Berlin/Heidelberg, 2013, 197-212 p.Conference paper, Published paper (Refereed)
Abstract [en]

Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while-programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2013. 197-212 p.
Series
Lecture Notes in Computer Science, 7998
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-207378DOI: 10.1007/978-3-642-39634-2_16ISBN: 978-3-642-39633-5 (print)OAI: oai:DiVA.org:uu-207378DiVA: diva2:647919
Conference
4th International Conference on Interactive Theorem Proving (ITP); Rennes, France; July 22-26, 2013
Available from: 2013-09-12 Created: 2013-09-12 Last updated: 2013-09-13Bibliographically approved

Open Access in DiVA

fulltext(682 kB)234 downloads
File information
File name FULLTEXT01.pdfFile size 682 kBChecksum SHA-512
18c17c684d89bd6f8cac6e2ca0525fe0cc1ee61e87f5b79838bce3012afa927044fbe43f79c6c11d88a2ab677832cc06b287ae35aec4d57691ebe4f147fbbe98
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Weber, Tjark
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 234 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 498 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf