The formal verification of IoT security protocols is often split into two largely independent domains. Qualitative analysis establishes logical correctness against active intruders, whereas quantitative analysis evaluates performance metrics such as latency and energy consumption. Maintaining separate models for these purposes is both labor-intensive and prone to semantic drift, leading to a recurring mismatch: protocols that appear secure in theory may fail once exposed to stochastic constraints of real-world networks. To address this gap, we propose a unified framework anchored by Pat2Prism, a novel tool that automates the translation of CSP-based specifications into probabilistic models. Beyond mere automation, we establish a rigorous theoretical foundation for this transformation. We define a formal mapping from Process Analysis Toolkit (PAT)’s Labeled Transition Systems (LTSs) to PRISM’s Markov Decision Processes (MDPs) and prove that it preserves trace semantics and safety properties, ensuring quantitative insights are drawn from a behaviorally faithful refinement of the verified specification. We evaluate the framework on the CoAP-EAP protocol and its lightweight variant, Lo-CoAP-EAP. Although both pass qualitative verification, quantitative results expose a critical trade-off: the 7.87
Floating-point numerical errors are a major threat to software reliability. Existing oracle-based dynamic analysis tools typically use a statically configured precision oracle, forcing a trade-off between accuracy and overhead. We present RealSanitizer, an instrumentation tool with an ISREAL-based dynamic precision oracle that adjusts precision per operation while bounding oracle error by a user-specified threshold. On 42 reported GSL error-triggering cases, RealSanitizer detects 39 (93
Temporal logics are widely used to specify and reason about system behaviors over time. However, classical temporal logic reasoning often relies on explicit system models or complete execution traces and typically yields Boolean satisfaction results, which limits its applicability in data-driven settings where only partial observational traces are available. To address this issue, we propose a neural-symbolic framework for learning-based quantitative evaluation of GR(1) temporal properties upon partial data traces. The core idea is to treat elementary temporal formulas as learnable primitives that predict confidence values for future satisfaction of atomic propositions. Confidence values of more complex formulas are then derived using compositional rules. We apply the framework to a real-world academic collaboration prediction task on a temporal collaboration network. Experimental results demonstrate that the proposed approach effectively captures future collaboration patterns and supports temporal logic evaluation in real-world settings. This work bridges classical temporal logic reasoning and data-driven prediction, enabling quantitative temporal reasoning under partial observation.
Reinforcement Learning (RL) has shown significant success in sequential decision making for single (reachability) goals, but many practical tasks require pursing a series of goals with temporal dependencies among them. We introduce an incremental RL framework that leverages Linear Temporal Logic on finite traces (LTL _f ) specifications to express such goals. Our framework is formalized through Clocked Goal-Augmented Markov Decision Process (MDP), in which each goal corresponds to an atomic proposition, and the objective is to learn an optimal policy that satisfies LTL _f formulas constructed from these propositions. We propose solution techniques by training a Gated Recurrent Unit (GRU)-based RL network to learn policies for a set of single goals and employ DFA-based reward machines to guide their composition toward temporally-dependent goals. This technique enables incremental RL, allowing further temporally dependent goals and potential safety constraints (between ongoing and newly introduced ones) to arrive during execution without retraining the base network. Empirical evaluation on benchmark environments shows that under our approach, the success rate stablizes and converges empirically on incrementally specified temporally dependent goals, demonstrating stable and efficient learning.
Verifying the functional correctness of real-world code with complex algorithms requires reasoning about both implementation correctness and algorithm correctness. Implementation correctness, which relates concrete programs to abstract functional models, is inherently relational, yet is traditionally formalized using standard Hoare logic alone. This paper proposes a hybrid reasoning approach that combines relational Hoare logic and standard Hoare logic. Our key insight is that verifying implementation correctness naturally calls for relational Hoare logic, while algorithm correctness is well-suited to standard Hoare logic. Compared to traditional verifications that rely exclusively on standard Hoare logic, our approach simplifies proofs and offers more intuitive reasoning patterns. We demonstrate this in a setting where the concrete language is a C-like imperative language and the abstract algorithm is written in a simple nondeterministic functional language. Through case studies on binary search trees and merge sort, we show how our hybrid reasoning approach addresses challenges in verifying complex algorithms, reduces proof complexity, and enhances clarity.
Order-sorted equational logic is sound and complete with respect to all models, but it cannot prove inductive theorems because they are not necessarily satisfied by unreachable models. We propose OEqID ^ω , an extended order-sorted equational logic that permits infinite proofs, and has a case-split inference rule corresponding to the structural induction, which is sound and complete with respect to all reachable models, thereby enabling the proof of all inductive theorems. Although the case-split rule is defined with respect to a constructor family in a many-sorted specification, an order-sorted specification (1) might not allow the case-split rule for some constructor family, or (2) the rule may require redundant premises. In OEqID ^ω , we introduce the notion of constructor cover to address these two issues.
The reliability of Deep Reinforcement Learning (DRL) agents is a major obstacle to their deployment in safety-critical domains. Traditional evaluations, focused on maximizing cumulative rewards, often mask critical vulnerabilities and fail to capture the nuances of agent behavior. To address this gap, we introduce the DRL Metamorphic Testing Framework (DRL-MTF), a systematic approach for evaluating agent robustness through a novel taxonomy of 11 parameterized Metamorphic Relations (MRs). We evaluated prominent Proximal Policy Optimization (PPO) and Deep Q-Network (DQN) agents on the Atari benchmark, revealing a stark divergence between reward-based (outcome) and action-based (behavioral) robustness. For instance, a DQN agent passed 70
Understanding which memory locations are truly shared across threads is fundamental for debugging, testing, and analyzing multi-threaded software. Existing static analyses provide broad coverage, but often over-approximate sharing because of aliasing, indirect calls, and complex control flow, which limits their practical usefulness. This paper presents a synchronization-aware dynamic thread-sharing analysis that derives sharing information from concrete executions. Our approach instruments memory accesses and key synchronization events, executes the program under available test cases, and performs an offline analysis to identify source-level thread-sharing points and summarize cross-thread interactions. The analysis further distinguishes thread-local data, observed synchronized sharing, and critical thread sharing points. We implement the approach in an open-source tool, DtTsa, and evaluate it on three benchmark suites (i.e., CVE-Benchmark, DataRaceBench, SCTBench). Results show that DtTsa produces concise, execution-grounded sharing summaries, covers many race-relevant access sites reported by existing tools, directly supports subsequent controlled concurrency testing, and incurs practical overhead.
Code review is widely employed to verify software functionality against requirements. Increasing evidence suggests that adopting formal specifications can enhance the process and quality of traditional code review by introducing greater rigorS. A high level of automation in formal specification-based code review is desirable, as the process is time-consuming and labor-intensive. Additionally, the program reading techniques used in the existing formal specification-based review methods, such as checklist-based reading, provide little guidance for reviewers on how to detect faults or the inconsistencies, relying on the reviewer’s experience and personal skills. In this paper, we address these problems by proposing an improved method for formal specification-based code review, leveraging the remarkable capabilities of LLMs to automatically review code against the formal specification to identify potential discrepancies and produce review report. A tool is developed to support it. Experiments are conducted to evaluate its performance by using the public BuggyJava + JML dataset comprising 586 buggy programs after processing. The result demonstrates that the proposed method integrating GPT-5.4 is effective, attaining an 85.84
Classical Timed Games formulations may be unsuitable, or require substantial modeling effort, to capture complex interaction patterns between a controller and its surrounding environment, in which the non-determinism must be resolved after the controller has chosen which action to perform. This paper introduces Timed CLTLoc Games (TCGs), a novel Timed Game variant designed to facilitate the modeling of such patterns. Unlike classical Timed Games, TCGs partition locations rather than actions, and use Constraint Linear Temporal Logic over clocks formulae to specify the controller’s objectives. We implement algorithms for solving TCGs in our C++20 region-based library Tarzan, leveraging OpenMP for efficient parallelization. We then validate our theoretical results through an empirical evaluation on a Production Cell case study, demonstrating that the region-based implementation is computationally efficient in practice for medium-sized models.
Safety-critical scenarios are fundamental to the safety validation of Autonomous Driving Systems (ADS). Common approaches for identifying such high-value scenarios involve manual expert assessment or post-simulation analysis, which respectively suffer from human subjectivity and prohibitive computational overhead. To address this, we propose a formal framework for evaluating the risk level of a driving scenario via statistical model checking (SMC). The framework contains: (1) an automated conversion module that transforms a scenario subject to OpenSCENARIO standard into a probabilistic Timed Automata model; (2) a SMC module that verifies the formal model with a TTC-based quantitative metrics aligned with ISO 34502 standard and assigns the scenario a score to indicate its safety criticality. This framework provides an end-to-end objective evaluation approach for assessing safety criticality of driving scenarios, thereby improving efficiency. Experiments successfully scored 20 nondeterministic scenarios that are hard for humans to assess and achieved a 45- to 50-fold speedup compared to post-simulation evaluation, further saving labor and enabling rigorous automated safety scoring and scenario prioritization.
We propose a symbolic model checking framework for Linear Temporal Dynamic Logic (LTDL) via compositional testers, extending Linear Dynamic Logic (LDL) with bidirectional LTL operators. This enables past-time specifications (unattainable in pure LDL) while preserving LTL’s conciseness and verification efficiency, without increasing theoretical expressiveness. We make four contributions: (1) algorithms for constructing and optimizing regular grammars for LTDL path expressions to eliminate redundant variables and productions; (2) an algorithm for eliminating zero-delay cycles in regular grammars to avoid algebraic loops; (3) a method for generating compositional testers from LTDL; and (4) LTDLTester, an open-source tool for producing SMV-compatible LTDL testers. This reduces verification to checking the initial states of a system-tester synchronous parallel composition against output assertions, allowing direct application of standard symbolic checkers (e.g., NuSMV). Experiments show our approach significantly outperforms MCMAS _LDLK , the first native LDL model checker.
Modelling complex information systems (e.g., combinations of heterogeneous data sources, data from hybrid-system sensors, or medical diagnostic exams) often requires managing inconsistencies in which different decisions and instructions may simultaneously align or conflict. Decision and reasoning methods for such scenarios are a focus of paraconsistent logics, which provide a means of handling inconsistencies without collapsing into triviality, treating them as potentially informative rather than anomalous. Paraconsistent labelled transition systems (PLTS) were introduced as transition structures– parameterised by an underlying lattice– where each transition is characterised by a pair of values: one representing evidence that the transition occurs and the other representing evidence against it. Together with their associated modal logic and process algebra, PLTS provide a formal framework for modelling and reasoning in inconsistent scenarios. In this paper, we present an interactive toolkit that allows users to construct and visualise PLTS, as well as to interpret modal formulae over them. Finally, illustrative examples of the applicability of the framework and the toolkit are explored in fields such as robotics and finance.
C programmers who wish to perform interactive theorem proving (e.g., when verifying critical code they write) currently face a language barrier: working with existing provers requires familiarity with their own proof languages—usually a custom tactic language or a functional programming language—far removed from the C programming environment and paradigm. To bridge this gap, we present the first higher-order logic (HOL) theorem proving interface for C. Our interface is comprehensive: it covers the core data types and operations of HOL theorem proving in the LCF style, readily usable for forward derivation of theorems by invoking existing inference rules. Our interface is trustworthy: by extending the LCF architecture with a client-server model, it ensures every theorem constructed by arbitrary C code is necessarily derived from a small trusted proof kernel. Finally, programming derived proof facilities in C is practical: we demonstrate this by implementing commonly used tactics for goal-directed reasoning as a library on top of our interface, which utilizes a goal-tree data structure dedicated to the bookkeeping of proof states and applies imperative programming patterns naturally.
Formal methods have widespread use in high-assurance software development. In practice, the formal specification is derived from the informal user requirements, but traceability links between them are often not explicitly established by formal specification developers. These links are essential and desirable for validating the formal specification and maintaining the formal specification as requirements evolve. Manually creating trace links is not recommended due to its time-consuming nature. Additionally, we have applied some existing automated trace links recovery techniques based on textual similarity and found them suffer from low precision and F1-score. To address these problems, this paper proposes an improved method for automatic establishment of trace links from the informal requirements to the formal specification by leveraging the remarkable capability of LLMs. Our approach consists of three key activities: identifying desired functions from a structured natural language requirements document, deriving process (operation) specifications along with their associated type declarations from the formal specification, and establishing the trace links between them using LLMs. A tool is developed to support the proposed method. We evaluate the proposed method across four projects such as the ATM system and the Sun Search System in avionics. The experiment results demonstrate that the proposed method performs significantly better in precision, recall and F1-score than the existing text-based similarity techniques, including Latent Semantic Indexing, Vector Space Model, Word2Vec embeddings, and LLM-based embeddings. Specifically, our evaluation involving GPT-4o, Gemini 3.1 Pro, and DeepSeek V3 shows that while all three LLMs achieve consistent precision, recall, and F1-score, GPT-4o is the most time-efficient for trace link recovery.
Memory safety vulnerabilities in C programs remain a critical challenge in systems software. While rewriting legacy code in Rust offers a promising solution, manual migration is error-prone and labor-intensive. Existing automated translation tools either generate unsafe Rust or rely on heavy-weight static analysis that struggles with C’s flexible pointer arithmetic. We present a lightweight and automated approach to translating C to safe Rust by exploiting dynamic ownership and borrow checking provided by a small trusted runtime built with Rust’s smart-pointer primitives. Our method dynamically tracks ownership and borrow boundaries by using a novel pointer structure Ptr, enabling the translation of complex C pointer operations—including aliasing and pointer arithmetic—into safe Rust code while confining unavoidable unsafe operations (raw pointer dereference/casts and C FFI) to the trusted runtime. We implement our approach for the Clight subset of C, as defined in the CompCert verified compiler. Evaluation on a suite of benchmarks demonstrates that the main test cases in CompCert’s test suite are successfully translated. Their functional correctness is validated by comparing with the reference C compilers such as Clang and GCC.
The physical memory allocator is a foundational component of an operating system, whose functional correctness is paramount for system reliability. Although Rust provides compile-time memory safety, it cannot guarantee the correctness of allocator-specific implementation logic. This paper presents the formal verification of UtManager, a Rust-based buddy physical memory allocator. Leveraging the Verus verification tool, we define state invariants and provide function specifications for the bitmap-based Rust implementation. We prove that operations such as allocation and free preserve these invariants and satisfy their postconditions, while ensuring bounds safety, overflow freedom, and termination. Notably, during verification, we uncovered and fixed a previously unknown control-flow defect in the original code. These results demonstrate that formal methods can enhance the reliability of Rust-based memory management components with zero runtime overhead.
Regular expressions (regexes) are widely used but error-prone, making effective testing critical. A common testing approach involves generating a set of strings from a given regex and checking whether they are accepted or rejected as intended. However, existing string generation methods focus mainly on matching strings, overlooking non-matching strings that are crucial for detecting overly restrictive errors, a type of fault that accounts for a majority of real-world regex bugs. In this paper, we propose a method for systematically generating non-matching strings to test regexes. We adapt graph-based edge-pair coverage to the complement automaton of the regex and perform a depth-first traversal to generate a set of non-matching strings satisfying this criterion. To keep test suites compact, we incorporate a three-level reduction strategy including alphabet-level reduction, path-level reduction, and semantic-level filtering. Experimental results on a dataset containing 1,738 faulty regexes detectable by non-matching strings show that our method achieves 68.53 × improvement over the nearest competitor. Furthermore, it yields compact test suites with an average of 24 strings per regex, where 90 ≤ 10 .
As NAND flash-based storage systems operate over time, wear-induced degradation gradually increases page- and block-level faults, threatening system reliability. Existing bad block management (BBM) schemes are typically triggered by hard failure events such as uncorrectable errors or program failures, which fail to capture the gradual evolution of degradation and often lead to reactive management and concentrated reserved block consumption. To address these limitations, this paper proposes a Health-State-Aware Adaptive Bad Block Management method (HABBM). HABBM constructs a lightweight block-level health-state model based on bad-page accumulation and ECC-correctable errors (CE), and incorporates system-wide wear information through an adaptive threshold mechanism to dynamically classify blocks and regulate management decisions. By enabling proactive identification and protection of degraded blocks, HABBM mitigates concentrated replacement behaviors and smooths reserved resource consumption. Experiments using a configurable flash-level simulator with real-world workloads show that HABBM increases the supported cumulative host writes by approximately 1.64–2.04 × compared with representative BBM schemes while maintaining low runtime overhead, demonstrating its effectiveness in improving flash storage reliability.
Formal verification of Rust programs using Verus provides rigorous correctness guarantees but demands significant manual effort to craft auxiliary specifications and proofs. While Large Language Model (LLM) agents such as AutoVerus show promise for automating this process, they often fail on non-trivial tasks because generation is under-grounded: the model lacks access to fine-grained, verification-relevant proof patterns. Naïve retrieval-augmented generation (RAG) is also ineffective, since retrieving coarse-grained entire files or functions introduces noise and obscures the fine-grained logical patterns required for verification. To bridge this gap, we present VerusSeek, a retrieval-augmented framework for automated Verus proof synthesis that addresses this granularity mismatch. VerusSeek semantically chunks verified Verus code into proof constructs (e.g., contracts, loop invariants, lemmas, proof blocks, and assertions), performs type-aware retrieval, and applies hierarchical context expansion to provide concise yet logically grounded evidence to the model. We evaluate VerusSeek on 150 VerusBench tasks, showing that our fine-grained approach substantially improves verification success and significantly outperforms both AutoVerus and the RagVerus, with improvements of 76.7
