From: "Dan'l Miller" <optikos@verizon.net>
Subject: Re: Why not Coq2Ada program extraction?
Date: Mon, 7 May 2018 06:27:53 -0700 (PDT)
Date: 2018-05-07T06:27:53-07:00 [thread overview]
Message-ID: <121e759d-610e-4adb-8a9c-3b7269198d60@googlegroups.com> (raw)
In-Reply-To: <bf355b31-b3d2-4fe2-826d-f27cb7b59a49@googlegroups.com>
On Sunday, May 6, 2018 at 9:30:14 PM UTC-5, Dan'l Miller wrote:
> As it turns out Coq isn't the only one to have made progress in program-verification-based/proof-based decompilation/reverse-engineering of machine code. Isabelle/HOL (i.e., HOL4, based on more-recognizable[-to-people-who've-studied-symbolic-logic] garden-variety higher-order logic) is at somewhat the same era of progress on that topic of producing interesting results taking machine-code on a variety of ISAs as input:
> https://acjf3.github.io//papers/itp15.pdf
For those readers who are casually following along with these threads about theorem provers as potential correctness verifiers for Ada in the future:
Q: What is that Hoare-triple stuff in the HOL4 machine-code verification? A: Here is an introduction:
http://www.cl.cam.ac.uk/%7Emom22/arm-hoare-logic.pdf
prev parent reply other threads:[~2018-05-07 13:27 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-05-01 3:38 Why not Coq2Ada program extraction? Dan'l Miller
2018-05-01 3:59 ` Paul Rubin
2018-05-01 6:59 ` Chris M Moore
2018-05-01 7:41 ` Paul Rubin
2018-05-01 11:44 ` Jere
2018-05-02 16:47 ` G.B.
2018-05-02 17:12 ` Paul Rubin
2018-05-01 8:21 ` Jeffrey R. Carter
2018-05-01 17:30 ` Dan'l Miller
2018-05-01 9:12 ` Paul Rubin
2018-05-07 2:30 ` Dan'l Miller
2018-05-07 2:37 ` Paul Rubin
2018-05-07 3:50 ` Dan'l Miller
2018-05-07 4:01 ` Dan'l Miller
2018-05-07 4:20 ` Paul Rubin
2018-05-07 16:33 ` Dan'l Miller
2018-05-07 13:27 ` Dan'l Miller [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox