一句话：推出工业级开源 C 模型检测器 ESBMC 5.0，新增前后端、IEEE 浮点支持与改进的 k-归纳算法。
ESBMC 是成熟且采用宽松许可证的开源上下文限界模型检测器，用于验证单线程和多线程 C 程序。它能自动检查预定义安全性质（如数组越界、指针安全和算术溢出）以及用户定义的程序断言。ESBMC 5.0 的主要改进包括新的前端与后端、IEEE 浮点支持，以及改进的 k-归纳算法；同时提供 C++ 和 Python API，使研究者可访问内部数据结构，并在验证过程的任意阶段进行检查和扩展。论文还通过在线演示展示了该工具的实际使用。
ESBMC is a mature, permissively licensed open-source context-bounded model checker for the verification of single- and multi-threaded C programs. It can verify both predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions automatically. ESBMC provides C++ and Python APIs to access internal data structures, allowing inspection and extension at any stage of the verification process. We discuss improvements over previous versions of ESBMC, including the description of new front- and back-ends, IEEE floating-point support, and an improved k-induction algorithm. A demonstration is available at https://www.youtube.com/watch?v=YcJjXHlN1v8 .
@inproceedings{paperbot4727,
title = {ESBMC 5.0: an industrial-strength C model checker},
author = {Mikhail R. Gadelha and Felipe R. Monteiro and Jeremy Morse and Lucas C. Cordeiro and Bernd Fischer and Denis A. Nicole},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240481}
}