Current tools for pattern matching computer programs often operate on abstract syntax trees or other static representations of programs. These approaches, though efficient, are fundamentally limited when it comes to capturing the dynamic behavior of programs. For example, it is not always possible to express (concise) syntactic patterns that capture programs which are semantically equivalent but differ in their syntactic representation. A tool that takes into account the behavior (or dynamic semantics) of programs would be able to capture programs that are semantically equivalent in a more concise manner with a single pattern. Additionally, taking into account program behavior leads to more precise pattern matching, by excluding unreachable paths of computation. In this thesis, we explore a novel method, based on behavioral models of programs, that allows patterns to take into account the dynamic semantics of a program. We propose the Dyno pattern language, in which concrete object language syntax can be used to express intuitive semantic patterns of programs. Pattern matching is performed by translating Dyno patterns to μ-calculus formulas and model checking these formulas against models extracted from object programs. Because our method is based on dynamic models of programs, we are fundamentally limited by the halting problem. In favor of precision, our method compromises on efficiency and termination guarantees. In particular, termination is not guaranteed when the extracted model of a program has infinitely many states. To recover termination in some cases, we provide the facility to express bounds on input parameters, limiting the search space while compromising on soundness. We recognize some limitations in our work, including a lack of match evidence (e.g. the location of a match in the object program’s syntax tree), as well as holes in Dyno’s expressiveness. To address the latter issue, we suggest operators that could be added to Dyno in the future.

With widespread use of advanced technology for the recording, storing and sharing of social interactions, protecting privacy of people has been a growing concern. This paper zooms in on the collection of spoken audio with regard for the privacy of recorded individuals. Recently efforts have been made to collect audio at a low sampling rate to obfuscate spoken words in the recorded audio, such that conversations are kept private. This research investigates whether it is possible to upsample this low-resolution audio, using an existing super-resolution model, in order to reveal parts of the previously obfuscated conversations. The performance of the model is measured in terms of the word error rate of automatically generated transcriptions of the upsampled audio. It turns out that it is possible to significantly increase the intelligibility of low resolution privacy-sensitive audio by upsampling. Though the use of the super-resolution model seems to be limited when it comes to revealing significant parts of conversations.