From 6f43405ebe9f64081decc8f3dfe6cd57ee39e6be Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sat, 15 Jan 2022 23:05:36 +0200 Subject: Add estimates for SLOC and time taken --- verified_resource_sharing.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index c47cf66..7f5f57c 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -418,7 +418,7 @@ stack is proven correct. Proofs of the load and store instructions are not quit additional invariants need to be proven to hold for those instructions. The pass that renames variables in HTL is yet to be proven, as is the pass that generates the final Verilog. -To give a rough idea of the scale and complexity of the task: the implementation of \vericertfun{} involved the addition of about \MP{\ref{???}} lines of Coq code to \vericert{} and took the first author \MP{\ref{???}} months. The correctness proof, so far, has taken \MP{\ref{???}} lines of Coq code and \MP{\ref{???}} months. +To give a rough idea of the scale and complexity of the task: the implementation of \vericertfun{} involved adding or changing about 700 lines of Coq code in \vericert{} and took the first author 4 months. The correctness proof, so far, has required about 2300 lines of additions or changes to the Coq code and 8 months. \section{Performance evaluation} -- cgit