Support

Support for my research comes from a variety of government and industrial
sources gratefully acknowledged below:

National Science Foundation

• FMiTF: Vayu: Verifying Infrastructure for Safe and Performant Tunable Consistency (abstract)
• CRONUS: High-Level Reasoning for Low-Level Isolation (abstract)
• Programming Non-Coherent Memory(abstract)
• EAGER: Verified Compilation and High-Level Memory Models (abstract)
• Robust Distributed Wind Power Engineering (abstract)
• A Computational Infrastructure for Scalable Transactional Memory Abstractions (abstract)
• Eager Maps and Lazy Folds for Graph-Structured Applications (abstract)
• A Unified Open Source Transactional Infrastructure (abstract)
• Relax: Controlled Declassification with Transactional Memory (abstract)
• Kala: An Efficient and Scalable Time-Travel Infrastructure for Concurrent Systems (abstract)
• A Computational Infrastructure for Experimentation on Relaxed Concurrency Abstractions and their Applications (abstract)
• Fault Determination and Recovery in Cycle-Sharing Infrastructures (abstract)
• Plethora: A Wide-Area Read-Write Storage Repository for the Internet (abstract)

DARPA
    Quelea: Verified Implementation of Weakly-Consistent Distributed Programs
    Mitchell: A Declarative Dataflow Framework and Real-Time Resource Optimization Engine
    SPARTA: Automating Format Comprehension and Trustworthy Parser Development
    Leveraging Symbolic Represenatations for Safe and Assured Learning
    Exploration Service for Synthesis and Evaluation of Novel CPS Emergent Designs (ESSENCE)

Semiconductor Research Corporation and DARPA
    C-BRIC:Center for Brain-inspired Computing

Cisco
    Investigation of IP Storage Protocols for Database Applications

Intel
    Profile-Guided Speculation for Multicore Architectures

Microsoft
    Compiler Backend Experimentation and Extensibility Using Phoenix
    Language and Runtime Support for Safe and Scalable Programs

NEC
    Distributed Storage Systems Research