Hands-on VeriFast with STM32 microcontroller

Posted on February 5, 2017 / Tags: c, verifast, stm32, arm, chibios

Table of contents

We had “Hands-on VeriFast with STM32 microcontroller” on 静的コード解析の会 at Tokyo.

This hands-on purpose is that non-professional person for embedded programming understands the development method and verification using VeriFast. The VeriFast is a verifier for single-threaded and multithreaded C language programs annotated with preconditions and postconditions written in separation logic. And VeriFast is easy to use with the graphical IDE.

The hands-on was going as following steps:

All of participants have had VeriFast verification platform, and feel the verification way of VeriFast for ChibiOS/RT on STM32 microcontroller. STMicroelectronics kindly gives me their MCU board NUCLEO-F091RC, for free. Thanks a lot!

We are planning same hands-on on OSC2017 at Hokkaido. Let’s propagandize verification method by VeriFast for embedded application!

Source code


Hands-on VeriFast with STM32 microcontroller from Kiwamu Okabe


blog comments powered by Disqus