caxapa.ru :: CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. -> While CBMC is aimed for embedded software, it also supports dynamic memory allocation

Evgeny_CD, Архитектор (30.09.2015 22:34 - 22:53, просмотров: 279) ответил Evgeny_CD на Подборка по метапрограммированию вокруг С и С++.

CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. -> While CBMC is aimed for embedded software, it also supports dynamic memory allocation http://www.cprover.org/cbmc/
using malloc and new.

mit2011.pdf cbmc-slides.pdf

Ответить

- SCOOT statically analyses systems described using SystemC and extracts models that can be passed to verification tools such as SatAbs or CBMC. -> - Evgeny_CD(30.09.2015 22:54, ссылка)

Средства и методы разработки