2
$\begingroup$

Given that there are examples of formal proofs used to formally verify real-world software applications, I would like to know what these people and teams actually do to create these formal proofs. That is, the kind of code they write and/or the types of formal proofs they create, and how the proofs work. For example, maybe the proofs are term derivation trees, or state-transition graphs, etc.

I understand how model checking works, but the model itself should probably be "proven" somehow even before checking it against a specification. What I am wondering here is only about proofs. For example, in airplanes, what types of things they are proving, and how they are going about proving them. For example, maybe they prove that the plane will land if this button is pressed. That is the what they prove part. Then they do this by writing some Coq code that is exported to ocaml, and in the Coq code they have to prove x about the button itself, and y about the forces of air while the plane is flying, and z that the air brakes will apply effective force etc. And they do this by starting from axioms a b and c. That is the how part.

I don't need to know exactly they are doing the specific proofs, just generally how they go about it. I would like to know generally what they start from, how they formalize and prove it (the model not the spec) in a language, and how this results in a feeling of "now our code is proven". My previous questions about proofs didn't go into enough depth about how the proofs actually work.

Another example from the link is satellite technology, compilers, and os-kernels.

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ I would suggest you read their papers... $\endgroup$
    – xuq01
    Jun 24, 2018 at 3:08
  • $\begingroup$ Near-duplicate of this question which had answers to this question also: You can study the source code (including proof) of CompCert & of seL4 for example (since these are publicly downloadable for research purposes) $\endgroup$
    – Basile Starynkevitch
    Jun 24, 2018 at 5:09
  • $\begingroup$ @xuq01 Comments like that are not very helpful and make this community seem very unhelpful to newcomers. Those papers are often very intimidating and not helpful for most people. This is a form of elitism that drives me insane about cs/math communities. $\endgroup$
    – avf
    Apr 13, 2021 at 0:04
  • $\begingroup$ @avf I'm not sure what you mean by intimidating. Many system verification papers are very easily accessible. And also, there is no real way to answer this type of question besides summarizing and/or pointing one to those papers. If you want to learn about someone's research, you'd have to read their papers --- nothing elitist about that IMO. $\endgroup$
    – xuq01
    Apr 13, 2021 at 7:07
  • $\begingroup$ Many system verification papers are very easily accessible. This is exactly what I mean with elitism. Most system verification papers are extremely difficult to read for people who are not familiar with the matter. Just because something comes easy to you doesn't mean it's easy for others. I came to this question hoping for a good resource/blog post with a good example for a formal proof of verified software, with an understandable explanation. Thus far I haven't been able to find something like this online, and I think this attitude is part of the reason for it. $\endgroup$
    – avf
    Apr 13, 2021 at 11:04

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.