9
$\begingroup$

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT solvers (in ongoing - reactive systems), but what about first order Logic with temporal? Does it use theorem provers? Or can it also use SAT?

Any pointers to books or articles for beginners in this matter is much appreciated.

$\endgroup$
9
$\begingroup$

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 is a counter-example.

The tool Alloy is one tool that allows models to be described in first-order logic (though the surface syntax is based on relationally described models) and uses bounded model checking to find solutions. A SAT solver is used under the hood. One alloy extension allows models with a temporal character, though technically it does not support temporal logic.

If you wish to explore further, for example, to verify program correctness, then you can look at program verification tools. These are generally based on Hoare logic (for reasoning about pre- and post-conditions), possibly extended with Separation logic (for reasoning about heaps). These logics are generally undecidable, so a certain amount of interaction between the human and the verification tool is required. Some example tools are:

$\endgroup$
10
$\begingroup$

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 checking and Formal Software Verification: Model Checking and Theorem Proving

Dave has given a good answer for which I cannot do much more justice to the first part of the question than Dave had done, since I am also new to this.

Since this is your first question at an SE site, the reason I did not give an answer but a comment is because here an answer cannot be just a set of links, but must give a written answer and use links in support of the answer; thus a comment instead of an answer.

With regards to:

Any pointers to books or articles for beginners in this matter is much appreciated.

Books I would suggest and use are:

At present I cannot expand more on theorem proving because I am still learning the pro/cons and differences of each one, but the ones I am focusing in are

  • HOL Light because of the book by John Harrison.
  • Coq because it is based on Calculus of constructions
  • Isabelle because it is based on higher-order unification.

    These proof assistants also typically have book(s), are current, popular, open-source, maintained, and have active support communities.

Note: I used worldcat.org to reference the books, but you can review them using Amazon's look inside feature.

$\endgroup$
  • $\begingroup$ To avoid lots of edits to the answer, I will drop added info as comments and then in the future roll them up into the answer. For trying to sort out the many similarities and differences between proof assistants. Google for Freek Wiedijk; I find his papers to be quite useful. $\endgroup$ – Guy Coder Aug 12 '12 at 0:42
  • $\begingroup$ Many many thanks for your detailed and thorough answer. For adding your comments on books and providing a link to the free book. Again, I can't thank you enough :-) $\endgroup$ – FELIPE N. Aug 14 '12 at 17:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.