Sökning: "Andreas Lööw"

Hittade 2 avhandlingar innehållade orden Andreas Lööw.

1. 1. Building Verified Hardware and Verified Stacks in HOL

   Författare :Andreas Lööw; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

   Sammanfattning : This thesis explores building provably correct software and hardware inside the HOL4 interactive theorem prover. Interactive theorem provers such as HOL4 are proof environments where manual (human) and automated (machine) proofs can be composed in logically safe ways, and all proof steps (be it manual or automated) are mechanically checked. LÄS MER

3. 2. Building Verified Hardware and Verified Stacks in HOL

   Författare :Andreas Lööw; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; hardware synthesis; compilers; formal verification; interactive theorem proving;

   Sammanfattning : This thesis explores building provably correct software and hardware inside the HOL4 interactive theorem prover. Interactive theorem provers such as HOL4 are proof environments where manual (human) and automated (machine) proofs can be composed in logically safe ways and all proof steps (be it manual or automated) are mechanically checked. LÄS MER