On Sat, Dec 02, 2023 at 01:32:09PM -0800, SeongJae Park wrote: > On Sat, 2 Dec 2023 11:29:45 -0800 "Paul E. McKenney" <paulmck@xxxxxxxxxx> wrote: > > > On Sat, Dec 02, 2023 at 09:26:14AM -0800, SeongJae Park wrote: > > > formalregress.tex is using mixed use of SEL4 and seL4. SEL4 is used 8 > > > times, while seL4 is used twice over the entire repository. Use SEL4 > > > for the consistency. Note that use of seL4 in swtools.bib is not > > > changed by this commit. > > > > > > Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx> > > > > Nice, thank you! > > You're very welcome, Paul! > > > > > I queued and pushed all but this one. Their website [1] says seL4. > > At least I *think* that this is their website. > > Agreed :) > > > > > Either way, I agree that this should be consistent with their naming. > > Sure, I will send a new revision soon. > > > > > On the Promela/spin change, should a similar change be applied in the > > Formal Verification chapter? > > I already finished the translation of the chapter, but hopefully I will revisit > it soon :) Don't wait for me, though! Fair enough! ;-) Thanx, Paul > Thanks, > SJ > > > > > Thanx, Paul > > > > [1] https://sel4.systems/ > > > > > --- > > > future/formalregress.tex | 2 +- > > > 1 file changed, 1 insertion(+), 1 deletion(-) > > > > > > diff --git a/future/formalregress.tex b/future/formalregress.tex > > > index b1a39b29..40bf2b35 100644 > > > --- a/future/formalregress.tex > > > +++ b/future/formalregress.tex > > > @@ -701,7 +701,7 @@ so they are all yellow with question marks. > > > Indeed there are! > > > This table focuses on those that Paul has used, but others are > > > proving to be useful. > > > - Formal verification has been heavily used in the seL4 > > > + Formal verification has been heavily used in the SEL4 > > > project~\cite{ThomasSewell2013L4binaryVerification}, > > > and its tools can now handle modest levels of concurrency. > > > More recently, Catalin Marinas used Lamport's > > > -- > > > 2.17.1 > > > > > >
