7 citations · 21 across the 10 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★ 4 cited
Certified proofs in programs involving exceptions
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, e…