Re: [PATCH 7/7] future/formalregress: Use SEL4 consistently

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" <[email protected]> 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 <[email protected]>
> > 
> > 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
> > > 
> > >