40 citations · 142 across the 19 of their papers we have counts for
Showing 2013Show all
2 papers · 1 filter
cs.LO2013★ 4 cited
Formal verification in Coq of program properties involving the global state effect
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
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 verific…
cs.LO2013★ 7 cited
Kleene Algebra with Tests and Coq Tools for While Programs
Damien Pous
We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equationa…