Zhang, Linpeng; (2025) Quantitative Program Analysis: From Strongest Postconditions to Hyperproperties. Doctoral thesis (Ph.D), UCL (University College London).

Preview

Text Linpeng Zhang - PhD Thesis.pdf - Accepted Version Download (1MB) | Preview

Abstract

The main aim of this thesis is to provide a holistic comprehension of strongest-postcondition-style calculus and weakest-precondition-style calculus for quantitative program analysis. To achieve this goal, the thesis will present novel concepts that deepen the understanding of program correctness and incorrectness, paving the way for the creation of new program logics. For example, it will define new predicate transformers such as the strongest liberal post, along with their quantitative variants, and demonstrate their applications in Information Flow Analysis. Furthermore, by bridging the gap between quantitative forward and back- ward transformers, the thesis will progressively elevate the reasoning to a more general setting, making the calculi parametrized to a class of semirings. This parametrization will enable a deeper understanding of the fundamental relationships between forward and backward, correctness and incorrectness, as well as nontermination and unreachability. Finally, the thesis will delve into the study of hyperproperties and integrate predicate transformers reasoning into them, and beyond. It will demonstrate that their quantitative variants enable reasoning about hyperquantities, thus facilitating analyses involving expected values, variance, and other quantitative metrics. Moreover, the exploration of higher-order predicate transformers will provide insights into their limitations and advantages, allowing for the instantiation of simpler predicate transformers when reasoning about less complex properties.

Download activity - last month

Export as CSVJSONXML

Download activity - last 12 months

Export as JSONXMLCSV

Downloads by country - last 12 months

Export as CSVJSONXML

Archive Staff Only

View Item