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.
"synopsis" may belong to another edition of this title.
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 – from arithmetic circuits to microcode to instruction sets to operating systems to applications. We focus on recent hardware, software, and system designs that have actually been built and deployed, and feature systems that have been certified at high Evaluation Assurance Levels, namely the Rockwell Collins AAMP7G microprocessor (EAL7) and the Green Hills INTEGRITY-178B separation kernel (EAL6+). The contributing authors to this book have endeavored to bring forth truly new material on significant, modern design and verification efforts; many of the results described herein were obtained only within the past year.
"About this title" may belong to another edition of this title.
(No Available Copies)
Search Books: Create a WantCan't find the book you're looking for? We'll keep searching for you. If one of our booksellers adds it to AbeBooks, we'll let you know!
Create a Want