Mechanised wire-wise verification of Handel-C synthesis

DOI10.1016/J.SCICO.2010.02.007zbMath1243.68154OpenAlexW2016401360MaRDI QIDQ436367

J. C. P. Woodcock, Juan I. Perna

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

correctnessdenotational semanticsHOLmechanical verificationHandel-C synthesis

Mathematics Subject Classification ID

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

Uses Software

• HOL
• Handel-C

Cites Work

• A Denotational Semantics for Handel-C
• UTP Semantics for Handel-C
• Mechanised Wire-wise Verification of Handel-C Synthesis
• Higher Order Logic and Hardware Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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