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


25

Can I find a general algorithm to solve the halting problem for some possible program input pairs? Yes, sure. For example you could write an algorithm that returns "Yes, it terminates" for any program which contains neither loops nor recursion and "No, it does not terminate" for any program that contains a while(true) loop that will definitely be reached ...


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


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

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

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


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


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

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


4

If you count as a " program verification technique " the combination of runtime bound-checking and fuzzing, yes this particular bug could have been caught. Proper fuzzing will cause the now infamous memcpy(bp, pl, payload); to read across the limit of the memory block pl belongs to. Runtime bound-checking can in principle catch any such access, ...


4

A formal specification of a program is (more or less) a program written in another programming language. As a result, the specification will certainly include its own bugs. The advantage of formal verification is that, as the program and the specification are two separate implementations, their bugs will be different. But not always: one common source of ...


4

Using a tighter language doesn't just move goal posts around from getting implementation correct to getting the spec right. It is hard to make something that is very wrong yet consistent logically; which is why compilers catch so many bugs. Pointer Arithmetic as it is normally formulated is unsound because the type system doesn't actually mean what it is ...


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