Research

People

Publications

Software

Support

Links

Internal

Research Funding

Last modified: Sun Jun 25 17:35:53 2023 GMT.

• NSF SHF:Small: Compositional Certified Concurrent Abstraction Layers
• NSF PPoSS: Planning: High-Performance Certified Trust for Global-Scale Applications
• DARPA V-SPELLS: REFUEL: Verified Composition and Flattening of Unified Enclave Layers
• NSF FMitF:Track I: ADVERT: Compositional Atomic Specifications for Distributed System Verification
• NSF SaTC:CORE:Small: Partition-Oblivious Real-Time Hierarchical Scheduling
• NSF SHF:Medium: DeepSEA: A Language for Programming and Synthesizing Certified Software
• NSF SaTC:CORE:Small: Formal End-to-End Verification of Information-Flow Security for Complex Systems
• NSF Expeditions in Computing: The Science of Deep Specification
• NSF SHF:Small:VeriQ: Formal Quantitative Software Verification in Realistic Application Scenarios
• DARPA HACMS: Compositionality and Automation for Robotics Security
• ONR: Reasoning Infrastructure for Security-Aware Software Development
• NSF TC-Medium: Making OS Kernels Crash-Proof by Design and Certification
• DARPA CRASH: Advanced Development of Certified OS Kernels
• NSF TC-Small: Formal Reasoning about Concurrent Programs for Multicore and Multiprocessor Machines
• NSF TC-Large: Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software
• NSF CPA-SEL-T: Domain Specific Languages, Logics, and Proofs for Certified Software Design
• NSF CT-ISG: Certified Runtime Code Manipulation
• NSF CT-ISG: Modular Development of Certified Concurrent Code
• NSF: High-Assurance Common Language Runtime
• NSF ITR: FLINT---A Mobile-Code Infrastructure for Advanced Languages
• DARPA: Scaling Proof-Carrying Code to Production Compilers and Security Policies
• NSF: Typed Common Intermediate Format
• DARPA: Software Evolution using HOT Language Technology
• NSF: Foundations of Hot Languages and Software Evolution
• NSF CAREER: Type-Directed Compilation