Support
Research Funding
Last modified: Sat Jan 24 20:28:00 2026 GMT.
The work by the FLINT group has been supported by the following grants from NSF, DARPA and ONR as well as several gifts from Microsoft Research and Intel:- DARPA TRACTOR: PROCTOR: Compositional Certified Translation of Concurrent C to Idiomatic Rust
- 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
