Mechanised wire-wise verification of Handel-C synthesis

DOI10.1016/J.SCICO.2010.02.007MaRDI QIDQ436367zbMATH OpenOpenAlexFDO

Authors Juan Perna, Jim Woodcock

Publication date 20 July 2012

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2010.02.007

zbMATH Keywords

denotational semanticsHOLcorrectnessHandel-C synthesismechanical verification

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Mechanised wire-wise verification of Handel-C synthesis
• Publication:4942020
• Proof producing synthesis of arithmetic and cryptographic hardware
• Correct hardware synthesis
• Verified compilation of communicating processes into clocked circuits

Cites work

• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• scientific article; zbMATH DE number 3902009 (Why is no real title available?)
• scientific article; zbMATH DE number 42862 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3423547 (Why is no real title available?)
• A Denotational Semantics for Handel-C
• Higher Order Logic and Hardware Verification
• Mechanised wire-wise verification of Handel-C synthesis
• UTP semantics for Handel-C
• Unifying theories for logic programming

Cited in

(3)

• scientific article; zbMATH DE number 1418462 (Why is no real title available?)
• Correct hardware synthesis
• Mechanised wire-wise verification of Handel-C synthesis

Describes a project that uses

Uses Software

• HOL
• Handel-C

This page was built for publication: Mechanised wire-wise verification of Handel-C synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q436367)