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.
