Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: AutoCorres2

Email Gateway (May 27 2024 at 10:38):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I’m happy to announce a new AFP entry:

AutoCorres2

by

Matthew Brecknell,
David Greenaway,
Johannes Hölzl,
Fabian Immler,
Gerwin Klein,
Rafal Kolanski,
Japheth Lim,
Michael Norrish,
Norbert Schirmer,
Salomon Sickert,
Thomas Sewell,
Harvey Tuch and
Simon Wimmer

Abstract:
AutoCorres2 is a tool to facilitate the verification of C programs within Isabelle. It is a fork of AutoCorres.

https://www.isa-afp.org/entries/AutoCorres2.html

Enjoy,
René

P.S.: Note that the brevity of the abstract is in stark contrast to the fact that this is impressive AFP entry.
For instance, the full proof document consists of over 2000 pages with a table of contents
that requires 10 pages.

Email Gateway (May 27 2024 at 11:37):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
The website seems inconsistent. All entries on
https://www.isa-afp.org/sessions/autocorres2_test/ are just empty for me
on the webpage. The page https://www.isa-afp.org/sessions/autocorres2/
correctly displays the code of the theories, though

Email Gateway (May 27 2024 at 13:23):

From: Christine Rizkallah <cl-isabelle-users@lists.cam.ac.uk>
As a user and a huge fan of AutoCorres, I would much appreciate a brief summary of what’s in there and how it differs from and/or extends AutoCorres or where one could find further information beyond the theory files.
Thanks,
Christine

Email Gateway (May 27 2024 at 13:36):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear Peter,

thanks for the report. The website has been fixed.

René

Email Gateway (May 27 2024 at 13:37):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Dear Christine,

Please have a look at the Introduction chapter of the provided document. In that chapter there are links into the document were to find the information you search for. Moreover, following the Isabelle tradition there is a NEWS file in the root directory.

Regards,
Norbert

Email Gateway (May 27 2024 at 15:26):

From: Liam O'Connor <l.oconnor@ed.ac.uk>
Dear Norbert,

To avoid risk of speaking for Christine I will only speak for myself. None of the documents you refer to answer my question, which is: why was a fork necessary at all? Is it somehow impossible to get any contributions upstreamed into the original AutoCorres? Is there some incompatibility here? I’m more interested in the “why fork” question than the technical delta between AutoCorres and AutoCorres2.

With best wishes,
Liam

Email Gateway (May 27 2024 at 15:47):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Dear Liam,

We discussed the option to upstream the changes to the original AutoCorres, but finally agreed (together with the original maintainers of AutoCorres) to go for the AFP for several reasons. Here some of the major thoughts:

• The original AutoCorres has no standalone repository but is part of the very large seL4/l4v repository. We agreed that AutoCorres2 should become a general purpose tool for C verification and should evolve independently of seL4/l4v. This liberates us from a lot of constraints from seL4/l4v.
• The AFP is the right place for such a tool with greater visibility and fosters a tighter Integration with core Isabelle development
• While AutoCorres2 is conceptually an extension of AutoCorres it technically takes the freedom to break compatibility. A notable example is the switch from the former "nondet_monad" to the “spec_monad”, which we believe is more canonical and has nicer algebraic properties.

I hope this gives some insight.

Regards,
Norbert

Email Gateway (May 27 2024 at 18:11):

From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi,

As an expert in semantics frameworks I consider this a very nice
contribution from the Autocoress team. Congratulations!
It was frustrating to see this very nicely shallowly embedded and
monad-based semantics framework hard-wired to the byte-level memory model
of SeL4 (which made the verification framework look ad-hoc to SeL4
verification).
Autocorress also has a very nice VCG implementation supporting backward
weakest precondition reasoning with debugging tools for goal inspection
when the VCG fails or diverges or crashes (I hope this is also part of the
distribution).

Now after 18 years we have 4 amazing Isabelle-based framework for program
verification down to IR level (allowing to remove compilers front-end from
the trusted code base), these tools are:

1. Isabelle/C (that can be used as frontend for these semantics
frameworks and allowing code annotation with distinguished features such as
markup strings for devs comments and assertions, which make frama-C way
behind)

2. Autocoress2 (code-level program verification with potential of doing
system-level verification of components with since now the semantics
framework is not hardwired to the byte-level memory model of SeL4)

3. Isabelle/LLVM (which provide verification down to IR which means the
verified programs are compiler (front-end) agnostic)

4. Word library (allowing refinement to different byte-level
memory models)

Can someone now create a FORMAL link between these 4 pieces and create the
most advanced and UNIFIED programs verification framework in the world
which will remove compilers front-ends from trusted code-base for any
project that will use Isabelle?

Best wishes,
Yakoub.

Last updated: Jan 04 2025 at 20:18 UTC