ABSTRACT. The trustworthiness of intelligent systems ultimately depends on the correctness of the underlying code. However, the development of system software and formal verification have long 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.

ABSTRACT. The temporal logic of actions (TLA) is widely used for specifying and verifying concurrent systems. It comes with a formal proof system and a rigorously defined semantics suitable for foundational reasoning. However, no existing formalization of TLA has completely captured the key features of TLA that are essential for enabling verification of complicated concurrent systems across different levels of abstraction, including meta-properties like invariance under stuttering, refinement reasoning, and flexible existential quantification. By overcoming the challenges facing the formalization of those key features, we provide a complete embedding of TLA in Rocq with explicit syntax and proof system. We prove its essential meta-properties such as invariance under stuttering and the soundness of all of its proof rules. We demonstrate that our embedding have the same verification power as the original TLA while generating foundational proofs by formalizing the two examples in the original paper of TLA. To the best of our knowledge, ours is the first complete formalization of TLA in a foundational prover.

ABSTRACT. Controlled information flow between partitions is a fundamental security assurance for OS kernels in safety- and security-critical systems. Information-flow verification of OS kernels can be achieved by proving unwinding conditions at the specification level and transferring these guarantees to the implementation through refinement. Existing approaches further reduce the verification effort via sound proof systems for specification-level unwinding conditions. However, multi-core, preemptive OS kernels introduce new challenges for such verification. This paper presents an information-flow proof system for preemptive kernel specifications that soundly enforces the unwinding conditions required for OS security. The proof system enables modular verification by reasoning about individual specification statements of kernel APIs and interrupt handlers, using rely-guarantee conditions to capture interference in concurrent executions. We evaluate the effectiveness of the proof system on a synthetic model of a partitioned, preemptive OS kernel featuring core functionalities for task management, scheduling, and communication.

ABSTRACT. The completeness theorem for first-order logic is a benchmark for mechanized metatheory, and formalizations exist in several proof assistants. Existing developments typically represent binding by de Bruijn indices, omit logical equality, or both. This paper presents a Rocq formalization of the Gödel completeness theorem for first-order logic over a countable language, formulated as a named-variable Hilbert-style system with equality as a primitive, following the Henkin construction of standard textbooks. Three components are developed as reusable infrastructure. The MapC framework replaces language extension by reindexing within the countable constant supply. Preservation of axioms and derivability holds for an arbitrary index map, and satisfiability is recovered whenever the map admits a left inverse, with parity-based allocation of Henkin witnesses as the instance used. A countability chain handles arity-indexed dependent vectors and supplies the enumeration the construction requires. A formula rank serves both as the stratification for that argument and as the induction measure for the truth lemma. Logical equality forces a canonical model over terms quotiented by provable equality, with the well-definedness obligations this entails. The development is machine-checked and publicly available.

ABSTRACT. Active model learning is a crucial technique for automatically constructing formal models of black-box timed systems. However, existing learning approaches typically construct a single monolithic automaton for a timed system with multiple synchronous components, obscuring its component structure and hindering component-level analysis. We propose a compositional learning approach that constructs a deterministic real-time automaton (RTA) for each component with access only to the target system as a whole. Upon termination, the learned RTAs form a network that exhibits exactly the same timed behaviors as the target system. Within the respective resource limits, our implementation terminates successfully on 213 of the 240 (88.8%) randomly generated benchmark instances and all six adapted case-study benchmarks, and requires less learning time than monolithic approaches on some instances.

ABSTRACT. Probabilistic timed automata extend the classical timed automata formalism with discrete probabilistic choice over edges. We consider the case of the verification of a combination of multiple objectives of probabilistic timed automata, where the objectives can be non-probabilistic (referring to sure satisfaction along all behaviors) and probabilistic (referring to a probability threshold), and refer to reachability or \omega-regular properties on executions expressed using parity conditions. We show that existing algorithms for multiple objectives for finite-state Markov decision processes can be applied, using the classical region-graph construction, to obtain algorithms for the corresponding objectives of probabilistic timed automata. In particular, the verification of a probabilistic timed automata against multiple probabilistic-threshold parity objectives subject to the almost-sure divergence of time is EXPTIME-complete, while verification against the combination of sure properties, including sure divergence of time, and a single probabilistic-threshold parity objectives is in NEXPTIME and coNEXPTIME.

ABSTRACT. Compilers for synchronous dataflow languages such as Lustre are critical components in the development of safety-critical embedded systems. Although formal verification has been applied to several Lustre compilers, practical assurance remains challenging because verified translation stages may rely on incomplete semantic specifications, while unverified front-end stages can still introduce defects. Consequently, there is still no unified testing and assurance framework specifically designed for Lustre compilers. We present SCALC, a safety-case-guided assurance framework for Lustre compiler validation. SCALC uses structured safety cases to derive assurance goals, select validation activities, and organize the resulting evidence, integrating four complementary techniques: LLM-assisted generation of test programs targeted at specific assurance goals, manual review of translation rules, differential testing between independently developed Lustre compilers, and bounded functional equivalence checking of generated C code. We evaluate SCALC on the open-source L2C compiler and identify seven defects and two unsupported language features across multiple translation stages, including one defect in a Coq-verified part of the pipeline. These results show that SCALC can expose practical assurance gaps in partially verified compilers and provide traceable evidence for improving compiler reliability in safety-critical domains.

ABSTRACT. For heterogeneous networks, multiple technology stacks are simultaneously competing. For these stacks, both ASN.1 and YANG, are popular choices to define data models for protocols and communication messages. However, converting ASN.1 data model source code to YANG data model source code, also known as transpilation, would help reduce the interoperability issues between stacks and improve performance. For example, in the area of vehicular networks, models for Cooperative Awareness Messages (CAMs) can be transpiled to their YANG models. This helps CAMs leverage faster encoding made available by their YANG model. However, this transpilation needs to be verified for preserving the meaning of the data. Hence, this paper proposes a formal framework based on institutions for transpilation between two data modelling languages and the sufficient conditions for semantic preservation. Moreover, we apply this framework to a use case in vehicular communication by transpiling CAM model containing ASN.1 types with CafeOBJ-based proofs for preserving semantics.

ABSTRACT. In this paper, we propose a hybrid framework for Satisfiability Modulo the Theory of Nonlinear Real Arithmetic (SMT-NRA for short). First, we introduce a two-dimensional cell-jump move, called \emph{2D-cell-jump}, generalizing the key operation, cell-jump, of the local search method for SMT-NRA. In contrast to the existing cell-jump, which updates assignments exclusively along a given line, the 2D-cell-jump enables search over an arbitrarily selected plane. Then, we propose an extended local search framework, named \emph{2D-LS} (following the existing local search framework, LS, for SMT-NRA). Finally, we present a hybrid framework for SMT-NRA integrating 2D-LS, MCSAT and OpenCAD, to improve search efficiency through information exchange. The experimental results demonstrate improvements in local search performance, highlighting the effectiveness of the proposed methods.

ABSTRACT. Hardware model checking increasingly relies on portfolios of verification tools, engines, and configurations, because no single verifier is consistently best for all verification instances. Selecting an effective verifier is therefore important for reducing verification time, but exist ing verifier selectors mainly rely on fixed statistical representations and pairwise ranking, while directly learning from benchmark instances is difficult due to the limited number of labeled instances available. In this work, we propose Caster (Cost-Aware Selection of Tools, Engines, and Run Configurations), for selecting proper verifiers for BTOR2 instances. Caster is a two-stage cost-aware selection framework that separates structural representation learning from verifier-specific cost prediction. It first employs an Instance-Embedding graph neural network (GNN), denoted as IE-GNN, to learn a verifier-independent embedding from de pendency graphs of benchmark BTOR2 instances, with solvability and runtime cost as the training objective. It then trains a gradient boost ing decision tree (GBDT) from the embeddings and lightweight features of benchmark BTOR2 instances together with their verifier identities for predicting log-PAR-2 cost of each instance-verifier pair. We evaluate Caster on Btor2-Select’s two public BV and ARR datasets and one ric3 dataset curated using 1,936 BTOR2 instances and 130 verifiers spanning IC3, BMC, and k-induction (resulting in 251,680 instance-verifier pairs). Caster achieves the best Top-3 and Top-5 closed-gap result among the evaluated methods on all three datasets: especially 92.69% on BV, 91.13% on ARR, and 79.43% on ric3 in Top-5. These results indicate that Caster can improve portfolios even in the small-data regime.

ABSTRACT. Register allocation is one of the oldest and most classical problems in compiler optimization. We have a limited number of registers and, given a program $P,$ our goal is to assign each of the variables in $P$ to a register, ensuring that no two variables with intersecting live-ranges are stored in the same register. This leads to a tradeoff between live-range splitting and copy coalescing. Live-range splitting breaks a variable into several parts, allowing each part to be assigned a different register, but also causing overhead due to new copying/shuffling operations between the parts. Copy coalescing does the opposite. If a variable $x$ is copied into $y,$ one can avoid the copy/shuffle as long as both $x$ and $y$ are assigned to the same register, but this increases the register pressure and might cause spilling. If we do not allow splitting and coalescing, the problem is equivalent to graph coloring and hence NP-hard. On the other hand, if we forbid coalescing and convert the program to SSA, i.e.~applying maximum splitting, then register allocation is solvable in polynomial time, but the shuffle-code overhead would be prohibitively high. If we start with an SSA program and allow coalescing, the problem again becomes NP-hard.

In this work, we consider the problem of optimal spill-free register allocation on structured programs. We rely on the celebrated result of Thorup that control-flow graphs of structured programs have bounded treewidth. Our main contribution is a bound on the treewidth of $I \cup A$ where $I$ is the interference graph between variables and $A$ is the affinity graph modeling potential coalescings. We then use the treewidth of $I \cup A$ as a novel parameter to design a linear-time FPT algorithm for register allocation with copy coalescing. We do not directly consider live-range splitting in our approach. However, converting the program to SSA and then applying our algorithm would find an optimal register allocation with both splitting and coalescing, thus solving the most general variant of the problem.

ABSTRACT. Data sequences, such as time series, traces, and sensor streams, are words over large or infinite data domains. Their properties often depend on comparisons between values at different positions, which finite automata cannot express directly. We study synthesis and verification for Deterministic Register Automata (DRAs) over ordered data sequences. DRAs combine finite control with registers for remembered data values, providing compact symbolic descriptions of quantitative sequence languages. Our technical core is a local-search synthesis procedure and an exact robustness checker for DRAs. We fix the alphabet theory to ordered rationals $(\Q;<,=)$ with rational guard constants and use non-negative affine accumulator costs. For a fixed number of DRA registers, the checker runs in polynomial time; its dependence on that number is exponential. It reduces robustness to coverability and then to a shortest-path problem. Since the search ranges over $\Q^+$, it produces variable-length witnesses and, for RAA-definable alignment costs such as DTW, explores a counterexample space with no a priori length bound. As an application, we use learned DRAs as interpretable surrogates for queried neural sequence classifiers. A probably approximately correct (PAC) validation loop refines rejected candidates, returns genuine non-robustness witnesses for the classifier when found, and accepts a surrogate only with statistical guarantees for fidelity and local stability. We implement the framework in \textit{RAExc}, enabling the synthesis of interpretable automata and the verification of their robustness. We evaluate the approach on benchmark languages and sequentialized MNIST, demonstrating high accuracy while verifying the robustness of the learned automata.