46 votes
Accepted

Do theorem provers demonstrate their own correctness?

I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code. There are many levels of formal ...
Andrej Bauer's user avatar
  • 30.4k
30 votes
Accepted

Program Correctness, The specification

First off, you're absolutely right: you're on to a real concern. Formal verification transfers the problem of confidence in program correctness to the problem of confidence in specification ...
D.W.'s user avatar
  • 158k
20 votes

Formal program verification in practice

I would like to mention three remarkable applications of formal methods/formal verification tools in industry or non-trivial real systems. Note that I have little experience on this topic and I only ...
hengxin's user avatar
  • 9,521
19 votes

Program Correctness, The specification

D.W.'s answer is great, but I'd like to expand on one point. A specification is not just a reference against which the code is verified. One of the reasons to have a formal specification is to ...
Gilles 'SO- stop being evil''s user avatar
10 votes
Accepted

Data Flow Analysis with exceptions

Ignoring exceptions is unsound. Example: let g = { raise E; } let f = { x := interesting_stuff(); g(); x := 0; } When analyzing ...
Gilles 'SO- stop being evil''s user avatar
10 votes

Do theorem provers demonstrate their own correctness?

What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover": In many theorem provers, the trusted core—the code that must be right to ensure ...
Alexey Romanov's user avatar
7 votes
Accepted

An example of something you can formally verify with proofs in Software Development

Look into tools like Frama-C, SPARK, Astrée, etc... They have their use in very specific cases, notably software verification of small to medium sized embedded safety critical software (e.g. inside ...
Basile Starynkevitch's user avatar
7 votes

Is there a way to convert a program into a Boolean formula?

Disclaimer: I'm not sure how useful any of this is for getting this done practically since you have a program, not a Turing Machine. The Cook-Levin Theorem essentially states that you can translate ...
testuser's user avatar
  • 171
6 votes
Accepted

What is the difference between $x:A$ and $x \Xi A$?

$x:A$ is a statement about objects in the formal system, like, for example, $\vdash 2+4:\texttt{int}$, whereas $x\Xi A$ is an expression in the formal system, like $\texttt{if}~ 2 + 4 ~\texttt{==}~5 ~...
Dave Clarke's user avatar
  • 20.2k
6 votes

What are common formal techniques for proving functional code correct?

You can start with Software Foundations by Benjamin C. Pierce et al. Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, ...
Anton Trunov's user avatar
  • 3,469
6 votes

An example of something you can formally verify with proofs in Software Development

Quite a lot of things can and have been formally verified with formal methods. Compilers. We want to prove that a compiler preserves the semantics of its source program. For example, if we write a <...
xuq01's user avatar
  • 1,190
6 votes
Accepted

How CompCert "proves" different things in its codebase

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq. I would suggest ...
xuq01's user avatar
  • 1,190
6 votes

Do theorem provers demonstrate their own correctness?

While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is ...
Mario Carneiro's user avatar
6 votes
Accepted

A general picture of formal verification in software

A formally proven program is a formally proven program regardless of which language it's in. Just because a program is written in Coq and perhaps extracted to OCaml or Haskell, rather than written in ...
Gilles 'SO- stop being evil''s user avatar
5 votes

What are common formal techniques for proving functional code correct?

It turns out that an excellent source of proof techniques and examples for proving things about pure functional languages is proof assistants which usually include as part of their specification ...
cody's user avatar
  • 8,154
5 votes
Accepted

What are common formal techniques for proving functional code correct?

One of the de facto methods for proving results in functional programming is via Richard Bird's group. In particular, you ask for an in-depth or at least more comprehensive approach to equational ...
Musa Al-hassy's user avatar
5 votes
Accepted

What exactly is Symbolic Model Checking?

Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs). The ...
Lance's user avatar
  • 2,193
5 votes
Accepted

High-level requirements for a Proof of "Saving to the Database"

The SoftwareEngineering.SE link gives the wrong answer for the right reasons. You can only ever prove anything with respect to a formal model. Verifying that that formal model accurately captures ...
Derek Elkins left SE's user avatar
5 votes
Accepted

Stablishing termination of the construction of infinite stream with ranking functions

I think Turing's method is probably fine, but you are mistaken about why exactly the code you wrote, "terminates." First, note that this is not really (written as) a function at all. It is a self-...
Dan Doel's user avatar
  • 2,639
5 votes

Imperfection in randomness in VLC shuffle playlist - why?

This is just speculation, but perhaps what VLC is attempting is to simulate... perfect randomness. That is, each song is picked uniformly at random, independently of previous songs. According to the ...
Yuval Filmus's user avatar
4 votes
Accepted

How to use structural induction to prove law on lists

You'll want a helper lemma to make this endeavor more digestible. Notations for map and subs: I'm going to condense the ...
Lee's user avatar
  • 1,097
4 votes

What does "AF AX p" mean in CTL?

Your understanding of $AF AX p$ is correct (in my opinion). But whether it seems particularly strange or hard to understand is rather subjective. The argument you quote compares the expressiveness or ...
hengxin's user avatar
  • 9,521
4 votes

What are common formal techniques for proving functional code correct?

I suggest to use program logics. They deal much better with effects than typing systems. There are numerous program logics for functional languages. This becomes interesting with effects. See e.g. ...
Martin Berger's user avatar
4 votes

How is CFL-reachability solvable in exponential time and space?

The input for CFL-reachability problem consists of two parts: the grammar and the graph. As far as time complexity should be measured in terms of the input size, we should include both grammar and ...
gsv's user avatar
  • 141
4 votes

Formal program verification in practice

A formal specification of a program is (more or less) a program written in another programming language. As a result, the specification will certainly include its own bugs. The advantage of formal ...
vonbrand's user avatar
  • 14k
4 votes

How to Generate Control flow graph from a Petri net model?

Since you are interested in generating test sequences automatically using colored Petri nets, note that it's not clear that you need reduction to control flow graphs (and dealing with all the related ...
ivcha's user avatar
  • 540
4 votes

Where in the toolchain does formal specification come in?

Tests can be written based on either a formal spec or an informal spec. Verification always requires a formal specification. Formal verification might be manual or automated, or some combination of ...
D.W.'s user avatar
  • 158k
4 votes

Finding weakest precondition

Weakest precondition (WPC) can be computed with a procedure that takes your program, as well as the given postcondition (in this case, x=y), as inputs, and applies ...
ivcha's user avatar
  • 540
4 votes

A general picture of formal verification in software

The book that defines TLA+ is "Specifying systems" by Leslie Lamport. TLA+ is a language for writing mathematics (TLA+ is based on Zermelo-Fraenkel set theory). TLA+ includes temporal ...
0 _'s user avatar
  • 143
4 votes
Accepted

Proving program termination in the $\lambda$-calculus

This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops. Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda ...
Gilles 'SO- stop being evil''s user avatar

Only top scored, non community-wiki answers of a minimum length are eligible