Projects per year
Abstract
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. Alternationfree 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 ALFPbased 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 multivalued model checking problems, we have proposed multivalued ALFP. A Moore Family result for multivalued ALFP is also established, which ensures the existence and uniqueness of the least model. When the truth values in multivalued ALFP constitute a nite distributive complete lattice, multivalued ALFP can be reduced to twovalued ALFP. This result enables to implement a solver for multivalued ALFP by reusing existing solvers for twovalued ALFP. Our ALFPbased technique developed for the twovalued CTL naturally generalizes to a multivalued setting, and we therefore obtain a multivalued analysis for temporal properties specied by CTL formulas. In particular, we have shown that the threevalued CTL model checking problem over Kripke modal transition systems can be exactly encoded in threevalued ALFP.
Last, we come back to twovalued 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 alternationfree μ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.
We focus on logical approaches to static analysis. Alternationfree 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 ALFPbased 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 multivalued model checking problems, we have proposed multivalued ALFP. A Moore Family result for multivalued ALFP is also established, which ensures the existence and uniqueness of the least model. When the truth values in multivalued ALFP constitute a nite distributive complete lattice, multivalued ALFP can be reduced to twovalued ALFP. This result enables to implement a solver for multivalued ALFP by reusing existing solvers for twovalued ALFP. Our ALFPbased technique developed for the twovalued CTL naturally generalizes to a multivalued setting, and we therefore obtain a multivalued analysis for temporal properties specied by CTL formulas. In particular, we have shown that the threevalued CTL model checking problem over Kripke modal transition systems can be exactly encoded in threevalued ALFP.
Last, we come back to twovalued 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 alternationfree μ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.
Original language  English 

Place of Publication  Kgs. Lyngby 

Publisher  Technical University of Denmark 
Number of pages  174 
Publication status  Published  2012 
Series  IMMPHD2012 

Number  280 
ISSN  09093192 
Fingerprint
Dive into the research topics of 'Model Checking as Static Analysis'. Together they form a unique fingerprint.Projects
 1 Finished

Combined Techniques of Static Analysis and Model Checking
Zhang, F., Nielson, F., Probst, C. W., Dam, M., Huth, M. & Nielson, H. R.
01/09/2009 → 22/11/2012
Project: PhD