Higher Order Logic and Hardware Verification

DOI10.1017/CBO9780511569845zbMath0819.68015OpenAlexW1588212183MaRDI QIDQ5966707

No author found.

Publication date: 23 January 1993

Full work available at URL: https://doi.org/10.1017/cbo9780511569845

zbMATH Keywords

formal logicdigital hardware designs

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Computer system organization (68M99)

Related Items (11)

Proof producing synthesis of arithmetic and cryptographic hardware ⋮ Verification of FPGA layout generators in higher-order logic ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ Mechanised wire-wise verification of Handel-C synthesis ⋮ Algebraic models of correctness for abstract pipelines. ⋮ A theory of abstraction ⋮ A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL ⋮ Implementation issues about the embedding of existing high level synthesis algorithms in HOL ⋮ Algebraic models of microprocessors architecture and organisation ⋮ Coquet: A Coq Library for Verifying Hardware ⋮ Refinement of time

This page was built for publication: Higher Order Logic and Hardware Verification