coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Li-yao Xia <lysxia AT gmail.com>
To: Lessness Randomness <lessnessr AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] [Newbie question about CompCert]
Date: Tue, 9 Jan 2018 15:44:09 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f177.google.com
Ironport-phdr: 9a23:QqYxLxH4OnI1U/+mrDafOp1GYnF86YWxBRYc798ds5kLTJ7zpsiwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95MWSJfDIOyb4gBAeQPMulXrYbyu1QAoACiBQSuHu7j1iNEi3H00KA8zu8vERvG3AslH98WtnrUrcz5NacIXuCy0aLHzDTDYOlL0jr67IjJcgshoP6NXb1qasfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFuW+Wvi2s9pAFwpDii3t8sipPIhoIT1l/L6zl5wIEzJdGiVkF0fMOkHZ1NvC+ZL4t7Wt0uT31stSogybALuYS3cDUUxJkk3RLTdv6KfoqQ7h/gSuqdOyl0iGxldb6lmRq+7VSsxvfyW8S31ltBszBLncPWtn8X0hze8siHReV5/kemwTuP0hrc6uBAIUwtm6vbMYItzqc+lpYOs0nOHDX6mErxjK+ReUUk/van5/77bbXho5+QL450igfgPaQygsGzH/g0PwwUU2WY+emwzqDv8VP6TblQk/E7kKvUvIjfJcsBp665BwFV0pwk6xa6Fzqm1NQZnWIILVJEYh2KlIfpO1TUL/D5CfezmUijkDBux/zeJL3uHo3NLmTfkLfmZbty90lcyBMqwd9D45JUF6oOLenoWk7xsdzYFgU2Pxa1w+bhEtV915kRVXiBAq+DY+vutgqs6/k0JeSXf8cvsTDxLP0j6uX1xSs9lEQGe6SyxoE/Z3WxH/AgKEKcNynCmNAEREML+xs3S6TaiVTKBTpCfGazVooz4zg6DMStCoKVFdPlu6CIwCruRs4eXWtBEF3ZVC6wL4g=

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