By the same authors

Refinement-Based Verification of the FreeRTOS Scheduler in VCC

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)

Published copy (DOI)



Publication details

Title of host publicationFormal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015
DatePublished - 2015
Number of pages16
PublisherLecture Notes in Computer Science
EditorsMichael Butler, Sylvain Conchon, Fatiha Zaidi
Original languageEnglish
ISBN (Print)978-3-319-25422-7


We describe our experience with verifying the scheduler-related functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.

Bibliographical note

© 2015. Springer International Publishing Switzerland. This is an author-produced version of the published chapter. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations