ETD

• Axiomatic proof systems
• Formal verification
• Precision in static analysis
• Program behavior semantics

Program analysis has long struggled with the challenge of understanding program behavior from multiple perspectives, each offering partial yet complementary insights. In this thesis, we study the principles of a unified program logic that can embed all previous correctness and incorrectness analyses, improve precision in program analysis and reduce the current fragmentation of program logics, like Hoare Logic, Incorrectness Logic, Necessary Conditions, and Separation Incorrectness Logic each aimed to different goals. We propose an intuitive and expressive notation that is capable of expressing all corresponding kinds of triples, as well as highlighting the absence of false positives/negatives in the analysis, whenever possible. In turn, it has the potential to provide more informative code summaries for compositional reasoning over large codebases.