You are downloading a tool and set of theories for Isabelle/HOL. This tool translates a large subset of C99 code into the imperative language Simpl embedded in the theorem prover Isabelle/HOL. This language provides a verified verification condition generator and further tools for software verification.
This tool is used to verify the functional correctness of the seL4 microkernel and some other programs, as part of the L4.verified project.
Please send email to c-parser <AT> trustworthy.systems
if you have questions, problems, or feature requests. While we
can't promise to be able to provide support and help for all
requests, we are interested in turning this tool from a research
prototype for experts into a slightly more widely applicable
tool.
The C parser code is part of the L4.verified repository, in
the tools/c-parser
directory.
The C parser is distributed under a BSD license. The tar file for download bundles the following 3rd party components.
c-parser-1.17.tar.gz (Released 2020-11-02, Isabelle 2020)
Older releases: