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.
Asked By : FELIPE N.
Answered By : Dave Clarke
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:
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/3110
0 comments:
Post a Comment
Let us know your responses and feedback