Design and Verification of Microprocessor Systems for High-Assurance Applications

• Corporate Author: SpringerLink (Online service)
• Other Authors: Hardin, David S. (Editor)
• Format: Electronic eBook
• Language: English
• Published: Boston, MA : Springer US, 2010.
• Subjects: Engineering.; Computer-aided engineering.; Quality control.; Reliability.; Industrial safety.; Electronic circuits.; Circuits and Systems.; Computer-Aided Engineering (CAD, CAE) and Design.; Quality Control, Reliability, Safety and Risk.

Design and Verification of Microprocessor Systems for High-Assurance Applications Edited by: David S. Hardin This book examines several leading-edge design and verification technologies that have been successfully applied to microprocessor systems for high-assurance applications at various levels –...

Table of Contents:

• ACL2 and Its Applications to Digital System Verification
• A Mechanically Verified Commercial SRT Divider
• Use of Formal Verification at Centaur Technology
• Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol
• Verifying Pipelines with BAT
• Formal Verification of Partition Management for the AAMP7G Microprocessor
• Compiling Higher Order Logic by Proof
• Specification and Verification of ARM Hardware and Software
• Information Security Modeling and Analysis
• Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel
• Refinement in the Formal Verification of the seL4 Microkernel
• Specification and Checking of Software Contracts for Conditional Information Flow
• Model Checking Information Flow.