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 ...
- 30k
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.♦
- 156k
25
votes
Accepted
What is this fraction-like "discrete mathematics"–style notation used for formal rules?
This is a standard notation for an inference rule. The premises are put above a horizontal line, and the conclusion is put below the line. Thus, it ends up looking like a "fraction", but with one or ...
D.W.♦
- 156k
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
Why does the state remain unchanged in the small-step operational semantics of a while loop?
The state can change in subsequent reduction steps because on the right hand side of
$$
\langle while\ B\ do\ S, \sigma \rangle
\quad\rightarrow\quad
\langle if\ B\ then\ ( {\color{red}{S}};\ ...
- 8,308
10
votes
Accepted
Why does the state remain unchanged in the small-step operational semantics of a while loop?
In programming language semantics, the notion of program state is not a vague philosophical notion, but a very precise mathematical one. A state $s$ in this small-step operational semantics is a ...
- 2,486
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
9
votes
How does automated verification of systems with infinitely many states work?
Infinite-state system verification is indeed a rather broad topic. First of all, all computers used nowadays can only have a finite number of states, as the amount of RAM is fixed. But that's is ...
- 2,732
9
votes
Why does the state remain unchanged in the small-step operational semantics of a while loop?
The state $\sigma$ does not change when we consider $B$ to decide whether to perform one iteration of the loop, but it can change later when we run the body $S$. And so, the next time we consider $B$, ...
- 30k
9
votes
Accepted
How does TLC check liveness properties?
Presumably it can check any "liveness" property that that can be formulated in LTL. A "liveness" property is typically described as a property stating that "something good eventually happens". This is ...
7
votes
What is this fraction-like "discrete mathematics"–style notation used for formal rules?
Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition!
The Ap is the state of your system or ...
- 171
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
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
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
Problem with definition of bisimilarity
You seem to be confusing the definition of bisimilarity with an algorithm for finding a bisimulation.
In your examples, the states are indeed bisimilar, and the relation is the set
$$\{(A,A)\}$$
It ...
- 17k
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
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
Relating a proof to a Haskell program
Your goal is to “prove” --I'm using bullets “•” for syntactic separators--
$$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x < (y+1)²$$
Proof Methods
In the natural deduction style, one proves “∀ x : ℕ • P x” by ...
- 884
5
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
Accepted
What are these questions in the PoplMark challenge asking?
The reduction relation is beta reduction (for term and type variables) as defined in the description of Challenge 2B. It's a single reduction step, not repeated reduction until a value is reached.
(3)...
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.♦
- 156k
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
How does automated verification of systems with infinitely many states work?
While DCTLib's answer provides some insight in the general ideas, I think it is useful to give a more concrete example that has some use in practice.
One kind of 'infinite state system' is a labelled ...
- 7,768
4
votes
Minimal Deterministic Buchi Automata Product
This is only a partial answer (as I believe that the state of the art is insufficient to answer your questions completely - I am happy to be proven wrong here), but I hope that it helps you anyway.
...
- 2,732
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,501
4
votes
Accepted
What exactly state is in Model Checking
My vote is on (4) from an intuition point of view.
I just started learning this recently so take this with a grain of salt but as mentioned by D.W. the set of states can be anything you want. It is ...
- 178
4
votes
Accepted
How to express the existence of winning strategy of the starter of a game in temporal logic?
I don't think it's possible in CTL nor LTL to model two competing players.
You would probably need ATL (Alternating-time Temporal Logic). In ATL, the formula $\langle\langle A \rangle\rangle \phi$ ...
- 15.5k
4
votes
Why does the denotational semantics for a while loop have a existence quantifier?
The existential quantifier is misplaced. This is due to lack of reasonable notation for what needs to be expressed, namely: "if there is $i$ safisfying condition $C$, then use that $i$", where we make ...
- 30k
4
votes
Roadmap to formal verification
My goal is to be able to judge what parts of formal verification I
could apply to my job as a software/network engineer.
If you plan to use formal verification as black boxes, then I would suggest ...
- 522
Only top scored, non community-wiki answers of a minimum length are eligible