Program analysis techniques for algorithmic complexity and relational properties

Analyzing standard safety properties of a given program has traditionally been the primary focus of the program analysis community. Unfortunately, there are still many interesting analysis tasks that cannot be effectively expressed with standard safety properties. One such example is to derive the asymptotic complexity of a given program. Another example is to verify relational properties, i.e. properties that must be satisfied jointly by multiple programs of multiple runs of one program. Existing program analysis techniques for standard safety properties are usually not immediately applicable to asymptotic complexity analysis problems and relational verification problems. New approaches are therefore needed to solve these unconventional problems.

This thesis studies techniques for algorithmic complexity analysis as well as relational verification. To that end, we present three case studies: (1) We propose a new fuzzing technique for automatically finding inputs that trigger a program's worst-case resource usage. (2) We show how to build a scalable, end-to-end side channel detection tool by combining static taint analysis and a program logic designed for verifying non-interference of a given program. (3) We propose a general and effective relational verification algorithm that combines reinforcement learning with backtracking search. A common theme among all these solutions is to exploit problem-specific structures and adapt existing techniques to exploit those structures accordingly.