Weakest Precondition Static Analysis for Stack Machines
Name
Mirjam Iher
Abstract
Static analysis is a way to inspect software. As opposed to dynamic analysis, code does not need to be executed in order to be analysed. This property allows for safer and more general analysis than dynamic analysis.
This thesis focuses on weakest precondition computation through a backwards
static analysis. To show the soundness of this approach, the programs to be analysed are modelled as memory-augmented stack machines. The advangate of the backwards method compared to traditional forward analyses is avoiding analysing inconsequential properties of the program's semantics during verification. As a practical contrubition of this thesis, the weakest precondition analysis is implemented in the Põder static analyisis framework.
This thesis focuses on weakest precondition computation through a backwards
static analysis. To show the soundness of this approach, the programs to be analysed are modelled as memory-augmented stack machines. The advangate of the backwards method compared to traditional forward analyses is avoiding analysing inconsequential properties of the program's semantics during verification. As a practical contrubition of this thesis, the weakest precondition analysis is implemented in the Põder static analyisis framework.
Graduation Thesis language
Estonian
Graduation Thesis type
Bachelor - Computer Science
Supervisor(s)
Kalmer Apinis, PhD; Vesal Vojdani, PhD
Defence year
2019