TY - BOOK

T1 - A Succinct Approach to Static Analysis and Model Checking

A1 - Filipiuk,Piotr

AU - Filipiuk,Piotr

A2 - Nielson,Hanne Riis

A2 - Nielson,Flemming

ED - Nielson,Hanne Riis

ED - Nielson,Flemming

PB - Technical University of Denmark

PY - 2012

Y1 - 2012

N2 - 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. <br/><br/>First, we present a Lattice based Least Fixed Point Logic (LLFP) that allows<br/>interpretations over complete lattices satisfying Ascending Chain Condition. We establish a Moore Family result for LLFP that guarantees that there always is<br/>single best solution for a problem under consideration. We also develop a solving algorithm, based on a dierential worklist, that computes the least solution<br/>guaranteed by the Moore Family result. <br/><br/>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. <br/><br/>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. <br/><br/>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.

AB - 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. <br/><br/>First, we present a Lattice based Least Fixed Point Logic (LLFP) that allows<br/>interpretations over complete lattices satisfying Ascending Chain Condition. We establish a Moore Family result for LLFP that guarantees that there always is<br/>single best solution for a problem under consideration. We also develop a solving algorithm, based on a dierential worklist, that computes the least solution<br/>guaranteed by the Moore Family result. <br/><br/>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. <br/><br/>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. <br/><br/>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.

BT - A Succinct Approach to Static Analysis and Model Checking

T3 - IMM-PHD-2012

T3 - en_GB

ER -