Formal verification in Coq of program properties involving the global state effect

JFLA, pp. 1-16, 2014.

Cited by: 10|Bibtex|Views2|Links
EI
Keywords:
denotational semantics

Abstract:

The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verification in Coq of properties of programs manipulating the global state effect. These properties are expressed in a proof system which is close to the syntax, as i...More

Code:

Data:

Your rating :
0

 

Tags
Comments