Formal Verification for High-Assurance Behavioral Synthesis

DOI10.1007/978-3-642-04761-9_25zbMath1262.68128OpenAlexW2122890990MaRDI QIDQ3648710

Yan Chen, Sandip Ray, Kecheng Hao, Fei Xie, Jin Yang

Publication date: 1 December 2009

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04761-9_25

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Reliability, testing and fault tolerance of networks and computer systems (68M15)

Uses Software

• cvc3

Cites Work

• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Proof producing synthesis of arithmetic and cryptographic hardware
• Validating High-Level Synthesis
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Computer Aided Verification
• Formal certification of a compiler back-end or

This page was built for publication: Formal Verification for High-Assurance Behavioral Synthesis