Formal Verification: Theorem proving

How many times in the course of a project have you heard of the term Formal Verification? This relatively short on article theorem proving article assumes that you know the basic definition of Formal Verification while we try to see what Theorem proving is in relation to Formal Verification.

The theorem proving techniques relate specification and implementation as a theorem in logic to be proven in the context of a proof calculus. The implementation acts as a provider of axioms and assumptions for the proof. Like the math classes we had in school, involves proving of lemmas and theorems by deduction, rewriting and induction. This is mainly used for verification at a higher level of abstraction usually in algorithmic verification. This is more successful in complex problems and systems like distributed algorithms and real-time systems.

The first tools for this method were available in 1970's. Currently there exists a variety of tools which are more or less automatic. some of them being, ACL2, NQTHM, PVS, HOLY, Isabelle, STeP...

However this technique requires a strong user expertise and time intenseive guidance of the proof. The usual theorem prover tools are based on first order predicate logic, Higher-order predicate logic, Recursive functions, Induction etc. Eg., "The ACL2 logic is a first order logic of total recursive functions providing mathematical induction..."

Brush up of basics:
First-order predicate logic: Predicate logic in which predicates take only individuals as arguments and quantifiers only bind individual variables.

Induction: A powerful technique for proving that a theorem holds for al cases in a large infinite set. The proof has two steps, the basis and induction step. Roughly, in the basis the theorem is proved to hold for the "ancestor" case, and in the induction step it is proved to hold for all "descendant" cases.

Higher-order predicate logic: Predicate logic in which predicates take other predicates as arguments and quantifiers bind predicate variables. For example, second order predicates take first-order predicates as arguments. Oder n predicates take order n-1 predicates as arguments (n>1).

In summary, the theorem proving tools use sophisticated combination of decision proedures, conditional rewriting, Induction & recursion, propositional simplification, complex heuristics to orchestrate all of that. The tool learns over its lifetime by making use automatically of lemmas being proven by the user.

Bottomline:
Very powerful mainly at algorithmic level. However you should go get an expert :-)