Model Checking as Static Analysis

Both model checking and static analysis are prominent approaches to detecting software errors. Model Checking is a successful formal method for verifying properties specified in temporal logics with respect to transition systems. Static analysis is also a powerful method for validating program properties which can predict safe approximations to program behaviors. In this thesis, we have developed several static analysis based techniques to solve model checking problems, aiming at showing the link between static analysis and model checking.

We focus on logical approaches to static analysis. Alternation-free Least Fixed Point Logic (ALFP), an extension of Datalog, has been used as the specification language in most of our research results.

We have first considered the CTL model checking and developed an ALFP-based technique to solve the CTL model checking problem. We have shown that the set of states satisfying a CTL formula can be characterized as the least model of ALFP clauses specifying this CTL formula. The existence of the least model of ALFP clauses is ensured by the Moore Family property of ALFP. Then, we take fairness assumptions in CTL into consideration and have shown that CTL fairness problems can be encoded into ALFP as well.

To deal with multi-valued model checking problems, we have proposed multivalued ALFP. A Moore Family result for multi-valued ALFP is also established, which ensures the existence and uniqueness of the least model. When the truth values in multi-valued ALFP constitute a nite distributive complete lattice, multi-valued ALFP can be reduced to two-valued ALFP. This result enables to implement a solver for multi-valued ALFP by reusing existing solvers for twovalued ALFP. Our ALFP-based technique developed for the two-valued CTL naturally generalizes to a multi-valued setting, and we therefore obtain a multivalued analysis for temporal properties specied by CTL formulas. In particular, we have shown that the three-valued CTL model checking problem over Kripke modal transition systems can be exactly encoded in three-valued ALFP.

Last, we come back to two-valued settings and have considered the model checking for the modal μ-calculus. Our results have shown that ALFP suces to deal with the model checking problem for the alternation-free μ-calculus. However, to deal with the full fragment of the μ-calculus, we need to go beyond ALFP. Therefore, we proposed Succinct Fixed Point Logic (SFP), as an extension of ALFP. We have established a Moore Family result for SFP, which ensures the existence and uniqueness of the intended model of SFP. We have shown that SFP is well suited to specify nested xed points in the μ-calculus and the model checking problem for the μ-calculus can be encoded as the intended model of
SFP.

Our research results have strengthened the link between model checking and static analysis. This provides a theoretical foundation for developing a unied tool for both model checking and static analysis techniques.