[PATCH v2] future/formalregress: Use seL4 consistently

formalregress.tex is using mixed use of SEL4 and seL4.  SEL4 is used 8
times, while seL4 is used twice over the entire repository.  That said,
seL4 seems the intended name since their website[1] uses the name.  Use
seL4 consistently.

[1] https://sel4.systems/

Signed-off-by: SeongJae Park <[email protected]>
---
Changes from v1
- Use seL4 instead of SEL4

 future/formalregress.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/future/formalregress.tex b/future/formalregress.tex
index b1a39b29..63c9021f 100644
--- a/future/formalregress.tex
+++ b/future/formalregress.tex
@@ -118,23 +118,23 @@ that the compiler is correct.
 An alternative approach is to take the binary produced by the C compiler
 as input, thereby accounting for any relevant compiler bugs.
 This approach has been used in a number of verification efforts,
-perhaps most notably by the SEL4
+perhaps most notably by the seL4
 project~\cite{ThomasSewell2013L4binaryVerification}.
 
 \QuickQuiz{
 	Given the groundbreaking nature of the various verifiers used
-	in the SEL4 project, why doesn't this chapter cover them in
+	in the seL4 project, why doesn't this chapter cover them in
 	more depth?
 }\QuickQuizAnswer{
-	There can be no doubt that the verifiers used by the SEL4
+	There can be no doubt that the verifiers used by the seL4
 	project are quite capable.
-	However, SEL4 started as a single-CPU project.
-	And although SEL4 has gained multi-processor
+	However, seL4 started as a single-CPU project.
+	And although seL4 has gained multi-processor
 	capabilities, it is currently using very coarse-grained
 	locking that is similar to the Linux kernel's old
 	Big Kernel Lock (BKL)\@.
 	There will hopefully come a day when it makes sense to add
-	SEL4's verifiers to a book on parallel programming, but
+	seL4's verifiers to a book on parallel programming, but
 	this is not yet that day.
 }\QuickQuizEnd
 
-- 
2.17.1