Dear Thomas Maybe theorem prover can provide a proof or certification?
Shen > On Nov 20, 2015, at 7:08 PM, Thomas Melham <thomas.mel...@balliol.ox.ac.uk> > wrote: > > Dear Shengyu: > > There is a long history of hardware verification with higher order logic > theorem provers. This topic receded significantly when model checking and > BMC appeared on the scene, but in the longer run who knows? Attached is a > paper illustrating some recent practical work that builds on this long > tradition, and gives a history of one thread. > > All best regards, > Tom > > On 20/11/2015 09:44, "shengyu shen" <shengyus...@icloud.com> wrote: > >> Dear all: >> >> I am a new learner of HOL , and I am also a researcher on hardware >> verification. >> >> After learning HOL and COQ, and according to my experience in hardware >> verification, I get a feeling that : >> >> most, if not all, hardware verification problem can be solved with a >> framework similar to model checking, which generate CNF and call SAT/SMT >> solver. >> >> And it seems that almost all papers about coq and how appears in software >> language that reason about higher order logic.? >> >> Is this correct? >> >> >> >> -------------------------------------------------------------------------- >> ---- >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info > > <paper.pdf> ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
