Applications

ESBMC has been used in a broad range of applications. If you applied ESBMC in your research, but it is not mentioned below, please, do not hesitate to contact us through our GitHub repository.

• DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles
• ESBMC is used to verify embedded control software in Unmanned Aerial Vehicles.
• BMCLua: A Translator for Model Checking Lua Programs
• ESBMC is used to verify a ANSI-C version of the respective Lua program.
• CSeq: A Sequentialization Tool for C
• ESBMC is used as sequential verification back-end to model check multi-threaded programs.
• Sound and Unified Software Verification for Weak Memory Models
• ESBMC is used as a sequential consistency software verification tool in real-life C programs.
• Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples
• The counter-example produced by ESBMC is used to automatically debug software systems.
• Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker
• ESBMC is used as an untimed software model checker to verify real-time software.
• Scalable hybrid verification for embedded software
• ESBMC is used as a verification engine to model check embedded (sequential) software.
• Getting Rid of Store-Buffers in TSO Analysis
• ESBMC is used to verify sequential consistency concurrent C programs.