A Succinct Approach to Static Analysis and Model Checking

Publication: ResearchPh.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).

Kgs. Lyngby : Technical University of Denmark, 2012. 187 p. (IMM-PHD-2012; No. 278).

Publication: ResearchPh.D. thesis – Annual report year: 2012

Harvard

Filipiuk, P, Nielson, HR & Nielson, F 2012, A Succinct Approach to Static Analysis and Model Checking. Ph.D. thesis, Technical University of Denmark, Kgs. Lyngby. IMM-PHD-2012, no. 278

APA

Filipiuk, P., Nielson, H. R., & Nielson, F. (2012). A Succinct Approach to Static Analysis and Model Checking. Kgs. Lyngby: Technical University of Denmark. (IMM-PHD-2012; No. 278).

CBE

Filipiuk P, Nielson HR, Nielson F 2012. A Succinct Approach to Static Analysis and Model Checking. Kgs. Lyngby: Technical University of Denmark. 187 p. (IMM-PHD-2012; No. 278).

MLA

Filipiuk, Piotr, Hanne Riis Nielson, and Flemming Nielson A Succinct Approach to Static Analysis and Model Checking Kgs. Lyngby: Technical University of Denmark. 2012. (IMM-PHD-2012; Journal number 278).

Vancouver

Filipiuk P, Nielson HR, Nielson F. A Succinct Approach to Static Analysis and Model Checking. Kgs. Lyngby: Technical University of Denmark, 2012. 187 p. (IMM-PHD-2012; No. 278).

Author

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

Kgs. Lyngby : Technical University of Denmark, 2012. 187 p. (IMM-PHD-2012; No. 278).

Publication: ResearchPh.D. thesis – Annual report year: 2012

Bibtex

@phdthesis{3f1c41853535491aa777ef6ab2d2c1fc,
title = "A Succinct Approach to Static Analysis and Model Checking",
publisher = "Technical University of Denmark",
author = "Piotr Filipiuk and Nielson, {Hanne Riis} and Flemming Nielson",
year = "2012",
series = "IMM-PHD-2012",

}

RIS

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 -