Logic for software verification

Question

I'm looking at the requirements for automated software verification, i.e. a program that takes in code (ordinary procedural code written in languages like C and Java), generates a bunch of theorems saying that each loop must eventually halt, no assertion will be violated, there will never be a dereference of a null pointer etc., then passes same to a theorem prover to prove they are actually true (or else find a counterexample indicating a bug in the code).

The question is what kind of logic to use. The two major positions seem to be:

1. First-order logic is just fine.

2. First-order logic isn't expressive enough, you need higher order logic.

Problem is, there seems to be a lot of support for both positions. So which one is right? If it's the second one, are there any available examples of things you want to do, that verifiers based on first-order logic have trouble with?

Poundal

Answer 1

You can do everything you need in FOL, but it's a lot of extra work - a LOT! Most existing systems were developed by academics / people with not a lot of time, so they are tempted to take short cuts to save time / effort, and thus are attracted to HOLs, functional languages, etc. However, if you want to build a system that is to be used by hundreds of thousands of people, rather than merely hundreds, we believe that FOL is the way to go because it is far more accessible to a wider audience. There's just no substitute for doing the work; we've been at this for 25 years now! Please take a look at our project (http://www.manmademinions.com)

Regards, Aaron.

Duntson

Answer 2

In my practical experience, it seems to be "1. First-order logic is just fine". For examples of complete specifications for various functions written entirely in a specification language based on first-order logic, see for instance ACSL by Example or this case study.

First-order logic has automated provers (not proof assistants) that have been refined over the years to handle well properties that come from program verification. Notable automated provers for these uses are for instance Simplify, Z3, and Alt-ergo. If these provers fail and there is no obvious lemma/assertion you can add to help them, you still have the recourse of starting up a proof assistant for the difficult proof obligations. If you use HOL on the other hand, you cannot use Simplify, Z3 or Alt-ergo at all, and while I have heard of automated provers for high-order logic, I have never heard them praised for their efficiency when it comes to properties from programs.

Ecumenicalism

Answer 3

We've found that FOL is fine for most verification conditions, but higher order logic is invaluable for a small number, for example for proving properties about summation of the elements in a collection. So our theorem prover (used in Perfect Developer and Escher C Verifier) is basically first order, but with the ability to do some higher order reasoning as well.

True