From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server

Autor: Koh, Nicolas, Li, Yao, Li, Yishuai, Xia, Li-yao, Beringer, Lennart, Honoré, Wolf, Mansky, William, Pierce, Benjamin C., Zdancewic, Steve

Publikováno v: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '19), January 14--15, 2019, Cascais, Portugal

We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChic

Externí odkaz: http://arxiv.org/abs/1811.11911

Verifying an HTTP Key-Value Server with Interaction Trees and VST

Autor: Zhang, Hengchu, Honoré, Wolf, Koh, Nicolas, Li, Yao, Li, Yishuai, Xia, Li-Yao, Beringer, Lennart, Mansky, William, Pierce, Benjamin, Zdancewic, Steve

Publikováno v: Zhang, H, Honoré, W, Koh, N, Li, Y, Li, Y, Xia, L-Y, Beringer, L, Mansky, W, Pierce, B & Zdancewic, S 2021, Verifying an HTTP Key-Value Server with Interaction Trees and VST . in L Cohen & C Kaliszyk (eds), 12th International Conference on Interactive Theorem Proving (ITP 2021) . vol. 193, 32, Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, Dagstuhl, Germany, The 12th Conference on Interactive Theorem Proving, Rome, Italy, 29/06/21 . https://doi.org/10.4230/LIPIcs.ITP.2021.32

We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchai

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2b9ee561c8493c80cc8e92ee7df6371e
https://hdl.handle.net/20.500.11820/a1eae769-c4b8-4ab5-a983-d45a5a82bd53