Design and verification of microprocessor systems for high-assurance applications
By: David S. Hardin, editor
Publisher: Springer
Published: 2010
Place of publication: New York; London
Language: eng
Number of pages: 436
ISBN-13: 9781441915382; 9781441915399
Subjects: Programmable controllers; Testing; Design and construction
Notes: Includes bibliographical references and index.
Table of contents: title: ACL2 and its applications to digital system verification  -- Matt Kaufmann and J. Strother Moore; title: mechanically verified commercial SRT divider  -- David M. Russinoff; title: Use of formal verification at Centaur Technology  -- Warren A. Hunt, Jr., Sol Swords, Jared Davis and Anna Slobodova; title: Designing tunable, verifiable cryptographic hardware using Cryptol  -- Sally Browning and Philip Weaver; title: Verifying pipelines with BAT  -- Panagiotis Manolios and Sudarshan K. Srinivasan; title: Formal verification of partition management for the AAMP7G microprocessor  -- Matthew M. Wilding, David A. Greve, Raymond J. Richards and David S. Hardin; title: Compiling higher order logic by proof  -- Konrad Slind, Guodong LI and Scott Owens; title: Specification and verification of ARM hardware and software  -- Anthony C. J. Fox, Michael J. C. Gordon and Magnus O. Myreen; title: Information security modeling and analysis  -- David A. Greve; title: Modeling and security analysis of a commercial real-time operating system kernel  -- Raymond J. Richards; title: Refinement in the formal verification of the SeL4 microkernel  -- Gerwin Klein, Thomas Sewell and Simon Winwood; title: Specification and checking of software contracts for conditional information flow  -- Torben Amtoft, John Hatcliff and Edwin Rodriguez / -- Robby / -- Jonathan Hoag and David Greve; title: Model checking information flow -- Michael W. Whalen, David A. Greve and Lucas G. Wagner.