The aim of this thesis is the verification of task schedulers for operating systems through static analysis based on abstract interpretation. Operating systems are collections of software present on almost every computer. Their purpose is to allow other programs to run without having to manage low-level problems such as memory.…
We present the article “Shape analysis by means of bi-abduction” by Cristiano Calcagno, Dino Distefano, Peter O’Hearn, Hongseok Yang published at POPL in 2009. This article addresses the problem of pre- & post-condition generation and verification for function analysis. In order to resolve this problem, the authors introduce the notion…
Traditional separation logic-based shape analyses utilize inductive summarizing predicates so as to capture general properties of the layout of data-structures, to verify accurate manipulations of, e.g., various forms of lists or trees. However, they also usually abstract away contents properties, so that they may only verify memory safety and invariance…
