Formal verification for high-assurance behavioral synthesis
type: Item
instance of: scholarly article
title: Formal Verification for High-Assurance Behavioral Synthesis
zbMATH Open document ID: 1262.68128
DOI: 10.1007/978-3-642-04761-9_25
author: Sandip Ray
author: Kecheng Hao
author: Yan Chen
author: Fei Xie
author: Jin Yang
published in: Automated Technology for Verification and Analysis
publication date: 2009-12-01T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68M15
zbMATH DE Number: 5640947
describes a project that uses: cvc3
MaRDI profile type: MaRDI publication profile
full work available at URL: 978-3-642-04761-9 25
OpenAlex ID: W2122890990
cites work: Validating High-Level Synthesis
cites work: A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
cites work: Q4484891
cites work: The existence of refinement mappings
cites work: Computer Aided Verification
cites work: Q3777424
cites work: Proof producing synthesis of arithmetic and cryptographic hardware
cites work: Formal certification of a compiler back-end or: programming a compiler with a proof assistant
Recommended article: A study about the efficiency of formal high-level synthesis applied to verification
Recommended article: Formally analyzed dynamic synthesis of hardware
Recommended article: Q4503963
Recommended article: Mechanical certification of loop pipelining transformations: a preview
Recommended article: Mechanised wire-wise verification of Handel-C synthesis
description: scientific article; zbMATH DE number 5640947