Low-level code written in languages like C forms the bedrock of most computer systems today. Establishing the correctness of this code is important for the safety and security of our systems. The gold standard for code correctness is foundational verification -- the construction of mathematical proofs of program correctness verified in a proof assistant like Coq. However, foundational verification of low-level code is a tedious task that has, so far, largely relied on adapting code to suit the constraints of the verification framework, e.g., the programming idioms that are supported.

In this talk, I will present RefinedC, a new Coq-based C verification framework that aims to address the above limitation. By design, RefinedC is foundational (all proofs are mechanically verified within Coq), extensible (it can be extended to support new program properties, programming idioms and even new languages) and automation-friendly. Time permitting, I will also discuss projects that extend RefinedC's capabilities to reason about code written in other low-level languages like assembly, and code written in more than one language.

(This talk is based on joint work with several other research groups, notably the group of Derek Dreyer at MPI-SWS.)

Large language models (LLMs) currently dominate AI. They exhibit impressive, often human-like, behavior across a wide range of linguistic and non-linguistic tasks. However, LLMs are the result of a combination of clever engineering and financial investment, rather than a result of rigorous scientific or theoretical study. Thus, very little is known about how or why LLMs exhibit the behaviors that they do. As a result, LLMs often seem mysterious and unpredictable. In this talk, I will discuss recent work which seeks to characterize the mechanisms that LLMs employ in terms of higher-level data structures and algorithms. Using results on a series of simple tasks, I will argue that LLMs are not as inscrutable as they seem, but rather make use of simple and often modular computational components to solve complex problems.

In cyber-physical systems research, a significant challenge is synthesizing reliable controllers that meet general temporal specifications. These controllers must offer formal guarantees against various sources of disturbances. Efficient formal controller design opens up numerous exciting applications across different domains, including the autonomous vehicle industry, energy systems, and healthcare. In this talk, I will discuss formal controller synthesis for three different classes of dynamical systems. First, I will address our contributions to improving the scalability of abstraction-based controller design methods for dynamical systems with continuous state spaces and bounded uncertainty. These contributions include: (1) a data-driven scheme for relaxing the requirement of having analytical model, (2) a neural abstraction method to lower memory requirements of both synthesis and deployment, and (3) a scalable method for solving reach-avoid problems for multi-agent systems. Second, I will briefly describe our contributions to time-bounded model checking for continuous-time Markov decision processes, specifically: (1) a conditional decidability result, and (2) a systematic method for improving the scalability of numerical approximation methods. Finally, I will briefly discuss our results related to the decidability of reachability-related problems for linear dynamical systems, which include: (1) a hardness result for point-to-point reachability of linear dynamical systems with hyper-rectangular control sets, and (2) decidability of pseudo-reachability for hyperplane target sets.