Projects per year
Abstract
In a number of areas software correctness is crucial, therefore it is often desirable to formally verify the presence of various properties or the absence of errors. This thesis presents a framework for concisely expressing static analysis and model checking problems. The framework facilitates rapid prototyping of new analyses and consists of variants of ALFP logic and associated solvers.
First, we present a Lattice based Least Fixed Point Logic (LLFP) that allows
interpretations over complete lattices satisfying Ascending Chain Condition. We establish a Moore Family result for LLFP that guarantees that there always is
single best solution for a problem under consideration. We also develop a solving algorithm, based on a dierential worklist, that computes the least solution
guaranteed by the Moore Family result.
Furthermore, we present a logic for specifying analysis problems called Layered Fixed Point Logic. Its most prominent feature is the direct support for both inductive computations of behaviors as well as coinductive specications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worstcase time complexity result. We develop a BDDbased solving algorithm, which computes the least solution guaranteed by the Moore Family result with worstcase time complexity as given by the complexity result.
We also present magic set transformation for ALFP, known from deductive databases, which is a clauserewriting strategy for optimizing query evaluation. In order to compute the answer to a query, the original ALFP clauses are rewritten at compile time, and then the rewritten clauses are evaluated bottomup. It is usually more eciently than computing entire solution followed by selection ii of the tuples of interest, which was the case in the classical formulation of ALFP logic.
Finally, we show that the logics and the associated solvers can be used for rapid prototyping. We illustrate that by a variety of case studies from static analysis and model checking.
First, we present a Lattice based Least Fixed Point Logic (LLFP) that allows
interpretations over complete lattices satisfying Ascending Chain Condition. We establish a Moore Family result for LLFP that guarantees that there always is
single best solution for a problem under consideration. We also develop a solving algorithm, based on a dierential worklist, that computes the least solution
guaranteed by the Moore Family result.
Furthermore, we present a logic for specifying analysis problems called Layered Fixed Point Logic. Its most prominent feature is the direct support for both inductive computations of behaviors as well as coinductive specications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worstcase time complexity result. We develop a BDDbased solving algorithm, which computes the least solution guaranteed by the Moore Family result with worstcase time complexity as given by the complexity result.
We also present magic set transformation for ALFP, known from deductive databases, which is a clauserewriting strategy for optimizing query evaluation. In order to compute the answer to a query, the original ALFP clauses are rewritten at compile time, and then the rewritten clauses are evaluated bottomup. It is usually more eciently than computing entire solution followed by selection ii of the tuples of interest, which was the case in the classical formulation of ALFP logic.
Finally, we show that the logics and the associated solvers can be used for rapid prototyping. We illustrate that by a variety of case studies from static analysis and model checking.
Original language  English 

Place of Publication  Kgs. Lyngby 

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

Number  278 
ISSN  2012268 
Fingerprint Dive into the research topics of 'A Succinct Approach to Static Analysis and Model Checking'. Together they form a unique fingerprint.
Projects
 1 Finished

Static Analysis and Model Checking of Software Systems
Filipiuk, P., Nielson, F., Probst, C. W., Schmidt, D. A., Seidl, H. & Nielson, H. R.
Technical University of Denmark
01/08/2009 → 25/10/2012
Project: PhD