Ultra-low-latency trading systems demand runtime verification (RV) that is both expressive and fast, with processing budgets measured in hundreds of nanoseconds. We present ChronosRV, a framework that compiles specifications written in a bounded fragment of Metric Temporal Logic (MTL) extended with a SERE-style (regular sequence) subset and lightweight aggregations, into highly optimized C++ monitors integrated in a zero-copy, lock-free, NUMA-aware event engine. We formalize a discrete-time, three-valued prefix semantics that supports bounded memory and robust verdicts in the presence of bounded out-of-order (OOO) arrivals via watermarks. Our synthesis pipeline maps logic to an operator network of bounded timers, counters, and small DFAs, with per-key sharding to exploit data parallelism. On synthetic workloads reflecting equity trading pipelines, ChronosRV sustains >1–4M events/s with median per-event processing in the sub-microsecond range, and detects injected violations with high accuracy under bounded OOO jitter. We provide a proof sketch of soundness and bounded completeness under watermarking, and report detailed ablations for property complexity, sharding, and OOO robustness.
Modern type-theory-based proof assistants/languages are increasingly supporting general-purpose programming, making them both practical and formally rigorous. This dual nature aligns well with the needs of safety-critical embedded system design. It is hence promising that such a language can be employed as a proper meta-language for building an embedded system design framework that integrates reasoning and programming. In this paper, we demonstrate a unified framework for synchronous embedded system design, which leverages both aspects of the quantitatively typed language Idris2, with a focus on an embedded domain-specific language (EDSL), named SynQ, in the framework. Specifically, we show that the leveraging of the expressiveness of quantitative type theory and the tagless final embedding allows synchronous systems to be properly modelled by SynQ. This then enables a systematic usage of Idris2 for facilitating both design and verification of synchronous systems, demonstrating an initial step towards a correct-by-construction embedded system design process.
Multiprecision arithmetic is required in many applications, notably safety critical areas. It carries, however, a substantial performance impact compared to fixed precision arithmetic. Since a significant part of this is due to allocation and memory fragmentation, a substantial speed up can be obtained by optimising for small numbers by storing them inline on the stack rather than on the heap. Libraries implementing such an optimisation typically fix the range of numbers considered small. However, optimal performance requires customising this range depending on the problem. The contribution of this tool paper is to introduce MPL, a library for arbitrary fixed precision and multiprecision arithmetic, which allows developers to customise the range of small numbers based on the knowledge of their problem at compile time. We experimentally demonstrate that MPL can deliver significant speed-ups when benchmarked against GMP and CLN, both running microbenchmarks on our library. MPL is released under a permissive BSD license, and we also provide a full integration of MPL with cvc5, enabling using MPL as a back end in cvc5.
This paper proposes a machine-checked and interface-based formal verification for the k-center problem. This formal architecture is built with four modules (Metric, FiniteSet, Radius, and Feasible). These modules separate the abstract metric view from graph, tree, and Euclidean backends, so that proofs can be reused across these spaces without modification. The algorithms are certificate-based. First, the greedy algorithm returns a farthest-first solution and is also a packing and covering witness. Second, the tree decision routine returns traces that show when a radius is feasible. Third, the graph backend offers multisource breadth-first search oracles that support these proofs. As a result, composable machine-checked proofs of classical results are obtained, and specialized versions for new settings are easy to add. The farthest-first constant factor approximation is formalized with a simple separation invariant. An exact tree oracle, called checkR, is given by binary search over a finite set of radii. A graph formal method is also designed that uses a packing-based witness to show that a target radius is not feasible. The greedy template is also combined with symmetric epsilon coresets, so the constant factor bound is kept under a controlled error from the coreset. For online input, a template is proposed to keep maximal packing. This template provides a radius within a factor of 2 of the best possible radius at each step. The framework is independent of one proof assistant and can be used in Lean. It is built for extension, since capacities and outliers are added by changing only the feasibility part. Low doubling and planar cases reuse the same basic lemmas, and Euclidean backends can link to tools for nets and coresets. By using one simple and witness-based template for the relation between packing and covering and for search over the radius, long approximation proofs are turned into small and verifiable pieces. These pieces can be combined to build algorithms for dynamic data, streaming data, and networked systems.
We propose Separation Logic with Heap Variables (SLHV), an extension of separation logic which introduces explicit heap variables in conjunction with separating conjunction and classical Boolean operations. We provide a decision procedure for the satisfiability of SLHV by reducing to the satisfiability of quantifier-free linear integer arithmetic. We implement a prototype solver for SLHV based on Z3, which, together with the encoding of heap-manipulating C programs as SLHV formulas, gives rise to a new bounded model checker for heap-manipulating C programs. The experimental results show the efficacy of our approach.
A prominent functionality of smart contracts is regulating financial transactions on the blockchain. Flaws in a smart contract could cause funds to be frozen in the contract, resulting in financial losses of honest users. This issue of frozen funds is often considered a violation of liquidity requirements. In this work, we propose a liquidity property for account-based blockchain platforms such as Ethereum. The property captures the situation where the process of claiming funds by the honest users can be disrupted by the strategy of the environment. We formally establish the connection between this property and a strategy-less notion of liquidity under particular conditions, devise sound proof methods for the property, mechanize the theories and proof methods in the Rocq prover, and apply the proof methods to verify or refute the property for example smart contracts. Informative verification and refutation results are obtained for the examples—strategies help reveal how a user may act to ensure the transfer of funds out of a contract or how an attacker may exploit the inherent vulnerabilities of a contract to freeze funds.
A key operation in processing an unbounded data stream is windowing, which extracts finite portions of streams for further handling. The existing frameworks and query languages either require windows to be defined using ad hoc imperative languages or are limited to rudimentary constructs such as time- or count-based windows. We propose Window EXpression, a formal specification for precisely expressing windowing constructs based on monadic second-order logic. WEX can naturally express traditional windowing constructs such as sliding windows and tumbling windows, as well as more complex windows whose start and end indices are triggered based on the satisfaction of given logical conditions. After introducing a model of symbolic automata with lookbacks over an alphabet theory, we present another equivalent representation of WEX based on symbolic regular expressions. The precise semantics of windowing enable static analysis over WEX. In particular, we show that, in general,it is undecidable to check whether a WEX allows an unbounded number of overlapping windows. However, when the data stream is over a finite alphabet, or the alphabet theory has the so-called completion property, the problem becomes decidable.
Dynamic logic is a valuable formalism that has many applications in ensuring the correctness of safety-critical systems. We present a novel theory of parameterized dynamic logic, namely DL _p , for specifying and reasoning about program models based on their operational semantics. Different from most dynamic logics that deal with regular expressions or a particular type of models, DL _p allows arbitrary forms of programs and formulas according to specific domains. It provides a language-independent proof calculus under dynamic-logic settings, supporting symbolic-execution-based reasoning with a general notion of labels for capturing program configurations. To admit certain infinite proof deductions caused by loop programs, we adapt the cyclic proof approach to the theory of DL _p by building a cyclic proof structure specific to DL _p . The soundness of DL _p is analyzed and formally proved. A case study displays an instantiation of DL _p in particular domains, demonstrating the potential usage of DL _p in program verification.
Modularity and refinement are two important software engineering concepts. Modularity is essential for maintaining intellectual control over complex systems by breaking them into loosely coupled subsystems. Refinement is a systematic approach that gradually transforms a specification into a working system while ensuring correctness at each step. Unfortunately, modularity and refinement have an uneasy relationship with each other, as the operators used to describe a system model in a modular way are generally nonmonotonic with respect to refinement. In this work we present a useful technique and the necessary conditions to ensure that data refinement is monotonic with respect to conjunction. The essential idea is to represent all system operations using a smaller set of operations (kernel) that do not interfere with each other. It is then possible to refine the entire system by refining just the kernel. We demonstrate this technique with a simple example and refer to a larger case study in which this technique was applied to a model of a real-world application.
Threat modelling is crucial for analysing how attacks may affect security-critical systems, detecting present vulnerabilities, and managing risk. System designers use attack trees and their extensions during an application’s design and implementation phase for these tasks. However, it is equally essential that end-users know how to use the final system securely. The competence profiles of end-users highly differ from the profiles of system designers. Therefore, we aim to reflect these different levels of competences in our proposition to enhance the models. Our research examines the perception of attack trees and their extensions among laypeople. We conducted a task-oriented survey (n=133), where non-experts in cyber-security had to interpret three attack-defense tree representations of two different attack scenarios. Additionally, we use the technology acceptance model (TAM) to investigate how participants perceived these representations. Our survey demonstrates that standard attack-defense tree visualisations are on average as effective as running text for risk communication to laypeople. However, they may currently not evolve their full potential as laypeople usually lack logical skills. Basic logic is a crucial element for teaching laypeople about security. Motivated by the results, we suggest ways the models could be simplified for the users, to ease the access through simpler perspectives on the logical relationships described by the models.
Log parsing is a critical step for log analysis, responsible for converting raw, semi-structured log messages into structured templates. Despite using semantic knowledge to enhance template extraction, LLM-based log parsers frequently generate fragmented templates, generating several marginally distinct templates for semantically identical events. This fragmentation generates duplicate downstream processing, reduces cache hit rates, and inflates the template pool. We introduce EM-Merge, a lightweight, model-independent postprocessing layer that directly mitigates fragmentation without requiring further LLM calls. EM-Merge employs a two-stage strategy: (1) semantic screening, where newly generated and cached templates are encoded with Sentence-BERT and nearest-neighbor search selects semantically plausible candidates; (2) confidence-weighted structural merging, where candidate pairs are scored by a normalized longest-common-subsequence measure modulated by LLM generation confidences, then clustered and merged into generalized templates (non-common tokens replaced by wildcards). This design preserves semantic distinctions while preventing misleading splits driven by punctuation or surface variation. We evaluate EM-Merge on 14 public log datasets and find that, with no runtime overhead, it reliably reduces template redundancy, improves grouping and parsing accuracy, and lowers end-to-end processing cost when compared to strong baselines.
The complexity of unit systems for physical quantities and their informal treatment pose potential risk of errors in engineering and mathematical reasoning. Moreover, existing formal verification tools lack support for reasoning involving physical quantities with units. To address this, we propose VQCS (Verified Quantity Calculus System), a formal system implemented in the Rocq theorem prover. Its main contributions are as follows. First, we construct a unit system based on dimensional analysis, defining the syntax and semantics of units while supporting both manual and automatic conversion between units of the same kind. Second, we establish a quantity calculus system over abstract data types. Third, we define concrete quantity calculus systems over the real numbers and real vectors, enabling unit-aware computations for common mathematical derivations in engineering applications. Finally, we instantiate the system with the International System of Units (SI) and provide several case studies demonstrating its practical utility. The VQCS framework is released as an open-source Rocq library, providing a verifiable infrastructure for quantity calculus in engineering modeling.
As regulatory requirements for software systems in the European Union continue to evolve, there is growing pressure to embed mechanisms into deployed systems that ensure both operational trustworthiness and legal accountability. Frameworks such as the AI Act and the Cyber Resilience Act introduce obligations related to cybersecurity, incident response, transparency, and auditability, particularly for high-risk and autonomous systems. These demands go beyond traditional verification and increasingly call for runtime components capable of monitoring behaviour, detecting non-compliance, and preserving forensic evidence. In this work, we present FLARE, a runtime verification tool that combines automated monitoring with tamper-evident logging to support regulatory compliance. Building on existing runtime verification techniques, FLARE enables the construction of both a system harness that monitors live interactions with the environment and flags policy violations; and a forensic node, capable of recording verifiable logs. We demonstrate the application of FLARE on a waste-identification and localisation drone, a cyber-physical system subject to multiple legal and safety constraints. Our case study shows how FLARE can support legal and operational requirements while introducing minimal overhead, providing a practical path towards compliance-aware software instrumentation.
Automated translation of legacy software into modern languages is essential for adopting safer programming practices at scale. We review current rule-based, neural and neurosymbolic approaches and show why none fully address the needs of real-world repositories. Rule-based tools scale but mirror the source language, producing unidiomatic target code. LLM-based methods capture idioms but lack correctness guarantees. Hybrid systems partially bridge the gap but remain brittle when faced with complex features such as concurrency or third-party dependencies.
Byzantine-fault-tolerant (BFT) protocols allow distributed systems to function correctly even when some of the nodes act maliciously. Byzantine linearizability, as an extension of linearizability in the presence of faulty nodes, is often used as the correctness criterion for BFT protocols. In this paper, we propose a program logic for verifying Byzantine linearizability. We reason about the effects of faulty nodes using a helping mechanism that instruments the protocol code with abstract operations that model the faulty nodes’ behaviors in the views of correct nodes. We prove the soundness of our logic by establishing a contextual refinement that is equivalent to Byzantine linearizability. We apply our logic to verify two typical BFT protocols.
In this work, we focus on the Partial Constraint Satisfaction Problem (PCSP) over control-flow graphs (CFGs) of programs. PCSP serves as a generalization of the well-known Constraint Satisfaction Problem (CSP). In the CSP framework, we define a set of variables, a set of constraints, and a finite domain D that encompasses all possible values for each variable. The objective is to assign a value to each variable in such a way that all constraints are satisfied. In the graph variant of CSP, an underlying graph is considered, and we have one variable corresponding to each vertex of the graph and one or several constraints corresponding to each edge. In PCSPs, we allow for certain constraints to be violated at a specified cost, aiming to find a solution that minimizes the total cost. Numerous classical compiler optimization tasks can be framed as PCSPs over control-flow graphs. Examples include Register Allocation, Lifetime-optimal Speculative Partial Redundancy Elimination (LOSPRE), and Optimal Placement of Bank Selection Instructions. On the other hand, it is well-known that control-flow graphs of structured programs are sparse and decomposable in a variety of ways. In this work, we rely on the Series-Parallel-Loop (SPL) decompositions as introduced by [7]. Our main contribution is a general algorithm for PCSPs over SPL graphs with a time complexity of O(|G| · |D|^6) , where |G| represents the size of the control-flow graph. Note that for any fixed domain D , this yields a linear-time solution. Our algorithm can be seen as a generalization and unification of previous SPL-based approaches for register allocation and LOSPRE. In addition, we provide experimental results over another classical PCSP task, i.e., Optimal Bank Selection, achieving runtimes four times better than the previous state of the art.
The identification of deterministic finite automata (DFAs) from labeled examples is a cornerstone of automata learning, yet traditional methods focus on learning monolithic DFAs, which often yield a large DFA lacking simplicity and interoperability. Recent work addresses these limitations by exploring DFA decomposition identification problems (DFA-DIPs), which model system behavior as intersections of multiple DFAs, offering modularity for complex tasks. However, existing DFA-DIP approaches depend on SAT encodings derived from Augmented Prefix Tree Acceptors (APTAs), incurring scalability limitations due to their inherent redundancy. In this work, we advance DFA-DIP research through studying two variants: the traditional Pareto-optimal DIP and the novel states-optimal DIP, which prioritizes a minimal number of states. We propose a novel framework that bridges DFA decomposition with recent advancements in automata representation. One of our key innovations replaces APTA with 3-valued DFA (3DFA) derived directly from labeled examples. This compact representation eliminates redundancies of APTA, thus drastically reducing variables in the improved SAT encoding. Experimental results demonstrate that our 3DFA-based approach achieves significant efficiency gains for the Pareto-optimal DIP while enabling a scalable solution for the states-optimal DIP.
In light of the inherently complex and dynamic nature of real-world environments, incorporating risk measures is crucial for the robustness evaluation of deep learning models. In this work, we propose a Risk-Averse Certification framework for Bayesian neural networks called RAC-BNN. Our method leverages sampling and optimisation to compute a probabilistically sound approximation of the output set of a BNN, represented using a set of template polytopes. To enhance risk-aware robustness evaluation, we integrate a coherent distortion risk measure–Conditional Value at Risk (CVaR)–into the certification framework, providing probabilistic guarantees based on empirical distributions obtained through sampling. We validate RAC-BNN on a range of regression and classification benchmarks and compare its performance with a state-of-the-art method. The results show that RAC-BNN effectively quantifies robustness under worst-performing risky scenarios, and achieves tighter certified bounds and higher efficiency in complex tasks.
We introduce HHLPar, a tool for verifying hybrid systems modeled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is based on a Hybrid Hoare Logic for HCSP, which enables reasoning about both the continuous-time properties of differential equations and the communication and parallel composition of HCSP processes. This is achieved through the use of specialized trace assertions and their synchronization. The logic has been formalized and proven sound in Isabelle/HOL, providing a reliable foundation for the verification. HHLPar implements the logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating assertions for individual sequential processes, and then composing them via synchronization to obtain the final specification for the entire parallel HCSP process; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. The resulting assertions are sufficiently expressive to deduce both the state properties at termination and the continuous-time invariants maintained throughout the execution of processes, which are critical for ensuring system safety. Finally, we present the main issues related to the implementation of HHLPar and demonstrate its applicability through a case study involving a simplified cruise control system.
Enhanced regular expressions (EREs), which extend standard regular expressions with shuffle and counting operators, provide exponentially more succinct descriptions of regular languages. The membership problem, determining whether a given word w belongs to the language generated by an ERE E, is fundamental to numerous applications. However, efficient solutions for the membership problem of unconstrained EREs have remained elusive. This paper introduces a derivative for the counting operator and rigorously proves its correctness. We then leverage this derivative to design a membership algorithm for unconstrained EREs and analyze its time complexity based on a lemma establishing the relationship between the size of the derivative and the expression. We further propose algorithms based on the proposed derivatives to generate positive and negative words of specific lengths for EREs. The performance of the membership algorithm is then evaluated on real-world EREs. Finally, we validate the correctness of two existing inference algorithms that previously lacked formal correctness guarantees due to the absence of practical membership algorithms for unconstrained EREs.
