42

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 verification (that's the phrase you're looking for in place of "proven") of a proof assistant: Verify that the algorithms used by the proof assistant are correct. Verify ...


30

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 correctness, so it is not a silver bullet. There are several reasons why this process can still be useful, though. Specifications are often simpler than the code ...


25

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 more logical propositions above the line and a single proposition below the line. If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's ...


19

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 validate it by proving some fundamental properties. Of course, the specification cannot be completely validated — the validation would be as complex as the ...


10

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}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle $$ the $while$-loop is guarded (preceeded) by $S$. The computation of $S$ may change the state so that the ...


10

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 partial function $$ s : \mathbf{Var} \hookrightarrow \mathbb{Z} $$ that records the values of the variables. So if $s\, x = v$, then variable $x$ has value $v$. ...


10

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 faithfulness—is quite small. As examples, HOL Light is an LCF-style system whose trusted core is 400 lines of Objective Caml, and Milawa is a Boyer-Moore style prover ...


9

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. That is, the least $X$ such that $X = A\cup(B\cap\circ X)$, and the greatest $X$ such that $X = A\cap(B\cup\circ X)$, respectively. More generally, we are talking ...


9

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$, there can be a change of $\sigma$.


9

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 mainly a matter of terminology -- any verification technique that needs to iterate over all possible states is doomed from the beginning due to computation time. ...


8

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 care about becomes false. The GEN and KILL points thus depend on the facts you care about. For example: if you were doing a constant propagation analysis you ...


7

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 your running program. "State" can mean a lot of things but in this case it seems to include a list of all defined local variables and their values. Why is Ap a ...


7

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 the execution of a Turing Machine into a boolean formula that is polynomial in the length of the TM's execution such that the formula is satisfiable iff the TM ...


6

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 usually contrasted to a "safety" property which states that "nothing bad ever happens". See e.g. Slide 20 of this SPIN tutorial. Basically, a basic safety ...


6

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 aircrafts, per DO-178C, or nuclear power plants, etc...). Such software have a few dozen thousands lines (or perhaps two hundred thousands at most of C or Ada ...


6

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 spot on. The introduction of the paper lays out what is needed to make this happen, and it's only a problem of engineering. As Andrej says, there are several ...


5

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 unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process. A ...


5

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 that it returns the correct answer if it terminates. Total correctness means that is it additionally guaranteed that the algorithm terminates. Such a proof ...


5

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 +1 instead of *2 is not only much slower but also fails for floating point numbers (the gaps between large consecutive floating point numbers are bigger than 1). The above procedure should work for both ...


5

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 is easy to verify that it satisfies the desired properties. This means that the structures are indeed bisimilar. What you were trying to do is to find an ...


5

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 reality (or at least accurately captures the parts you care about for your purposes) is an informal process. In many applications of formal methods, one of the most ...


5

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 int x = 3; x++; in C, we mean that. But the compiler might not produce correct assembly and machine code. It is known to be difficult to debug compilers, so a ...


5

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 proving two statements: Base case :: P 0 Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function Where, in this case, $$P x \;\;≡\;\; ∃y \;•...


4

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 correct, when it terminates. This idea can be extended to the computation of incomplete (partial) answers. Whatever is computed of the answer is correct, but the ...


4

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 question is what do they do and how do they work. You first have your source code for some application. You then transform your source code into some state-transition ...


4

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 in its correct place. Then, prove the loop invariant for the outer for loop taking into account the suggestion by @Yuval and you are done.


4

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 issues). Some techniques were presented, that use various different methods to generate test sequences from Petri nets. Some examples include: H. Watanabe and ...


4

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 guarantees that the variant is always non-negative. This is necessary to have a lower bound for the variant which decreases every iteration. The third rule relaxes that condition a little bit. The variant ...


4

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) says to find a term $t'$ such that $t \to t'$ because if one exists, then there are infinitely many such terms in $F_{<:}$: all the terms in the same alpha ...


4

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 the two; it depends what techniques you use. Typically, it's hard to do completely automatic verification -- it's more usual that verification systems automate ...


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