William D. Young

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

2013

Building a Hypervisor on a Formally Verifiable Protection Layer.

[BibT_eX]

[DOI]

Michael McCoyd

Robert Bellarmine Krug

Deepak Goel

Mike Dahlin

Proceedings of the 46th Hawaii International Conference on System Sciences, 2013

2011

Toward the Verification of a Simple Hypervisor

[BibT_eX]

[DOI]

Mike Dahlin

Ryan Johnson

Robert Bellarmine Krug

Michael McCoyd

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

2008

Mechanized Information Flow Analysis through Inductive Assertions.

[BibT_eX]

[DOI]

Warren A. Hunt Jr.

Robert Bellarmine Krug

Sandip Ray

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2006

A robust machine code proof framework for highly secure applications.

[BibT_eX]

[DOI]

David S. Hardin

Eric W. Smith

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2005

Introducing Abstractions via Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

1997

Comparing Verification Systems: Interactive Consistency in ACL2.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1997

Mathematical Modeling and Analysis of an External Memory Manager.

[BibT_eX]

[DOI]

Proceedings of the FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 1997

1995

A State-Machine Approach to Non-Interference.

[BibT_eX]

[DOI]

J. Comput. Secur., 1995

Connection policies and controlled interference.

[BibT_eX]

[DOI]

Richard M. Cohen

Proceedings of the Eighth IEEE Computer Security Foundations Workshop (CSFW '95), 1995

1994

A State-Based Approach to Non-Interference.

[BibT_eX]

[DOI]

Proceedings of the Seventh IEEE Computer Security Foundations Workshop, 1994

1992

Machine Checked Proofs of the Design of a Fault-Tolerance Circuit.

[BibT_eX]

Formal Aspects Comput., 1992

Introduction to a Formally Defined Hardware Description Language.

[BibT_eX]

Bishop Brock

Warren A. Hunt Jr.

Proceedings of the Theorem Provers in Circuit Design, 1992

1991

Formal Methods versus Software Engineering: Is There a Conflict?

[BibT_eX]

[DOI]

Proceedings of the Symposium on Testing, Analysis, and Verification, 1991

Mathematical Methods for Digital Systems Development.

[BibT_eX]

[DOI]

Proceedings of the VDM '91, 1991

1990

Verified program support environments.

[BibT_eX]

[DOI]

Proceedings of the Conference proceedings on Formal methods in software development, 1990

1989

A Mechanically Verified Code Generator.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

An Approach to Systems Verification.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

Verified Compilation in micro-Gypsy.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGSOFT '89 Third Symposium on Testing, Analysis, and Verification, 1989

1987

Extending the Noninterference Version of MLS for SAT.

[BibT_eX]

[DOI]

J. Thomas Haigh

IEEE Trans. Software Eng., 1987

An Experience Using Two Covert Channel Analysis Techniques on a Real System Design.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1987

Coding for a Believable Specification to Implementation Mapping.

[BibT_eX]

[DOI]

John McHugh

Proceedings of the 1987 IEEE Symposium on Security and Privacy, 1987

Toward Verified Execution Environments.

[BibT_eX]

[DOI]

Warren A. Hunt Jr.

Proceedings of the 1987 IEEE Symposium on Security and Privacy, 1987

1986

Extending the Non-Interference Version of MLS for SAT.

[BibT_eX]

[DOI]

J. Thomas Haigh

Proceedings of the 1986 IEEE Symposium on Security and Privacy, 1986

1985

Secure Ada Target: Issues, System Design, and Verification.

[BibT_eX]

[DOI]

Proceedings of the 1985 IEEE Symposium on Security and Privacy, 1985

1981

Steelman and the verifiability of (preliminary) ADA.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 1981

HAL/S/V: a verifiable subset for HAL/S.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 1981

1980

Generics and verification in Ada.

[BibT_eX]

[DOI]

Proceedings of the ACM-SIGPLAN symposium on The ADA programming language, 1980

A preliminary evaluation of verifiability in Ada.

[BibT_eX]

[DOI]

Anand R. Tripathi