A Succinct Approach to Static Analysis and Model Checking

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 co-inductive specications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worst-case time complexity result. We develop a BDD-based solving algorithm, which computes the least solution guaranteed by the Moore Family result with worst-case time complexity as given by the complexity result.

We also present magic set transformation for ALFP, known from deductive databases, which is a clause-rewriting 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 bottom-up. 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.