Projects

Current Projects

CRASH - Correct-by-Construction Attack Tolerant Systems

Funded By: Defense Advanced Research Projects Agency

Project website: www.nuprl.org/crash

Formally Generating Adaptive Security Protocols

Funded By: US Air Force

DivA: Automated generation of logical code diversity

Funded By: Office of Naval Research

Project Led By: Architecture Technology Corporation

Past Projects

Funded by:

Projects:

Selected Papers:

Defense Advanced Research Projects Agency	Distributed System Security Ensemble Groupware System	-- Assuring the Integrity of Highly Decentralized Communications Systems
		-- 1997 DARPA Summary Report

Program Composition for Embedded Systems	Open Logical Programming Environments	-- Formal Methods for Software Evolution: Interoperability Results
		-- An Open Logical Programming Environment: A Practical Framework for Sharing Formal Models and Tools

National Science Foundation

Interactive Formal Courseware

Proof Automation in Constructive Type Theory

Enabling Large Scale Coherency Among Mathematical Texts in the NSDL

-- Extracting Propositional Decidability, by James Caldwell

-- Lessons in Discrete Mathematics, by Stuart Allen

-- Using Web Access to Formal Mathematics
to Support Instruction in Computational
Discrete Mathematics; (abstract)

Office of Naval Research	Overview Building Interactive Formal Digital Libraries	-- Computational Complexity in Constructive Type Theory, by Robert Constable
		-- Nuprl Math Library