Weakest Precondition Static Analysis for Stack Machines

Mirjam Iher
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.
Graduation Thesis language
Graduation Thesis type
Bachelor - Computer Science
Kalmer Apinis, PhD; Vesal Vojdani, PhD
Defence year