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 ...
- 29.9k
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.♦
- 154k
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 ...
- 9,471
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 ...
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 ...
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 ...
- 3,127
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 ...
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 ...
- 171
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, ...
- 3,469
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 ~...
- 20.2k
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 <...
- 1,180
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 ...
- 1,180
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 ...
- 531
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 ...
- 2,163
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 ...
- 7,979
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 ...
- 884
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 ...
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-...
- 2,579
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 ...
- 274k
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.♦
- 154k
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 ...
- 9,471
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. ...
- 8,308
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 ...
- 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 ...
- 13.9k
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 ...
- 540
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 ...
- 1,057
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 ...
- 540
4
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 ...
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 ...
- 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 ...
Only top scored, non community-wiki answers of a minimum length are eligible