Although Isabelle/HOL can be run in batch mode to check proofs, it is primarily an interactive tool. AutoCorres, and also the C parser on which it builds, have not been designed to write specifications and proofs to files. Rather, specifications and proofs are constructed in the internal state of Isabelle/HOL, and the only realistic way to inspect these is in interactive mode.

For example, the following sequence of commands should give you an interactive session looking at the AutoCorres "plus" example:

# Check out l4v and its companion repositories.

# Requires the Google `repo` tool.

# See https://github.com/seL4/verification-manifest/blob/master/README.md for more details.

$ mkdir verification

$ cd verification

$ repo init -u ssh://git@github.com/seL4/verification-manifest.git

$ repo sync

# Build some prerequisites. Requires the "MLton" Standard ML compiler, and possibly some other tools installed.

$ cd l4v
$ make -C tools/c-parser CParser

$ make -C tools/autocorres AutoCorres tests/ROOT

# Start an interactive session.

# Ignore the warnings in the pop-up dialog.

$ ./isabelle/bin/isabelle jedit -d . -l AutoCorres tools/autocorres/tests/examples/Plus.thy &

To see the specifications and definitions produced by the C parser and AutoCorres in the interactive session, make sure you have the "Output" pane open, and type the command "print_theorems" immediately after each of the "install_C_file" and "autocorres" commands, respectively.

Best regards,
Matthew Brecknell

Hello,

I have been trying to study how seL4's C code is formally verified. So I looked into Autocorres tool and had a bit of hard time understanding how to use the tool to generate Isabelle definitions from C code. I tried to follow Autocorres' quickstart but I was confused since I do not know much about Isabelle/HOL.

I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it gave me this output:

```

Session Pure/Pure
Session FOL/FOL
Session HOL/HOL (main)
Session HOL/HOL-Eisbach
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Number_Theory (main timing)
Session HOL/HOL-Statespace
Session HOL/HOL-Word (main timing)
Session Lib/Word_Lib (lib)
Session Lib/Lib (lib)
Session C-Parser/Simpl-VCG
Session C-Parser/CParser
Session Lib/CLib (lib)
Session Unsorted/AutoCorres
Session Unsorted/AutoCorresTest
Building AutoCorresTest ...
AutoCorresTest: theory AutoCorresTest.CustomWordAbs
AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation

...

Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor 3.23)

```

But I couldnt find any Isabelle definitions as output except "thy" files that contain:

```

theory somefile
imports "AutoCorres.AutoCorres"
begin

external_file "somefile.c"

install_C_file "somefile.c"

autocorres "somefile.c"

end

```

I suppose I need to invoke this file somehow using Isabelle in order to generate the definition but I'm not sure how to do that. Any help would be very appreciated.

Best Regards,

Norrathep

Norrathep (Oak) Rattanavipanon

M.S. in Computer Science

University of California - Irvine