I need to verify the correctness of a program and I'd like to this with Coq. As a beginner in the topic, I've read the chapters of Softwares Foundations vol2 about Hoare Logic. In the provided implementation, the only mechanism to store value are variables. Is there a similar implementation in Coq that has arrays or even more complex abstract datatypes?

The decision to tackle this task using Coq is just because I have a tight deadline to meed and Coq is something I am familiar with. Any other recommendation of literature and technologies are welcome

I am biased, but I suggest Why3: https://www.why3.org/doc/whyml.html

the other more heavyweight option is arguably VST (C programs), one example of applying VST here

another option purely inside Coq: https://github.com/imdea-software/htt

Many thanks for the tips! :wink:

Last updated: Jun 22 2024 at 16:02 UTC