Mechanised wire-wise verification of Handel-C synthesis

DOI10.1016/J.SCICO.2010.02.007zbMATH Open1243.68154OpenAlexW2016401360MaRDI QIDQ436367FDOQ436367

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unifying theories for logic programming
• A Denotational Semantics for Handel-C
• UTP semantics for Handel-C
• Title not available (Why is that?)
• Title not available (Why is that?)
• Mechanised Wire-wise Verification of Handel-C Synthesis
• Higher Order Logic and Hardware Verification

Cited In (1)

• Title not available (Why is that?)

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)