# Tag Info

62

First, to dispel a possible cognitive dissonance: reasoning about infinite structures is not a problem, we do it all the time. As long as the structure is finitely describable, that's not a problem. Here are a few common types of infinite structures: languages (sets of strings over some alphabet, which may be finite); tree languages (sets of trees over some ...

41

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 ...

21

Let us consider the following inductive definition: \qquad \displaystyle \begin{align*} &\phantom{\Rightarrow} \quad \varepsilon \in \mathcal{T} \\ w \in \mathcal{T} \quad &\Rightarrow \quad aw \in \mathcal{T}\\ aw \in \mathcal{T} \quad &\Rightarrow \quad baw \in \mathcal{T} \end{align*} What is $\mathcal{T}$? Clearly, the set of ...

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 ...

16

In contrast to what the nay-sayers say, there are many effective techniques for doing this. Bisimulation is one approach. See for example, Gordon's paper on Coinduction and Functional Programming. Another approach is to use operational theories of program equivalence, such as the work of Pitts. A third approach is to verify that both programs satisfy the ...

16

The constructive equivalence of linear-time fixed point formulae (the logic is called $\nu$TL by some) and Buechi automata is given in a paper by Mads Dam from 1992. Fixed Points of Buchi Automata, FST&TCS 1992. See page 4 for the construction of a $\nu$TL formula from a Buechi automaton. The construction of a Buechi automaton from a $\nu$TL formula ...

14

In the preface of his book “Mathematical Discovery, On Understanding, Learning, and Teaching Problems Solving” George Pólya writes: Solving problems is a practical art, like swimming, or skiing, or playing the piano: you can learn it only be imitation and practice. This book cannot offer you a magic key that opens all the doors and solves all the ...

12

Because a CCS process is worth a thousand pixels – and it is easy to see the underlying LTS – here are two processes that simulates each other but are not bisimilar: $$P = ab + a$$ $$Q = ab$$ $\mathcal{R_1}=\{(ab+a, ab), (b, b), (0,b), (0, 0)\}$ is a simulation. $\mathcal{R_2}=\{(ab, ab+a), (b, b), (0,0)\}$ is a simulation. $P\ \mathcal R_1\ Q$ and $Q\ \... 12 This is clearly reducible from the Halting Problem. If a machine$M$does not stop on input$x$then any final state is "useless". Given an input$M,x$for the Halting problem, it is easy to construct$M_x$that halts on every input (thus its final state is not useless) if and only if$M$halts on$x$. That way you can decide Halting Problem if you can ... 10 To elaborate slightly on the "it's impossible" statements, here's a simple proof sketch. We can model algorithms with output by Turing Machines which halt with their output on their tape. If you want to have machines that can halt by either accepting with output on their tape or rejecting (in which case there's no output) you can easily come up with an ... 10 After reading your question the only way I could see and had enough knowledge to tie the topics together was to give a hi-level set of articles that drill down from software verification ending up with trying to unite model checking and theorem proving. Hopefully my comment did that: Take a look at Software verification then Formal verification then Model ... 10 The intuitive answer is that if you don't have unbounded loops and you don't have recursion and you don't have goto, your programs terminate. This isn't quite true, there are other ways to sneak non-termination in, but it's good enough for most practical cases. Of course the converse is wrong, there are languages with these constructs that do not allow non-... 10 Even if there's a simulation in each direction, the simulations back and forth may not relate the same sets of states. Sometimes you have a simulation$R_1$in one direction, and a simulation$R_2$in the other direction, and two states$p_1$and$q$which are related by$R_1$but not by$R_2$nor by any other simulation in the same direction. The canonical ... 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$. ... 9 First order logic is undecidable, so SAT solving does not really help. That said, techniques exist for bounded model checking of first order formulas. This means that only a fixed number of objects can be considered when trying to determine whether the formula is true or false. Clearly, this is not complete, but if a counter-example is found, then it truly ... 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. ... 9 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 ... 8 John Harrison's book is an exception in going all the way from theory to practice and making all the source code available. I think you will find it difficult to find an equivalent book for model checking, but there are a few that achieve a close approximation. Principles of Model Checking by Baier and Katoen contains a lot of examples and pretty detailed ... 7 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 ...

7

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

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

I really think "formal" methods are not a very good idea for educational purposes. For that matter, programming a computer is a "formal" method. Does it succeed as an educational tool? What is needed is understanding, intuition, and the ability to deal with abstraction. Formal methods hinder all that. Rather, they promote trial and error, hacking, ...

5

See Terminator and AProVe. They tend to rely on heuristics, and I'm not sure if they clearly describe the class of programs for which they work. Still, they are regarded as state-of-the art, so they should be good starting points for you.

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