I take inspiration from the property-testing literature, particularly the work of Prof. John Hughes [17], and explore how such ideas might be applied to numerical models of the ocean. Specifically, I ask whether geophysical fluid dynamics (GFD) theory, expressed as property tests, might used to address the oracle problem of testing the correctness of ocean models. I propose that a number of simple idealized GFD problems can be framed as property tests. These examples clearly illustrate how physics naturally lends itself to specifying property tests. Which of these proposed tests might be most feasible and useful, remains to be seen.
We describe a machine-checked correctness proof of a C program that converts a coordinate-form (COO) sparse matrix to a compressed-sparse-row (CSR) matrix. The classic algorithm (sort the COO entries in lexicographic order by row,column; fill in the CSR arrays left to right) is concise but has rather intricate invariants. We illustrate a bottom-up methodology for deriving the invariants from the program.
Correctness in scientific computing (SC) is gaining increasing attention in the formal methods (FM) and programming languages (PL) community. Existing PL/FM verification techniques struggle with the complexities of realistic SC applications. Part of the problem is a lack of a common understanding between the SC and PL/FM communities of machine-verifiable correctness challenges and dimensions of correctness in SC applications. To address this gap, we call for specialized challenge problems to inform the development and evaluation of FM/PL verification techniques for correctness in SC. These specialized challenges are intended to augment existing problems studied by FM/PL researchers for general programs to ensure the needs of SC applications can be met. We propose several dimensions of correctness relevant to scientific computing, and discuss some guidelines and criteria for designing challenge problems to evaluate correctness in scientific computing.
Scientific software is, by its very nature, complex. It is mathematical and highly optimized which makes it prone to subtle bugs not as easily detected by traditional testing. We outline how symbolic execution can be used to write tests similar to traditional unit tests while providing stronger verification guarantees and apply this methodology to a sparse matrix algorithm.
Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development.
We present a verification challenge based on the fractional cascading (FC) technique for accelerating repeated searches across a collection of sorted arrays. The specific context is nuclear cross section lookup in a simulation code, where a material consists of many nuclides, each with its own sorted energy grid. A naive search performs a binary search in each array individually. The FC-based cascade grid structure reduces this cost by performing a single binary search followed by constant-time refinements. The challenge consists of verifying the correctness of the FC algorithm with respect to the naive approach and validating its structural properties.
We mechanize the fundamental properties of a rounding error model for floating-point arithmetic based on relative precision, a measure of error proposed as a substitute for relative error in rounding error analysis. A key property of relative precision is that it forms a true metric, providing a well-defined measure of distance between exact results and their floating-point approximations while offering a structured approach to propagating error bounds through sequences of computations. Our mechanization formalizes this property, establishes rules for converting between relative precision and relative error, and shows that the rounding error model based on relative precision slightly overapproximates the standard rounding error model. Finally, we demonstrate, with a simple example of the inner product of two vectors, that this alternative model facilitates a tractable approach to developing certified rounding error bounds.
We describe a challenge problem for verification based on the MPICH implementation of MPI. The MPICH implementation includes several algorithms for allreduce, all of which should be functionally equivalent to reduce followed by broadcast. We created standalone versions of three algorithms and verified two of them using CIVL.
Sparse matrix vector multiplication (SpMV) is a fundamental kernel in scientific codes that rely on iterative solvers. In this first part of our work, we present both a sequential and a basic MPI parallel implementations of SpMV, aiming to provide a challenge problem for the scientific software verification community. The implementations are described in the context of the PETSc library.
This paper describes our experience developing polynomial approximations for trigonometric functions that produce correctly rounded results for multiple representations and rounding modes using the RLIBM approach. A key challenge with trigonometric functions concerns range reduction with "pi", which reduces a given input in the domain of a 32-bit float to a small domain. Any rounding error in the value of "pi" is amplified during range reduction, which can result in wrong results. We describe our experience implementing fast range reduction techniques that maintain a large number of bits of "pi" both with floating-point and integer computations. The resulting implementations for trigonometric functions are fast and produce correctly rounded results for all inputs for multiple representations up to 32-bits with a single implementation.
Session types are a typing discipline used to formally describe communication-driven applications with the aim of fewer errors and easier debugging later into the life cycle of the software.Protocols at the transport layer such as TCP, UDP, and QUIC underpin most of the communication on the modern Internet and affect billions of end-users.The transport layer has different requirements and constraints compared to the application layer resulting in different requirements for verification.Despite this, to our best knowledge, no work shows the application of session types at the transport layer.In this work, we discuss how multiparty session types (MPST) can be applied to implement the TCP protocol.We develop an MPST-based implementation of a subset of a TCP server in Rust and test its interoperability against the Linux TCP stack.Our results highlight the differences in assumptions between session type theory and the way transport layer protocols are usually implemented.This work is the first step towards bringing session types into the transport layer.
Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software.However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control.This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems).We propose a methodology for integrating multiple behaviourally-typed components, written in different languages.Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment.We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing.
Session types are a type discipline for describing and specifying communication behaviours of concurrent processes. Session subtyping, firstly introduced by Gay and Hole, is widely used for enlarging typability of session programs. This paper gives the complexity analysis of three algorithms for subtyping of synchronous binary session types. First, we analyse the complexity of the algorithm from the original paper, which is based on an inductive tree search. We then introduce its optimised version, which improves the complexity, but is still exponential against the size of the two types. Finally, we propose a new quadratic algorithm based on a graph search using the concept of XYZW-simulation, recently introduced by Silva et al.
In robotic radiation therapy, high-energy photon beams from different directions are directed at a target within the patient. Target motion can be tracked by robotic ultrasound and then compensated by synchronous beam motion. However, moving the beams may result in beams passing through the ultrasound transducer or the robot carrying it. While this can be avoided by pausing the beam delivery, the treatment time would increase. Typically, the beams are delivered in an order which minimizes the robot motion and thereby the overall treatment time. However, this order can be changed, i.e., instead of pausing beams, other feasible beam could be delivered. We address this problem of dynamically ordering the beams by applying a model checking paradigm to select feasible beams. Since breathing patterns are complex and change rapidly, any offline model would be too imprecise. Thus, model checking must be conducted online, predicting the patient's current breathing pattern for a short amount of time and checking which beams can be delivered safely. Monitoring the treatment delivery online provides the option to reschedule beams dynamically in order to avoid pausing and hence to reduce treatment time. While human breathing patterns are complex and may change rapidly, we need a model which can be verified quickly and use approximation by a superposition of sine curves. Further, we simplify the 3D breathing motion into separate 1D models. We compensate the simplification by adding noise inside the model itself. In turn, we synchronize between the multiple models representing the different spatial directions, the treatment simulation, and corresponding verification queries. Our preliminary results show a 16.02 % to 37.21 % mean improvement on the idle time compared to a static beam schedule, depending on an additional safety margin. Note that an additional safety margin around the ultrasound robot can decrease idle times but also compromises plan quality by limiting the range of available beam directions. In contrast, the approach using online model checking maintains the plan quality. Further, we compare to a naive machine learning approach that does not achieve its goals while being harder to reason about.
We explore the integration of metaprogramming in a call-by-value linear lambda-calculus and sketch its extension to a session type system. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may then be boxed and transmitted in messages. Once received, one such value may then be unboxed (with a let-box construct) and locally applied before being run. We present a series of examples where servers prepare and ship code on demand via session typed messages.
A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.
We address the question of characterising the well-formedness properties of multiparty session types semantically, i.e., as properties of the semantic model used to interpret types. Choosing Prime Event Structures (PESs) as our semantic model, we present semantic counterparts for the two properties that underpin global type well-formedness, namely projectability and boundedness, in this model. As a first step towards a characterisation of the class of PESs corresponding to well-formed global types, we identify some simple structural properties satisfied by such PESs.
Ensuring resource isolation at the hardware level is a crucial step towards more security inside the Internet of Things. Even though there is still no generally accepted technique to generate appropriate tests, it became clear that tests should be generated at the system level. In this paper, we illustrate the modeling aspects in test generation for resource isolation, namely modeling the behavior and expressing the intended test scenario. We present both aspects using the industrial standard PSS and an academic approach based on conformance testing.
The consensus problem is a fundamental problem in distributed systems. It involves a set of actors, or entities, that need to agree on some values or decisions. The Raft algorithm is a solution to the consensus problem that has gained widespread popularity as an easy-to-understand and implement alternative to Lamport's Paxos algorithm. In this paper we discuss a formalisation of the Raft algorithm and its associated correctness properties in the mCRL2 specification language.
We revisit the IEEE 1394 high-performance serial bus ("FireWire"), which became a success story in formal methods after three PhD students, by using process algebra and model checking, detected a deadlock error in this IEEE standard. We present four formal models for the asynchronous mode of the Link Layer of IEEE 1394: the original model in muCRL, a simplified model in mCRL2, a revised model in LOTOS, and a novel model in LNT.
