Program Analysis as Model Checking

Bidragets oversatte titel: Program Analyse som Model Checking

Mads Chr. Olesen

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

4 Citationer (Scopus)
185 Downloads (Pure)

Resumé

Software programs are proliferating throughout modern life, to a point where even the simplest appliances such as lightbulbs contain software, in addition to the software embedded in cars and airplanes. The correct functioning of these programs is therefore of the utmost importance, for the quality and sustenance of life. Due to the complexity inherent in the software it can be very difficult for the software developer to guarantee the absence of errors; automated support in the form of automated program analysis is therefore essential.

Two methods have traditionally been proposed: model checking and abstract interpretation. Model checking views the program as a finite automaton and tries to prove logical properties over the automaton model, or present a counter-example if not possible — with a focus on precision. Abstract interpretation translates the program semantics into abstract semantics efficiently represented as a lattice structure, and tries to use the
invariants given by the lattice element to prove the absence of errors — with a focus on efficiency.

Previous work has argued that on a theoretical level the two methods are converging, and one method can indeed be used to solve the same problems as the other by a reformulation. This thesis argues that there is even a convergence on the practical level, and that a generalisation of the formalism of timed automata into lattice automata captures key aspects of both methods; indeed model checking timed automata can be formulated in terms of an abstract interpretation.

For the generalisation to lattice automata to have benefit it is important that efficient tools exist. This thesis presents multi-core tools for efficient and scalable reachability and Büchi emptiness checking of timed/lattice automata.

Finally, a number of case studies are considered, among others numerical analysis of c programs, and worst-case execution time analysis of ARM programs. It is shown how lattice automata allow automatic and manual tuning of the precision and efficiency of the verification procedure. In the case of worst-case execution time analysis a sound overapproximation of the hardware is needed; the case of identifying timing anomalous hardware for which such abstractions are hard to find is considered.
OriginalsprogEngelsk
ForlagInstitut for Datalogi, Aalborg Universitet
Antal sider159
StatusUdgivet - 1 sep. 2014
NavnPublication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University
Nummer85
ISSN1601-0590

Fingerprint

Model checking
Semantics
Hardware
Embedded software
Finite automata
Numerical analysis
Railroad cars
Tuning
Aircraft
Acoustic waves

Citer dette

Olesen, M. C. (2014). Program Analysis as Model Checking. Institut for Datalogi, Aalborg Universitet. Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University, Nr. 85
Olesen, Mads Chr. / Program Analysis as Model Checking. Institut for Datalogi, Aalborg Universitet, 2014. 159 s. (Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University; Nr. 85).
@phdthesis{956c3de8815f4647955fa777c7223938,
title = "Program Analysis as Model Checking",
abstract = "Software programs are proliferating throughout modern life, to a point where even the simplest appliances such as lightbulbs contain software, in addition to the software embedded in cars and airplanes. The correct functioning of these programs is therefore of the utmost importance, for the quality and sustenance of life. Due to the complexity inherent in the software it can be very difficult for the software developer to guarantee the absence of errors; automated support in the form of automated program analysis is therefore essential.Two methods have traditionally been proposed: model checking and abstract interpretation. Model checking views the program as a finite automaton and tries to prove logical properties over the automaton model, or present a counter-example if not possible — with a focus on precision. Abstract interpretation translates the program semantics into abstract semantics efficiently represented as a lattice structure, and tries to use theinvariants given by the lattice element to prove the absence of errors — with a focus on efficiency.Previous work has argued that on a theoretical level the two methods are converging, and one method can indeed be used to solve the same problems as the other by a reformulation. This thesis argues that there is even a convergence on the practical level, and that a generalisation of the formalism of timed automata into lattice automata captures key aspects of both methods; indeed model checking timed automata can be formulated in terms of an abstract interpretation.For the generalisation to lattice automata to have benefit it is important that efficient tools exist. This thesis presents multi-core tools for efficient and scalable reachability and B{\"u}chi emptiness checking of timed/lattice automata.Finally, a number of case studies are considered, among others numerical analysis of c programs, and worst-case execution time analysis of ARM programs. It is shown how lattice automata allow automatic and manual tuning of the precision and efficiency of the verification procedure. In the case of worst-case execution time analysis a sound overapproximation of the hardware is needed; the case of identifying timing anomalous hardware for which such abstractions are hard to find is considered.",
author = "Olesen, {Mads Chr.}",
year = "2014",
month = "9",
day = "1",
language = "English",
series = "Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University",
number = "85",
publisher = "Institut for Datalogi, Aalborg Universitet",
address = "Denmark",

}

Olesen, MC 2014, Program Analysis as Model Checking. Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University, nr. 85, Institut for Datalogi, Aalborg Universitet.

Program Analysis as Model Checking. / Olesen, Mads Chr.

Institut for Datalogi, Aalborg Universitet, 2014. 159 s. (Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University; Nr. 85).

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

TY - BOOK

T1 - Program Analysis as Model Checking

AU - Olesen, Mads Chr.

PY - 2014/9/1

Y1 - 2014/9/1

N2 - Software programs are proliferating throughout modern life, to a point where even the simplest appliances such as lightbulbs contain software, in addition to the software embedded in cars and airplanes. The correct functioning of these programs is therefore of the utmost importance, for the quality and sustenance of life. Due to the complexity inherent in the software it can be very difficult for the software developer to guarantee the absence of errors; automated support in the form of automated program analysis is therefore essential.Two methods have traditionally been proposed: model checking and abstract interpretation. Model checking views the program as a finite automaton and tries to prove logical properties over the automaton model, or present a counter-example if not possible — with a focus on precision. Abstract interpretation translates the program semantics into abstract semantics efficiently represented as a lattice structure, and tries to use theinvariants given by the lattice element to prove the absence of errors — with a focus on efficiency.Previous work has argued that on a theoretical level the two methods are converging, and one method can indeed be used to solve the same problems as the other by a reformulation. This thesis argues that there is even a convergence on the practical level, and that a generalisation of the formalism of timed automata into lattice automata captures key aspects of both methods; indeed model checking timed automata can be formulated in terms of an abstract interpretation.For the generalisation to lattice automata to have benefit it is important that efficient tools exist. This thesis presents multi-core tools for efficient and scalable reachability and Büchi emptiness checking of timed/lattice automata.Finally, a number of case studies are considered, among others numerical analysis of c programs, and worst-case execution time analysis of ARM programs. It is shown how lattice automata allow automatic and manual tuning of the precision and efficiency of the verification procedure. In the case of worst-case execution time analysis a sound overapproximation of the hardware is needed; the case of identifying timing anomalous hardware for which such abstractions are hard to find is considered.

AB - Software programs are proliferating throughout modern life, to a point where even the simplest appliances such as lightbulbs contain software, in addition to the software embedded in cars and airplanes. The correct functioning of these programs is therefore of the utmost importance, for the quality and sustenance of life. Due to the complexity inherent in the software it can be very difficult for the software developer to guarantee the absence of errors; automated support in the form of automated program analysis is therefore essential.Two methods have traditionally been proposed: model checking and abstract interpretation. Model checking views the program as a finite automaton and tries to prove logical properties over the automaton model, or present a counter-example if not possible — with a focus on precision. Abstract interpretation translates the program semantics into abstract semantics efficiently represented as a lattice structure, and tries to use theinvariants given by the lattice element to prove the absence of errors — with a focus on efficiency.Previous work has argued that on a theoretical level the two methods are converging, and one method can indeed be used to solve the same problems as the other by a reformulation. This thesis argues that there is even a convergence on the practical level, and that a generalisation of the formalism of timed automata into lattice automata captures key aspects of both methods; indeed model checking timed automata can be formulated in terms of an abstract interpretation.For the generalisation to lattice automata to have benefit it is important that efficient tools exist. This thesis presents multi-core tools for efficient and scalable reachability and Büchi emptiness checking of timed/lattice automata.Finally, a number of case studies are considered, among others numerical analysis of c programs, and worst-case execution time analysis of ARM programs. It is shown how lattice automata allow automatic and manual tuning of the precision and efficiency of the verification procedure. In the case of worst-case execution time analysis a sound overapproximation of the hardware is needed; the case of identifying timing anomalous hardware for which such abstractions are hard to find is considered.

M3 - Ph.D. thesis

T3 - Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University

BT - Program Analysis as Model Checking

PB - Institut for Datalogi, Aalborg Universitet

ER -

Olesen MC. Program Analysis as Model Checking. Institut for Datalogi, Aalborg Universitet, 2014. 159 s. (Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University; Nr. 85).