Stream: Coq users

Topic: Program verification using Hoare Logic


view this post on Zulip João Mendes (Mar 21 2024 at 16:46):

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

view this post on Zulip Guillaume Melquiond (Mar 21 2024 at 16:52):

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

view this post on Zulip Karl Palmskog (Mar 21 2024 at 16:58):

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

view this post on Zulip Karl Palmskog (Mar 21 2024 at 17:03):

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

view this post on Zulip João Mendes (Mar 21 2024 at 18:13):

Many thanks for the tips! :wink:


Last updated: Jun 22 2024 at 16:02 UTC