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

Gudmund Grov

doi:10.1145/1101908.1101995

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

Gudmund Grov

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005
Pages	444-447
Number of pages	4
DOIs	https://doi.org/10.1145/1101908.1101995
Publication status	Published - 2005
Event	20th IEEE International Conference on Automated Software Engineering 2005 - Long Beach, CA, United States Duration: 7 Nov 2005 → 11 Nov 2005

Conference

Conference	20th IEEE International Conference on Automated Software Engineering 2005
Abbreviated title	ASE 2005
Country/Territory	United States
City	Long Beach, CA
Period	7/11/05 → 11/11/05

Keywords

Formal methods
Formal verification
Model checking
Specification languages
Theorem proving

Access to Document

10.1145/1101908.1101995

Cite this

@inproceedings{26b55a65c5f544b4b17b02a5358cbdb5,

title = "Verifying the correctness of hume programs - An approach combining deductive and algorithmic reasoning",

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.",

keywords = "Formal methods, Formal verification, Model checking, Specification languages, Theorem proving",

author = "Gudmund Grov",

year = "2005",

doi = "10.1145/1101908.1101995",

language = "English",

isbn = "1-58113-993-4 ",

pages = "444--447",

booktitle = "Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005",

note = "20th IEEE International Conference on Automated Software Engineering 2005, ASE 2005 ; Conference date: 07-11-2005 Through 11-11-2005",

}

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, 20th IEEE International Conference on Automated Software Engineering 2005, Long Beach, CA, United States, 7/11/05. https://doi.org/10.1145/1101908.1101995

TY - GEN

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

AU - Grov, Gudmund

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

KW - Formal methods

KW - Formal verification

KW - Model checking

KW - Specification languages

KW - Theorem proving

U2 - 10.1145/1101908.1101995

DO - 10.1145/1101908.1101995

M3 - Conference contribution

SN - 1-58113-993-4

SP - 444

EP - 447

BT - Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005

T2 - 20th IEEE International Conference on Automated Software Engineering 2005

Y2 - 7 November 2005 through 11 November 2005

ER -

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

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this