## A Succinct Approach to Static Analysis and Model Checking

Publication: Research › Ph.D. thesis – Annual report year: 2012

### Standard

**A Succinct Approach to Static Analysis and Model Checking.** / Filipiuk, Piotr; Nielson, Hanne Riis (Main supervisor); Nielson, Flemming (Supervisor).

Publication: Research › Ph.D. thesis – Annual report year: 2012

### Harvard

*A Succinct Approach to Static Analysis and Model Checking*. Ph.D. thesis, Technical University of Denmark, Kgs. Lyngby. IMM-PHD-2012, no. 278

### APA

*A Succinct Approach to Static Analysis and Model Checking*. Kgs. Lyngby: Technical University of Denmark. (IMM-PHD-2012; No. 278).

### CBE

### MLA

*A Succinct Approach to Static Analysis and Model Checking*Kgs. Lyngby: Technical University of Denmark. 2012. (IMM-PHD-2012; Journal number 278).

### Vancouver

### Author

### Bibtex

}

### RIS

TY - BOOK

T1 - A Succinct Approach to Static Analysis and Model Checking

AU - Filipiuk,Piotr

A2 - Nielson,Hanne Riis

A2 - Nielson,Flemming

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.

M3 - Ph.D. thesis

BT - A Succinct Approach to Static Analysis and Model Checking

PB - Technical University of Denmark

ER -