OSVAuto: semi-automatic verifier for functional specifications of operating systems
CoRR(2024)
Abstract
We present the design and implementation of a tool for semi-automatic
verification of functional specifications of operating system modules. Such
verification tasks are traditionally done in interactive theorem provers, where
the functionalities of the module are specified at abstract and concrete levels
using data such as structures, algebraic datatypes, arrays, maps and so on. In
this work, we provide encodings to SMT for these commonly occurring data types.
This allows verification conditions to be reduced into a form suitable for SMT
solvers. The use of SMT solvers combined with a tactic language allows
semi-automatic verification of the specification. We apply the tool to verify
functional specification for key parts of the uC-OS/II operating system, based
on earlier work giving full verification of the system in Coq. We demonstrate a
large reduction in the amount of human effort due to increased level of
automation.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined