Invited Speakers

Abstract: Safety standards in domains such as automotive and aerospace demand traceability, change impact analysis, and regulatory compliance. Yet requirements remain numerous, interdependent, and written in natural language, so these analyses are manual and costly. This talk draws on three studies, two with industry partners, to show how large language models (LLMs) can help.

The studies present LEREDD, which detects dependencies between requirements and was evaluated at General Motors, and ProReFiCIA, which identifies the requirements affected by a change and was evaluated on a real satellite system. They also compare a trained classifier with an engineered prompt for tracing requirements to GDPR provisions. Across all three, LLMs work best as triage tools: they shrink the analyst’s search space by an order of magnitude while keeping most true links. The surrounding pipeline matters more than the bare model. The talk closes with open challenges for industrial adoption, notably audit-grade rationales and tool qualification.

Abstract: Neural language models, most notably transformers, are the backbone of today’s Large Language Models (LLMs). Although such models admit fast and parallelizable training algorithms, they are often not easily amenable to analysis. In contrast, a plethora of algorithms are available for analyzing automata-based models, but such models do not admit fast training algorithms. In this talk, I will survey the growing area of FLaNN (Formal Languages and Neural Networks), which attempts to bridge these two classes of models. In particular, I will illustrate how automata theory has been used successfully to analyze various neural architectures. In addition, I will describe recent work on verifying “transformer programs”, which are automata-based models that capture transformers. Finally, I will discuss the challenge of producing fast and reliable code from examples using both neural language models and automata-based models.

Abstract: The trustworthiness of intelligent systems ultimately depends on the correctness of the underlying code. However, for a long time, the development of system software and formal verification have remained separate, resulting in high barriers and low efficiency. In this talk, I will introduce C*, a systems programming language designed to integrate development and proof: it embeds formal proofs directly into the C language, enabling code and proofs to be tightly coupled and to evolve synchronously during system development, thereby achieving "development as proof" and significantly lowering the barriers and costs of formal verification for system software. I will discuss the key design ideas, current progress, and open problems for future research.