coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Newbie question about CompCert]

From: Lessness Randomness <lessnessr AT gmail.com>
To: Li-yao Xia <lysxia AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] [Newbie question about CompCert]
Date: Tue, 9 Jan 2018 23:27:12 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lessnessr AT gmail.com; spf=Pass smtp.mailfrom=lessnessr AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f180.google.com
Ironport-phdr: 9a23:BWF3aRTl2Lc65G2oxM5NZvAH59psv+yvbD5Q0YIujvd0So/mwa69bByN2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/2PZisJwgqxVow+vqQJjzIPPeo6ZKOBzc7nBcd8GR2dMWNtaWSxbAoO7aosCF+wPMvhDr4nmoVsBswC+BRKxD+3z0DBIgGL53ao/0+QnDw7GxxcgFM8JvXTQstr1L7wSUearw6nT1jXDdehb2Tj46IfScxAhpeuAUq53ccrU0EQiER7OgFuXqYzgJTyV1+INvnCD7+p6VOKvjXIopB9tojiowMcgkJfGiZ8Iyl3C6C53w541KMWmREJnZdOoCphduiGAO4drXM8vQHtktDs5x7Eav5OwYTIEx449xxHFbvyKa4iI7QznVOaWOTp4gWhqeLO7hxqr/0mg0PHwWtC60FpXrSdJjsPAtn8K1xzU5ciHTuVy8l291jaI0gDf8uBEIUYqmqrHM5Mt3KI8m54JvUnAHiL6glj6gLGVe0k+5+Sl6Pjrbq3jppCGNo90jg/+Mr4pmsy6Gek4NhYBX3OA+eS6yrLj5lb5QK9Rg/05l6nWqpHaJcABqqGlBA9V154v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4MdwC/QQKfW7ak74/IjcHwQpMgWczOPuCdE73YQbDybHCaiAdajWrFWg5+Q1IuDKapVGliz6Lq0B6uX1i3IighcndK+l2p4RZWujVqBiLl6CZ3f3mc0pHmIDvw54R+vv3g7RGQVPbmq/CvpvrgowD5irWN/O

Big thank you for the pointer!

2018-01-09 22:44 GMT+02:00 Li-yao Xia <lysxia AT gmail.com>:

On 01/09/2018 03:21 PM, Lessness Randomness wrote:

Is it possible (using CompCert library in Coq, its formalisation of the C) to specify and prove properties of C functions?

That's exactly what the Verified Software Toolchain is for! (It's connected to Compcert.)

http://vst.cs.princeton.edu

Li-yao

[Coq-Club] [Newbie question about CompCert], Lessness Randomness, 01/09/2018
- Re: [Coq-Club] [Newbie question about CompCert], Li-yao Xia, 01/09/2018
  - Re: [Coq-Club] [Newbie question about CompCert], Lessness Randomness, 01/09/2018