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!
I queued and pushed all but this one. Their website [1] says seL4.
At least I *think* that this is their website.
Either way, I agree that this should be consistent with their naming.
On the Promela/spin change, should a similar change be applied in the
Formal Verification chapter?
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
>
>
