coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is there a VST mailing list/chat?

From: Nika Pona <npona AT codeminders.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Is there a VST mailing list/chat?
Date: Mon, 11 Jan 2021 19:01:20 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=npona AT codeminders.com; spf=Pass smtp.mailfrom=npona AT codeminders.com; spf=None smtp.helo=postmaster AT mail-wm1-f44.google.com
Ironport-phdr: 9a23:q/xJRxP5tCDROXEKy/cl6mtUPXoX/o7sNwtQ0KIMzox0LfT+rarrMEGX3/hxlliBBdydt6sbzbCL6uuxByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+Ngu6oAXMusUZhYZvK7s6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZoga1UoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VoZH8p1sNtxS1GBOiBOTpyjBSm3T72qs60/wmEQHAxgMtBM4BsHPJo9rrMacSUOa1w7TWwjXZdPNawyvy6I/Nch04p/yHQL1/f9bLx0Y1CwPFkkufqZbjPz6Ny+kDvGiW4uRkWO+vi2AqqB99rzyyy8kil4TEm4AYxF/L+yh63Ys4Id+1RkFnbdOmEJZdtCWXOpZ1T80sQmxmtyA3waAFt56jZCUG1ogryhrFZ/GEc4WE+A/vWPiSLDtii39od7SyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTvtx50mg2TOS2wzK5OFJLk85mbDUK54mxb4wmZ4TvlrZEiDqn0X2ibeadkQi+ue29+TqeqvqqoOYOoNuiQzzMr4iltGhDek7KAQDUGeW9fy51LL5/E35RLtKjucxkqncqJ3aI9wbpqm/AwBPyYss9xG/ACq439QdnHkHKk9Kdwydj4jyIV3BPPf4DfKnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaCaiAdajWrFWg5+Q1IuDKapVGliz6Lq0D5v3nxUc+n1ZVKa+x2p0eQHu/EvljIkOVbGD3xNwGFDFZ7UIFUOX2hQjaAnZobHGoUvdkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkZWFuLHXrtdoOIVu0XLimVJ504y2FWZf2aU4YkkCqWmkr6xr5gdLeG/yQZsdf80YEw6bGP0x418jNwAoKW1GTfFzgozFNNfCc/2eVEmWI40k2KiPcqiPtUGNlS4f9ESBx8PpnZnbR3

Hi all,

I've been working with VST for a year now and I was wondering if there was a way to communicate with VST developers and users, similar to coq-club. Stackoverflow verifiable-c tag is not very active, github issues are not always appropriate.

For instance, I am not sure how to prove this:

Lemma forall a, valid_pointer a |-- weak_valid_pointer (offset_val 1 a)). Any hints?

Best,

Nika

[Coq-Club] Is there a VST mailing list/chat?, Nika Pona, 01/11/2021
- Re: [Coq-Club] Is there a VST mailing list/chat?, Yixuan Chen, 01/11/2021
  - Re: [Coq-Club] Is there a VST mailing list/chat?, Nika Pona, 01/11/2021