Introduction into first order logic verification

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.

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:

-
Logic in Computer Science - Modelling and Reasoning about Systems 2nd Ed. by Huth and Ryan This introduces logic and moves up to model checking, but doesn't go into theorem proving. So this should cover all of your basic questions related to logic and model checking.

-
Principles of model checking by Baier and Katoen I just started reading this one, and it is much better than reading lots of papers and trying to see how they all fit together. This is one of the most, if not the most recommended book on the subject of model checking. It should answer your more advanced questions on model checking.

-
Temporal logic and state systems by Kroger and Merz I often like to have books by different authors when self-learning a subject. This one is to complement/round out "Principles of model checking"

-
Handbook of practical logic and automated reasoning by Harrison Being a programmer I can't recommend this book enough. The book starts off with introducing logic and moves all the way through the point of creating the kernel for a theorem prover based on the work of HOL Light. Just to highlight that the book uses working OCaml code, explains the theorems in terms I find friendly and gives you what you need to know but not so much that you can't make the connection or feel like you are running down side tracks. If is a very focused book on going from logic to a specific type of theorem prover.

-
How to prove it : a structured approach by Velleman To get into the Proof assistants for theorem proving you will need to live and sleep theorems.

-
A Introduction to Proofs and the Mathematical Vernacular by Day This is a free book that not only complements "How to prove it", it goes beyond it in sum regards. I would not be surprised to see this one become popular.

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.

StackExchange Computer Science Q#3110, answer score: 11