>From aefb442330115d2af25f532fcd725ed4c06e6908 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa <akiyks@xxxxxxxxx> Date: Tue, 19 Jul 2016 23:30:18 +0900 Subject: [PATCH] formal: Trivial typo fixes Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx> --- formal/formal.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/formal/formal.tex b/formal/formal.tex index 0e5fef3..ed9d7a3 100644 --- a/formal/formal.tex +++ b/formal/formal.tex @@ -126,7 +126,7 @@ The larger overarching software construct is of course validated by testing. because the rate of change is just too great. Furthermore, although the L4 microkernel is a large software artifact from the viewpoint of formal verification, it is tiny - compared to the a great number of projects, including LLVM, + compared to a great number of projects, including LLVM, gcc, the Linux kernel, Hadoop, MongoDB, and a great many others. Although formal verification is finally starting to show some @@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than a mechanical proof for a complex implementation! And the open challenge to those working on formal verification techniques -and systems is prove this summary wrong! +and systems is to prove this summary wrong! -- 1.9.1 -- To unsubscribe from this list: send the line "unsubscribe perfbook" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
