Computers have become ubiquitous in everyday life and so have bugs in programs running on those computers. Research in the field of programming languages and verification has produced countless ways to attack the problem of software defects. This thesis concerns itself with two established techniques being applied to an unconventional setting.

Firstly, in the category of extending the applicability of program verification to more realistic settings, we demonstrate how to verify high-performance algorithms and data structures making use of highly efficient memory access patterns that are not automatically synchronized with main memory or other processors’ caches. Hardware and programming languages that expose these weakly or un-synchronized memory accesses are said to have weak memory models. The lack of synchronization in weak memory models goes directly against the assumption of sequential consistency which still sits at the heart of most verification works. Concretely, we show how to perform verification in weak memory models using an existing program logic framework, Iris, that was traditionally limited to sequential consistency. In building on Iris, we inherit its mechanized proof of soundness of the core logic as well as the ability to perform mechanized program verification.

Secondly, we propose to bring the benefits of dependent types to the process of writing and automating proofs in the Rocq proof assistant. This aims to adress the limitations of Rocq's oldest — and, for a long time, only — tactic language: Ltac. Ltac's pitfalls are numerous and it is arguably unable to fulfill the requirements of large verification projects. Our contribution is a new tactic language called Mtac2. Mtac2 is based on Mtac, a principled metaprogramming language for Rocq offering strongly typed primitives based on Rocq’s own dependent type system. Mtac’s primitives could already be used to implement some tactics but it lacks the ability to directly interact with Rocq’s proof state and to perform backwards reasoning on it. Mtac2 extends Mtac with support for backwards reasoning and keeps in line with Mtac’s tradition of strong types by introducing the concept of typed tactics. Typed tactics statically track the expected type of the current goal(s) and can rule out entire classes of mistakes that often plague Ltac tactics.

The synthesis of logical controllers that guarantee desired specifications is a central problem in the design of cyber-physical systems (CPS). In practice, such guarantees rely on assumptions about how the controller interacts with its environment. These assumptions restrict environment behavior to make synthesis feasible, but in existing approaches they are often overly restrictive, leading to conservative designs and limiting the range of behaviors that systems can safely accommodate.

This thesis rethinks the role of assumptions in logical controller synthesis by emphasizing their \emph{permissiveness}---the ability to capture a wide range of admissible environment behaviors. We study permissive assumptions in two key settings: (a) interactions among multiple discrete components in distributed systems, and (b) interactions between high-level logical controllers and low-level physical dynamics in hybrid systems. In both settings, we develop theoretical and algorithmic foundations for computing and exploiting permissive assumptions to enable new design paradigms for logical controller synthesis.

For distributed systems, we define permissiveness as capturing all cooperative behaviors of other components that enable a controller to satisfy its specification. We present an algorithm for computing such assumptions in monolithic systems and extend it to distributed systems via a negotiation-based framework that iteratively constructs permissive assume-guarantee contracts for each component. These contracts enable decentralized synthesis and are applied to human-robot interaction, allowing robots to cooperate with humans whenever possible and request cooperation only when necessary.

For hybrid systems, we utilize permissive assumptions on the plant model---the abstract representation of physical dynamics---to address three key challenges. To enable seamless adaptation of controllers to changing logical contexts, i.e., changes in high-level goals or tasks, we introduce a novel synthesis framework that utilizes \emph{persistent live groups}, a class of assumptions capturing liveness properties of continuous dynamics. To improve scalability to large or uncertain plant models, we develop \emph{universal controllers} where decisions are conditioned on branching-time assumptions called \emph{prophecies}, which are learned from representative models and efficiently verified at runtime on unseen plant models. Finally, to enhance robustness under uncertainty or partial violations of assumptions on the plant model, we introduce a robust semantics for branching-time temporal logics, enabling formal reasoning about controller behavior under such violations.

Overall, this work enables correctness-by-construction synthesis while avoiding unnecessary conservatism, resulting in CPS that are more robust, scalable, and responsive.

Floating-point numbers often represent real numbers in computer systems. They are applicable in many domains, including embedded systems, machine learning, and scientific computing. Despite their widespread use, they pose some difficulties. Floating-point numbers and operations typically suffer from roundoff errors, making computations over floating-points inaccurate with respect to a real-valued specification. Moreover, the IEEE 754 floating-point standard, a fundamental element in formalizing floating-point arithmetic for today’s computers, presents additional challenges due to special values and resulting unintuitive behaviors. This thesis has three main contributions that address existing gaps in automated reasoning about floating-point arithmetic, making it easier for developers and researchers to understand, verify, and trust the floating-point computations in their programs. First, we introduce the first floating-point support in a deductive verifier for the Java programming language. Our support in the KeY verifier automatically handles floating-point arithmetic and transcendental functions. We achieve this with a combination of delegation to external SMT solvers on one hand, and rule-based reasoning within KeY on the other, exploiting the complementary strengths of both approaches. As a result, this approach can prove functional floating-point properties for realistic programs. Second, inspired by KeY’s treatment of method calls and the need for a scalable roundoff error analysis, we present the first modular optimization-based roundoff error analysis for non-recursive procedural floating-point programs. Our key idea is to achieve modularity while maintaining reasonable accuracy by automatically computing procedure summaries that are a function of the input parameters. Technically, we extend an existing optimization-based roundoff error analysis and show how to effectively use first-order Taylor approximations to compute precise procedure summaries, and how to integrate those to obtain end-to-end roundoff error bounds. Third, our experience using SMT solvers to discharge KeY’s floating-point verification conditions revealed unexpected performance behavior, motivating a systematic study of floating-point reasoning in SMT solvers. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values, to uncover unexpected performance behavior in SMT solvers’ handling of floating-point formulas, such as an increase in solving time when the SMT queries are simplified. Using real-world test inputs, our approach can identify such performance bugs for every SMT solver tested.

As users are exposed to an unprecedented range of security threats, a rich ecosystem of support mechanisms has emerged to assist the "last line of defense". Yet as these mechanisms become widely adopted in industry, a question arises: do they provide the support users actually need? In the first part of this talk, I will show that this is not always the case. Using phishing (one of the most prevalent and damaging cybercrimes) as a case study, I will present results from large-scale, real-world measurement studies that challenge common assumptions: that widely deployed mechanisms such as training and password managers are inherently effective, and that users primarily lack knowledge about this threat and how to detect it. Instead, I will show that phishing susceptibility is often an attention problem, due to limited and poorly surfaced indicators and cues. In the second part of the talk, I will discuss how we translate these insights into the design of novel systems that better support secure behavior. I will present a tailored countermeasure that assists users at critical decision points, and discuss its limitations in terms of increased user burden to introduce recent work on automating security decisions through AI-driven assistance. I will conclude by outlining key research challenges in designing security systems that are adaptive, context-aware, and robust.

Real-world AI systems must be robust across a wide range of conditions. One path to such robustness is if a model recovers a coherent structural understanding of its domain. But it is unclear how to measure, or even define, structural understanding. This talk will present theoretically-grounded definitions and metrics that test the structural recovery — or implicit "world models" — of generative models. We will propose different ways to formalize the concept of a world model, develop tests based on these notions, and apply them across domains. In applications ranging from testing whether LLMs apply logic to whether foundation models acquire Newtonian mechanics, we will see that models can make highly accurate predictions with incoherent world models. We will also connect these tests to a broader agenda of building generative models that are robust across downstream uses, incorporating ideas from statistics and the behavioral sciences. Developing reliable inferences about model behavior across tasks offer new ways to assess and improve the efficacy of generative models.

Online platforms increasingly rely on opaque content recommendation systems to curate personalized content. The black-box nature of these systems has raised significant societal concerns, such as formation of filter bubbles or promotion of extreme content. In response, regulatory bodies such as the European Commission have enacted digital regulations aimed at strengthening platform accountability and transparency. Achieving these goals requires audits of content recommendations and the mechanisms that govern them. To systematically audit personalized content recommendation systems deployed by online platforms, in this thesis we investigate their data gathering practices and transparency efforts. To this end, this thesis makes the following three contributions: First, it investigates personal data collection practices of online platforms, as these practices directly enable personalized content recommendations. Second, by employing sockpuppet accounts, it conducts an audit of transparency efforts implemented by online platforms through studying explanations provided for organic content recommendations. Finally, this thesis contributes to improving transparency in the procedures and objectives of recommendation systems deployed by online platforms.