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",
author = "Piotr Filipiuk and Nielson, {Hanne Riis} and Flemming Nielson",
year = "2012",
publisher = "Technical University of Denmark",

}

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

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

M3 - Ph.D. thesis

BT - A Succinct Approach to Static Analysis and Model Checking

PB - Technical University of Denmark

ER -