45
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 ...
- 31.2k
32
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.♦
- 166k
20
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
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,192
9
votes
Accepted
What's role of software verification in modern software engineering
This is actually a surprisingly complex topic.
Who verifies the verifiers?
Have you heard of Ada/SPARK?
Ada is a programming language which is mostly used in embedded contexts, including in military ...
- 550
8
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
7
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 ...
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.3k
6
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,295
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,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 ...
- 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 ...
- 541
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 ...
- 12.1k
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,927
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 ...
- 279k
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,631
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,097
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
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 ...
- 550
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 ...
4
votes
What's role of software verification in modern software engineering
To be honest this feels like it's a question of just practicality and feasibility. The reality is that all of our systems are just so complex these days, that it's almost impossible to just verify ...
- 330
3
votes
Accepted
Continuation-passing style: what is meant by "CPS'ing"?
I had only a quick look at the paper, but I believe that they are referring to moving from
$$
t_1 \to t_2 \cdots \to t_n
$$
to
$$
t_1 \to t_2 \cdots \to \lnot \lnot t_n
$$
where $\lnot t = (t \...
- 14.7k
3
votes
Accepted
How to prove the equivalence between Hoare and Floyd assignment axioms?
but when I try $F = G[v/e]$ then from $\exists v' (F[v/v'] \land v=e[v/v'])$ I can't obtain $G$.
We can assume $v'$ not free in $G$. Then, we have
$$
\begin{array}{ll}
& \exists v' (F[v/v'] \...
- 14.7k
3
votes
Accepted
How to define the Atomic Propositions in Model Checking
Formal verification often involves at least three steps:
Make a formal model of the real-world system. (The formal model might be a state-transition graph or automaton, for example.)
Write down a ...
D.W.♦
- 166k
3
votes
Accepted
How to Specify the Behavior of Automata for Verification
It feels to me like this has already been explained before (1, 2). To prove that an automaton is correct, you first must define what correctness means to you. Usually that is done by writing a ...
D.W.♦
- 166k
3
votes
Proof Carrying LLVM?
This is a project I've been thinking of venturing into for a few years now, and I was fortunate to have a very useful discussion about it at the time I started planning it with Chris Lattner (at the ...
- 201
3
votes
Accepted
How a Symbolic Evaluator Generates Test Input for this Example
Tools that solve problems like this often use a SMT (Satisfiability Modulo Theories) solver. This a SAT solver combined with a "theory solver" that can understand operations in some domain.
For ...
- 1,043
3
votes
Accepted
Alternatives to Unit Testing?
There are several ways to ensure product/code quality and functionality before deployment:
Basic functionality testing
Code Review
Static code analysis
Unit Testing
Single user performance testing
Only top scored, non community-wiki answers of a minimum length are eligible