CAD for Assurance of Electronic Systems


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

Stage: Software Design and Development


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.


Tuba Yavuz

Input/Output Interface

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


LLVM 3.8

Licensing Info

Apache 2.0


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


  • 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