CAD for Assurance of Electronic Systems
 

PROMPT

By: Tuba Yavuz (University of Florida) and Ken (Yihang) Bai (University of Florida)

Stage: Software Design and Development

Summary

PROMPT performs component-level analysis using API model guided symbolic execution. API models can be specified using the PROSE API modeling language. PROMPT has been applied to a variety of system code, including device drivers and protocol stack implementations in the Linux kernel and cryptographic libraries.

Contact

Tuba Yavuz

Input/Output Interface

  • Input: LLVM bitcode and the API model
  • Output: A set of test cases and/or reports of various errors

Dependencies

LLVM 3.8

Licensing Info

Apache 2.0

References

Yavuz, Tuba; Bai, Ken (Yihang)

Analyzing system software components using API model guided symbolic execution Journal Article

In: Automated Software Engineering, 2020, ISSN: 1573-7535.

Abstract | Links | BibTeX

Acknowledgments

  • Partially funded by by the National Science Foundation awards CNS-1815883 and CNS-1942235 and by the Semiconductor Research Corporation

Additional Information

User Guide Link can be found at this link