On Tue, Feb 22, 2022 at 10:18:57AM +0800, Zhouyi Zhou wrote: > In section formal regression test, "an question" should be "a question" instead. > > Signed-off-by: Zhouyi Zhou <zhouzhouyi@xxxxxxxxx> > --- > Hi Paul, > > I think in the first paragraph of section formal regression test, > "an question" should be "a question" instead. Good eyes! But the fix is to make it read "However, it is an open question as to whether hard-core formal verification will ever be included in the automated regression-test suites used for continuous integration within complex concurrent codebases, such as the Linux kernel", that is, to add the word "open". I made this change with your Reported-by, thank you! > I am very interested in this section. I have published a paper > related to formal methods 17 years ago, you may like it ;-) > > "A formal description of SECIMOS operating system" > https://dl.acm.org/doi/10.1007/11560326_22 Thank you for the tip! I will take a look. Thanx, Paul > Many thanks > Cheers > Zhouyi > -- > future/formalregress.tex | 2 +- > 1 file changed, 1 insertion(+), 1 deletion(-) > > diff --git a/future/formalregress.tex b/future/formalregress.tex > index e33c5161..279f4596 100644 > --- a/future/formalregress.tex > +++ b/future/formalregress.tex > @@ -11,7 +11,7 @@ > > Formal verification has long proven useful in a number of production > environments~\cite{JamesRLarus2004RightingSoftware,AlBessey2010BillionLoCLater,ByronCook2018FormalAmazon,CaitlinSadowski2018staticAnalysisGoogle,DinoDistefano2019FBstaticAnalysis}. > -However, it is an question as to whether hard-core formal verification > +However, it is a question as to whether hard-core formal verification > will ever be included in the automated regression-test suites used for > continuous integration within complex concurrent codebases, such as the > Linux kernel. > -- > 2.25.1 >
