Design and Verification of Microprocessor Systems for High-Assurance Applications

1. ACL2 and Its Applications to Digital System Verification
Matt Kaufmann, J Strother Moore

2. A Mechanically Verified Commercial SRT Divider
David M. Russinoff

3. Use of Formal Verification at Centaur Technology
Warren A. Hunt, Sol Swords, Jared Davis, Anna Slobodova

4. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol
Sally Browning, Philip Weaver

5. Verifying Pipelines with BAT
Panagiotis Manolios, Sudarshan K. Srinivasan

6. Formal Verification of Partition Management for the AAMP7G Microprocessor
Matthew M. Wilding, David A. Greve, Raymond J. Richards, David S. Hardin

7. Compiling Higher Order Logic by Proof
Konrad Slind, Guodong Li, Scott Owens

8. Specification and Verification of ARM Hardware and Software
Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen

9. Information Security Modeling and Analysis
David A. Greve

10. Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel
Raymond J. Richards

11. Refinement in the Formal Verification of the seL4 Microkernel
Gerwin Klein, Thomas Sewell, Simon Winwood

12. Specification and Checking of Software Contracts for Conditional Information Flow
Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David Greve

13. Model Checking Information Flow
Michael W. Whalen, David A. Greve, Lucas G. Wagner

Avainsanat: Engineering, Circuits and Systems, Computer-Aided Engineering (CAD, CAE) and Design, Quality Control, Reliability, Safety and Risk