SBIR/STTR Research Award
A Semantics-Based Verification Toolset for UAS Embedded Software
Award amount
$749,847Program and phase
SBIR · Phase IIAward year
2021Award details
- Awarding agency
- National Aeronautics and Space Administration
- Branch
- Not reported
- Recipient company
- Runtime Verification, Inc.
- Proposal award date
- 2021-08-03
- Contract end date
- 2023-08-02
- UEI
- FFVYL2M1N826
- Solicitation number
- SBIR_20_P2
- Topic code
- A2
Research abstract
Develop bounded model checker for C programs that detects undefined behavior.nbsp; Convert prototype developed in Phase I into a robust tool capable of analyzing Airliner, a drone autopilot developed by Windhover under contract from NASA.The bounded model checker and a C interpreter that detects undefined behavior in unit tests are both generated from the same formal semantics of C.Both the tools will be integrated into the build system of Airliner, and used to analyze Airliner and applications built from Airliner.
Technology keywords
Not reported
Other awards by this recipient
Verified by the same UEI. These are other public SBIR/STTR award pages, not a merged company record.
- A Semantics-Based Verification Toolset for UAS Embedded Software
- SBIR Phase II: RV-Embedded: Runtime Verification for Embedded Systems
- SBIR Phase I: Runtime Verification for Automobiles
- A Scalable Semantics-Based Verification System for Flight Critical Software
- A Scalable Semantics-Based Verification System for Flight Critical Software
Research funding history
7 SBIR/STTR records share this UEI (2010–2021). Reported award amounts total $2,871,189. Reported amounts are not federal obligations.
Phases: Phase I, Phase II
Agencies: National Aeronautics and Space Administration, National Science Foundation