Design and Verification of Microprocessor Systems for High-Assurance Applications - Hardin, David S.; SpringerLink (Online service) (New York, NY : Springer US : Imprint: Springer, 2010)
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.
Keywords: Electronic circuits; Computer-aided engineering; Quality control; Reliability; Industrial safety; Circuits and Systems; Computer-Aided Engineering (CAD, CAE) and Design; Quality Control, Reliability, Safety and Risk