kirancodes.me
To Proof Maintenance & Beyond!
ASE 2005

Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning

Gudmund Grov

PDFDOI 10.1145/1101908.1101995dblp

Abstract

Hume is a programming language targeted at safety-critical, resource-bounded systems. Bounded time and space usage is achieved by a clear separation of coordination and computation in the design of the language. However, there is no correctness verification. Such verification is imperative in safety-critical environments. It is our contention that the language design makes a combination of deductive and algorithmic reasoning tractable.

BibTeX
@inproceedings{Grov:ASE05,
  author    = {Gudmund Grov},
  title     = {Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning},
  booktitle = {ASE},
  pages     = {444--447},
  publisher = {{ACM}},
  year      = {2005},
}

Related papers