OSVAuto: automatic proofs about functional specifications in OS verification
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916750221639680 |
|---|---|
| author | Wu, Yulun Xia, Bican Xu, Jiale Zhan, Bohua Zhao, Tianqi |
| author_facet | Wu, Yulun Xia, Bican Xu, Jiale Zhan, Bohua Zhao, Tianqi |
| contents | We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to support natively those data types that commonly occur in OS verification, including sequences, maps, structures and enumerations. Propositions about these data are encoded into a form that is suitable for SMT solving. For quantifier instantiation, we propose an extension of recent work for automatic proofs about sequences. We evaluate the algorithm on proof obligations adapted from existing verification of the uC-OS/II kernel in Coq, demonstrating that a large number of proof obligations can be solved automatically, significantly reducing the proof effort on the functional side. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_13457 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | OSVAuto: automatic proofs about functional specifications in OS verification Wu, Yulun Xia, Bican Xu, Jiale Zhan, Bohua Zhao, Tianqi Symbolic Computation Logic in Computer Science We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to support natively those data types that commonly occur in OS verification, including sequences, maps, structures and enumerations. Propositions about these data are encoded into a form that is suitable for SMT solving. For quantifier instantiation, we propose an extension of recent work for automatic proofs about sequences. We evaluate the algorithm on proof obligations adapted from existing verification of the uC-OS/II kernel in Coq, demonstrating that a large number of proof obligations can be solved automatically, significantly reducing the proof effort on the functional side. |
| title | OSVAuto: automatic proofs about functional specifications in OS verification |
| topic | Symbolic Computation Logic in Computer Science |
| url | https://arxiv.org/abs/2403.13457 |