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


35

I'll try to give a succinct answer to some of your questions. Please bear in mind that this is not strictly my field of research, so some of my info may be outdated/incorrect. There are many tools that are specifically designed to formally prove properties of Java and C++. However I need to make a small digression here: what does it mean to prove ...


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


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


15

I would like to mention three remarkable applications of formal methods/formal verification tools in industry or non-trivial real systems. Note that I have little experience on this topic and I only learn them from reading papers. The open-source tool Java Pathfinder (JPF for short) released by NASA in 2005 is a system to verify executable Java bytecode ...


11

I am not in a position to tell how much more research should be done on the topic, but I can tell you that there is research being done, for example the Verisoft XT program funded by the german government. The concepts which I think you are looking for are called formal verification and contract based programming, where the latter is a programmer-friendly ...


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

Ignoring exceptions is unsound. Example: let g = { raise E; } let f = { x := interesting_stuff(); g(); x := 0; } When analyzing f, you need to take into account the fact that g raises an exception, otherwise you would incorrectly conclude that x is always 0 on return from f. I don't know that there is a “standard” technique for dealing ...


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

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

Your axiom is not really an axiom, it's missing hypotheses. Simple presentations of Hoare logic manipulate formulas of the form $\{P\} C \{P'\}$ where $P$ and $P'$ are logical formulas and $C$ is a command. You do need to ensure that $C$ is well-formed. In simple languages such as the ones often used for a first introduction to Hoare logic, well-formedness ...


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

Notice that what Wikipedia is saying is that The assignment axiom means that the truth of $\{P[x/E]\}$ is equivalent to the after-assignment truth of $\{P\}$. In other words, ($P$ holds after the execution of $x:= E$) if ($P[x/E]$ holds before the execution). This is equivalent to the definition $A$ you provided, which is generally a more intuitive ...


6

To answer your question in the most concise way - yes, this bug could have potentially been caught by formal verification tools. Indeed, the property "never send a block which is bigger than the size of the hearbeat that was sent" is fairly simple to formalize in most specification languages (e.g. LTL). The problem (which is a common criticism against ...


6

You can start with Software Foundations by Benjamin C. Pierce et al. Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students ...


6

$x:A$ is a statement about objects in the formal system, like, for example, $\vdash 2+4:\texttt{int}$, whereas $x\Xi A$ is an expression in the formal system, like $\texttt{if}~ 2 + 4 ~\texttt{==}~5 ~\texttt{then}~ e_1~ \texttt{else} ~e_2$.


6

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq. I would suggest you start with Software Foundations. Most of your questions would be answered there. But, basically: Definition and Fixpoint are like OCaml's let and let rec,...


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

Commercial program checkers like Klocwork or Coverity might have been able to find Heartbleed since it is a relatively simple "forgot to do a bounds check error," which is one of the main problems they are designed to check for. But there is a much simpler way: use opaque abstract data types that are well tested to be free from buffer overrun. There are 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

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

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


5

You have an intended postcondition for a loop, and you're looking for an interesting invariant. In this scenario, try taking the intended postcondition, and replacing the total number of iterations (here N) by the number of iterations so far (here i). There's no guarantee that this is an invariant: that's only the case if the way the postcondition is somehow ...


5

One of the de facto methods for proving results in functional programming is via Richard Bird's group. In particular, you ask for an in-depth or at least more comprehensive approach to equational reasoning and list induction and this is provided in Lectures on Constructive Functional Programming. More generally, the text "Algebra of Programming", by Bird ...


5

It turns out that an excellent source of proof techniques and examples for proving things about pure functional languages is proof assistants which usually include as part of their specification language a pure functional language on which it is possible to reason equationally. One might want to consult a book like Certified Programing with Dependent Types ...


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

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


5

I think Turing's method is probably fine, but you are mistaken about why exactly the code you wrote, "terminates." First, note that this is not really (written as) a function at all. It is a self-referential value. And the reason the program terminates even though it's defined in it is that the program does not attempt to evaluate it fully. In this case, ...


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