As of May 31, 2023, we have updated our Code of Conduct.
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
  • 29.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
  • 152k
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.'s user avatar
  • 152k
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
11 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 ...
Wandering Logic's 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}};\ ...
Martin Berger'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 ...
Hans Hüttel's user avatar
  • 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 ...
Alexey Romanov's 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. ...
Klaus Draeger's 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$, ...
Andrej Bauer's user avatar
  • 29.4k
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 ...
DCTLib's user avatar
  • 2,692
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 ...
Derek Elkins left SE's user avatar
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 ...
trunklop's user avatar
  • 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 ...
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

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 ...
Nadim Kobeissi's user avatar
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,170
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
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,103
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 ...
Shaull's user avatar
  • 16.7k
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

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 ...
Musa Al-hassy's 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 ...
D.W.'s user avatar
  • 152k
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,441
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
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)...
Gilles 'SO- stop being evil''s user avatar
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. ...
DCTLib's user avatar
  • 2,692
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 ...
Discrete lizard's user avatar
  • 7,533
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 ...
MuchToLearn's user avatar
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$ ...
Pål GD's user avatar
  • 14.5k

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