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 ...
user avatar
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 ...
user avatar
  • 140k
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 ...
user avatar
  • 140k
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 ...
user avatar
10 votes

What are GEN and KILL statements in dataflow analysis?

Dataflow analysis works on sets of facts. GEN points are points in the graph where one of the facts you care about becomes true, and KILL points are points in the graph where one of the facts you ...
user avatar
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}};\ ...
user avatar
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 ...
user avatar
  • 2,418
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 ...
user avatar
9 votes
Accepted

What does least fix point and greatest fix point mean in Safety games

Probably the most common fixpoint expressions in model checking are things like $\mu X.A\cup(B\cap\circ X)$ and $\nu X.A\cap(B\cup\circ X)$, where $\circ$ is some flavour of "next state" operator. ...
user avatar
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$, ...
user avatar
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 ...
user avatar
  • 2,672
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 ...
user avatar
  • 171
7 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 ...
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 ...
user avatar
  • 171
6 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 ...
user avatar
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 ...
user avatar
5 votes

What exactly is Symbolic Model Checking?

Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example: A symbolic model of an OAUTH2 implementation could help check for ...
user avatar
  • 151
5 votes
Accepted

Maximum value a variable can hold without documentation

The first step should be count = 0 while (x*2 > x) x = x*2 count++ to find the largest power of 2 that can fit into the variable. Note that doing ...
user avatar
5 votes

Can we quantify how close a partially correct programs is to being correct?

Partial correctness does not mean that not all statements of a specification are met by an algorithm. Have a look at the Wikipedia article about correctness: Partial correctness of an algorithm means ...
user avatar
  • 236
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 ...
user avatar
  • 16.1k
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 ...
user avatar
5 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 <...
user avatar
  • 1,150
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 ...
user avatar
4 votes

Can we quantify how close a partially correct programs is to being correct?

In a nutshell: Partial correctness is an issue of termination, not ot correctness of what is computed. A function is partially correct with respect to a specification iff whatever it computes is ...
user avatar
  • 19.1k
4 votes

Rigorous Proof of Insertion Sort

Hint: first prove a loop invariant for the nested while, i.e. you need to prove that the nested while shifts to the right the elements as required to insert the j-element indexed by the outer for loop ...
user avatar
4 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 ...
user avatar
  • 1,853
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 ...
user avatar
  • 540
4 votes
Accepted

Anotation rules for while rule in deductive verification

As you have already said, the second and third rule include a variant t to prove termination whereas the first rule does not consider it. The second rule ...
user avatar
  • 236
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)...
user avatar
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 ...
user avatar
  • 140k

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