Support

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

National Science Foundation

• SHF: Small: Automated Verification and Synthesis of Input Generators in Property-Based Testing Frameworks (abstract)
• 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)
• REVERSER: Repair Engineering for Verified Software Resilience.
• Discovering and Explaining Threats of Emergent Computation to enable Transformations (DETECT)
• Algorithms and Architectures for Robust Attack Detection Using Multi-Modal Controller Logs

STR and US Air Force
    Verification and Validation Assistant

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