Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large language models (LLMs) have demonstrated impressive capabilities in theorem proving and verified code generation, how powerful they truly are in generating program specifications remains unclear. Existing evaluations require either verifying implementation conformance or proving semantic equivalence between specifications, both are formidably difficult, yielding sparse and often inconclusive results about specification quality. To address this problem, we introduce Coins, a Coq-based evaluation framework that assesses specification quality through provable behavioral correctness on instantiated test cases. This design aligns the evaluation with the asymmetric nature of formal reasoning, where successful proofs provide reliable evidence while proof failures are inherently ambiguous. Using Coins, we conduct a large-scale empirical study of specification generation on HumanEval, supported by a curated set of human-written Coq specifications. Our results show that even generating specifications remains a formidable challenge, and that verification complexity substantially obscures genuine differences in specification quality. Overall, we find that accurately evaluating specifications—rather than increasing model capacity alone—is the central challenge in understanding the power of LLMs for specification synthesis, and that the test-case--based formal reasoning offers a more faithful and discriminative measure of progress.

MARS is a toolchain, supporting model-based design of cyber-physical systems (CPS), which integrates informal and formal design. With MARS, a system under development can be graphically modeled by the combination of AADL and Simulink/Stateflow, then the analysis of the graphical model can be conducted via simulation. Furthermore, the graphical model can be automatically transformed to Hybrid Communicating Sequential Processes (HCSP) for formal verification with HHLProver. Within HHLProver, both interactive and automated theorem proving of HCSP processes are supported, with the help of an invariant generator, which is used for automated synthesis of differential invariants of ordinary differential equations based on both numerical methods and neural networks. Finally, ANSI-C code or SystemC code can be generated from the verified HCSP formal model with the guarantee of correctness. As a case study of CPS, this paper applies the MARS toolchain to the design of an intelligent temperature control system, including its modeling, simulation, verification and code generation. This case study demonstrates the advantages of the design of CPS with MARS, including the integration of modeling, simulation, verification and code generation; the integration of informal and formal design, thus providing balance between efficiency and rigidity and enabling a correct-by-construction design flow.

System-level design, and dependability prediction of safety-critical systems demand integration of architectural and analysis artifacts in a single development environment. Hybrid systems, with mutual dependencies and extensive interactions between the control portion and its physical environment, further intensify this need. Architecture Analysis and Design Language (AADL) is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with sublanguages for modeling and analysis of discrete behavior of the control portion, but not for continuous behavior of the physical environment. In a previous work, we have introduced Hybrid Annex for continuous behavior modeling as part of initial findings of an ongoing research effort on fulfilling the need for integrated modeling of the computing system along with its physical environment. In this article, we first detail complete structure of the Hybrid Annex along with appropriate examples for each section. Then, we present formal semantics of the synchronous subset of AADL models annotated with Hybrid Annex specifications using Hybrid Communicating Sequential Processes (HCSP). Formal semantics are used to verify correctness of AADL models (with Hybrid Annex specifications) using Hybrid Hoare Logic (HHL). A case study on a realistically-scaled automatic cruise control system is provided to demonstrate modeling and verification of hybrid systems using AADL with the proposed extension.

Simulink is widely used in the design of safety-critical embedded systems, including avionics and automotive applications. While it offers simulation for model validation, formal verification remains essential to rigorously ensure system correctness. Existing approaches often translate Simulink diagrams into third-party formal models, however, the lack of a rigorously defined semantics for Simulink can lead to inconsistencies between the original diagrams and their translated formal counterparts. In this paper, we present a formal semantic foundation for a core subset of Simulink by defining both denotational and operational semantics. The denotational semantics offers a mathematical interpretation of the diagram's input-output behavior, faithfully capturing its hierarchical structure. In contrast, the operational semantics specifies the concrete execution of Simulink diagrams, resolving block execution order, solving continuous dynamics, and coordinating hybrid discrete-continuous interactions. Both semantics have been fully formalized in Isabelle/HOL, and we have established their consistency by proving the existence and uniqueness of the timed state trajectories defined by the denotational semantics. Furthermore, to facilitate application, we developed a translator that automatically converts Simulink graphical diagrams into their Isabelle representation. Our formal semantics supports the rigorous analysis of Simulink diagram properties, as demonstrated through a PID control example. The semantics also establishes a foundation for validating simulation results and ensuring consistency between Simulink models and other formal models, thus enabling sound verification.

Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π-calculus (HpC), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical π-calculus, i.e., the extension is “minimal”, and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the HpC by considering a realistic handover protocol among mobile devices.

Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verification. However, the inherent complexity of control and data structures in programs makes this task particularly challenging. This paper presents a novel framework that integrates symbolic execution with large language models (LLMs) to automatically synthesize formally verified program specifications. Our method first employs symbolic execution to derive precise strongest postconditions for loop-free code segments. These symbolic execution results, along with automatically generated invariant templates, then guide the LLM to propose and iteratively refine loop invariants until a correct specification is obtained. The template-guided generation process robustly combines symbolic inference with LLM reasoning, significantly reducing hallucinations and syntactic errors by structurally constraining the LLM's output space. Furthermore, our approach can produce strong specifications without relying on externally provided verification goals, enabled by the rich semantic context supplied by symbolic execution, overcoming a key limitation of prior goal-dependent tools. Extensive evaluation shows that our tool SESpec outperforms the existing state-of-the-art tools across numerical and data-structure benchmarks, demonstrating both high precision and broad applicability.

Digital infrastructures, grids, and networks heavily rely on Cyber-Physical Systems (CPSs) endpoints in a context of mobile computing, referred to as mobile CPSs, including applications such as smart cities, intelligent transportation systems, and unmanned vehicles. Most of such systems are safety-critical, i.e., any error may result in catastrophic consequences. Mobile CPSs represent a novel computing paradigm, and their inherent complexity and interdisciplinary nature pose significant challenges to system design beyond the limits of state-of-the-art separation of concerns. Model-Based Design (MBD) is a key approach to mitigate the complexity of safety-critical systems. However, it lacks adequate modeling and analysis techniques to tame mobile CPSs. To address this gap, this paper proposes an extension of sequence diagrams, as found in SysML/UML, to facilitate an accurate, graphical representation of the deeply-coupled mobile, parallel, and hybrid behaviors (i.e., the entangled interplay of discrete and continuous behaviors). To ensure the correctness of the designed models, we propose a set of transformation rules that convert the (graphical and hence, by nature, informal) extended sequence diagram to a formal representation using the hybrid π -calculus, thereby enabling formal verification using, e.g., bisimulation-based model checking. Finally, we provide a case study where we employ extended sequence diagrams to model the scenario of the handover protocol of a train control system and formalize it into a hybrid π -calculus model using the proposed transformation rules.

Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately reflects the formal model. In this paper, we propose a code generation algorithm from HCSP to C with POSIX library for concurrency. The main difficulties include how to bridge the gap between the synchronized communication model in HCSP and the use of mutexes for synchronization in C, and how to discretize evolution along ODEs and support interrupt of ODE evolution by communication. To prove the correctness of code generation, we define a formal semantics for POSIX C, and build transition system models for both HCSP and C programs. We then define an approximate bisimulation relation between traces of transition systems, and show that under certain robustness conditions for HCSP, the generated C program is approximately bisimilar to the original model. Finally, we evaluate the code generation algorithm on a detailed model for automatic cruise control, showing its utility on real-world examples.

MARS is a toolchain, supporting model-based design of cyber-physical systems (CPS), which integrates informal and formal design. With MARS, a system under development can be graphically modeled by the combination of AADL and Simulink/Stateflow, then the simulation of the graphical model can be conducted. Furthermore, the graphical model can be automatically transformed to Hybrid Communicating Sequential Processes (HCSP) for formal verification with HHLProver. Finally, ANSI-C code or SystemC code can be generated from the verified HCSP formal model with the guarantee of correctness. As a case study of CPS, in this paper, we apply MARS to design an intelligent temperature control system, including its modeling, simulation, verification and code generation. This case study demonstrates the advantages of the design of CPS with MARS, including the integration of modeling, simulation, verification and code generation; the integration of informal and formal design, thus providing balance between efficiency and rigidity.

We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the system to be developed. For a safety-critical system, formal analysis and verification of its combined AADL and Simulink/Stateflow model can be conducted via the following steps. First, the toolchain automatically translates AADL and Simulink/Stateflow models into Hybrid CSP (HCSP), an extension of CSP for formally modeling hybrid systems. Second, the HCSP processes can be simulated using the HCSP simulator, and to complement incomplete simulation, they can be verified using the Hybrid Hoare Logic prover in Isabelle/HOL, as well as the more automated HHLPy prover. Finally, implementations in SystemC or C can be automatically generated from the verified HCSP processes. The transformation from AADL and Simulink/Stateflow to HCSP, and the one from HCSP to SystemC or C, are both guaranteed to be correct with formal proofs. This approach allows model-driven design of safety-critical cyber-physical systems based on graphical and formal models and proven-correct translation procedures. We demonstrate the use of the toolchain on several benchmarks of varying complexity, including several industrial-sized examples.

Message passing is a fundamental element in software development, ranging from concurrent and mobile computing to distributed services, but it suffers from communication errors such as deadlocks. Session types are a typing discipline for enforcing safe structured interactions between multiple participants. However, each typed interaction is restricted to having one fixed sender and one fixed receiver. In this paper, we extend session types with existential branching types, to handle a common interaction pattern with multiple senders and a single receiver in a synchronized setting, i.e. a receiver is available to receive messages from multiple senders, and which sender actually participates in the interaction cannot be determined till execution. We build the type system with existential branching types, which retain the important properties induced by standard session types: type safety, progress (i.e. deadlock-freedom), and fidelity. We further provide a novel communication type system to guarantee progress of dynamically interleaved multiparty sessions, by abandoning the strong restrictions of existing type systems. Finally, we encode Rust multi-thread primitives in the extended session types to show its expressivity, which can be considered as an attempt to check the deadlock-freedom of Rust multi-thread programs.

Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a specification logic and proof system for Hybrid Communicating Sequential Processes (HCSP), that extends CSP with ordinary differential equations (ODE) and interrupts to model interactions between continuous and discrete evolution. Because it includes a rich set of algebraic operators, complicated hybrid systems can be easily modelled in an algebra-like compositional way in HCSP. Our logic can be seen as a generalization and simplification of existing hybrid Hoare logics (HHL) based on duration calculus (DC), as well as a conservative extension of existing Hoare logics for concurrent programs. Its assertion logic is the first-order theory of differential equations (FOD), together with assertions about traces recording communications, readiness, and continuous evolution. We prove continuous relative completeness of the logic w.r.t. FOD, as well as discrete relative completeness in the sense that continuous behaviour can be arbitrarily approximated by discretization. Besides, we discuss how to simplify proofs using the logic by providing a simplified assertion language and a set of sound and complete rules for differential invariants for ODEs. Finally, we implement a proof assistant for the logic in Isabelle/HOL, and apply it to verify two case studies to illustrate the power and scalability of our logic.

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2023. The characteristic features of the HSTP category remain as in the previous edition: HSTP focuses on flexibility of programming languages as structuring principles for hybrid systems, unambiguity and precision of program semantics, and mathematical rigor of logical reasoning principles. The benchmark set includes nonlinear and parametric continuous and hybrid systems and hybrid games, each in three modes: fully automatic verification, semi-automatic verification from proof hints, proof checking from scripted tactics. This instance of the competition focuses on presenting the differences between the provers on a subset of the benchmark examples.

Matlab/Simulink is a de-facto industrial standard for modelling embedded systems. Reflecting the complexity of cyber-physical system (CPS) design, the semantics of Simulink is complex, mixing discrete and continuous time and events. In this paper, we define a compositional semantics of hierarchical Simulink diagrams using Higher-order Unifying Theories of Programming (HUTP) for CPS design. The HUTP theory satisfies the suitable algebraic properties to serve as a mathematical foundation for expressing the semantics of CPSs, in particular Simulink diagrams. We characterise a class of well-formed Simulink diagrams and prove the determinacy of their HUTP semantics. Moreover, we construct a framework for proving the consistency between Simulink diagrams and their translation to HCSP (Hybrid Communicating Sequential Processes). Finally, we provide a case study to illustrate and justify this translation.

Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis, and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction, however, poses significant challenges. To address these issues, Hoare and He’s Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design. Higher-order UTP (HUTP) is a conservative extension to Hoare and He’s theory that supports the specification of discrete, real-time, and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of normal hybrid designs to model, analyse, compose, refine, and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for Hybrid Communicating Sequential Processes and Simulink using HUTP.

Message passing is a fundamental element in software development, ranging from concurrent and mobile computing to distributed services, but it suffers from communication errors such as deadlocks. Session types are a typing discipline for enforcing safe structured interactions between multiple participants. However, each typed interaction is restricted to having one fixed sender and one fixed receiver. In this paper, we extend session types with existential branching types, to handle a common interaction pattern with multiple senders and a single receiver in a synchronized setting, i.e. a receiver is available to receive messages from multiple senders, and which sender actually participates in the interaction cannot be determined till execution. We build the type system with existential branching types, which retain the important properties induced by standard session types: type safety, progress (i.e. deadlock-freedom), and fidelity. We further provide a novel communication type system to guarantee progress of dynamically interleaved multiparty sessions, by abandoning the strong restrictions of existing type systems. Finally, we encode Rust multi-thread primitives in the extended session types to show its expressivity, which can be considered as an attempt to check the deadlock-freedom of Rust multi-thread programs.