Verifying the correctness of hume programs - An approach combining deductive and algorithmic reasoning

Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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. Copyright 2005 ACM.

Original languageEnglish
Title of host publicationProceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005
Pages444-447
Number of pages4
DOIs
Publication statusPublished - 2005
Event20th IEEE International Conference on Automated Software Engineering 2005 - Long Beach, CA, United States
Duration: 7 Nov 200511 Nov 2005

Conference

Conference20th IEEE International Conference on Automated Software Engineering 2005
Abbreviated titleASE 2005
CountryUnited States
CityLong Beach, CA
Period7/11/0511/11/05

Keywords

  • Formal methods
  • Formal verification
  • Model checking
  • Specification languages
  • Theorem proving

Fingerprint Dive into the research topics of 'Verifying the correctness of hume programs - An approach combining deductive and algorithmic reasoning'. Together they form a unique fingerprint.

  • Cite this

    Grov, G. (2005). Verifying the correctness of hume programs - An approach combining deductive and algorithmic reasoning. In Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005 (pp. 444-447) https://doi.org/10.1145/1101908.1101995