A while program normal form theorem in total correctness

Solin, Kim (2009). A while program normal form theorem in total correctness. In: Rudolf Berghammer, Ali Mohamed Jaoua and Bernhard Möller, Relations and Kleene Algebra in Computer Science: 11th International Conference on Relational Methods in Computer Science, RelMiCS 2009 and 6th International Conference on Applications of Kleene Algebra. Proceedings. RelMiCS 11: 11th International Conference on Relational Methods in Computer Science and AKA6: 6th International Conference on Applications of Kleene Algebra, Doha, Qatar, (322-336). 1-5 November, 2009. doi:10.1007/978-3-642-04639-1_22

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Solin, Kim
Title of paper A while program normal form theorem in total correctness
Conference name RelMiCS 11: 11th International Conference on Relational Methods in Computer Science and AKA6: 6th International Conference on Applications of Kleene Algebra
Conference location Doha, Qatar
Conference dates 1-5 November, 2009
Proceedings title Relations and Kleene Algebra in Computer Science: 11th International Conference on Relational Methods in Computer Science, RelMiCS 2009 and 6th International Conference on Applications of Kleene Algebra. Proceedings   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2009
Sub-type Fully published paper
DOI 10.1007/978-3-642-04639-1_22
Open Access Status
ISBN 9783642046384
9783642046391
ISSN 0302-9743
1611-3349
Editor Rudolf Berghammer
Ali Mohamed Jaoua
Bernhard Möller
Volume 5827
Start page 322
End page 336
Total pages 15
Chapter number 22
Total chapters 24
Language eng
Formatted Abstract/Summary
A classical while-program normal-form theorem is derived in demonic refinement algebra. In contrast to Kozen’s partial-correctness proof of the theorem in Kleene algebra with tests, the derivation in demonic refinement algebra provides a proof that the theorem holds in total correctness.
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Thu, 07 Aug 2014, 14:30:00 EST by Emma Petherick on behalf of School of Information Technol and Elec Engineering