Skip to Main content Skip to Navigation
Conference papers

Logic against Ghosts: Comparison of Two Proof Approaches for a List Module

Abstract : Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays. This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a convenient high-level view of the linked list. The specifications of all functions are now proved faster and almost all automatically, only a small number of auxiliary lemmas and a couple of assertions being proved interactively in Coq. The proposed specifications are validated by proving a few client functions manipulating lists. During the verification, a more efficient implementation for one function was found and verified. We compare the new approach with the previous effort based on ghost arrays, and discuss the benefits and drawbacks of both techniques.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Allan Blanchard Connect in order to contact the contributor
Submitted on : Tuesday, April 16, 2019 - 8:36:22 AM
Last modification on : Tuesday, January 18, 2022 - 5:44:01 PM


Files produced by the author(s)



Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. Logic against Ghosts: Comparison of Two Proof Approaches for a List Module. SAC 2019 - The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297495⟩. ⟨hal-02100515⟩



Les métriques sont temporairement indisponibles