Simulation to Silicon: A Unified Concurrency Abstraction for Portable Verification Testbenches

Runtime Verification of Interleaved Concurrent Systems with Shared-Variable Communication

The paper introduces a comprehensive framework for parallel runtime verification designed to monitor concurrent systems that utilise shared-variable communication mechanisms operating under interleaved concurrency model. The proposed framework validates system behaviour during execution to confirm adherence to correctness specifications or identify violations thereof. Concurrent systems necessitate distinct correctness criteria compared to sequential programs, particularly regarding deadlock avoidance and mutual exclusion protocols when multiple processes access shared resources under interleaved concurrency models. Traditional sequential verification frameworks lack the architectural capability to monitor parallel systems effectively, as they are fundamentally designed to track single processes rather than multiple concurrent processes executing simultaneously. This work addresses various challenges in ensuring correctness of parallel programs at both hardware and software layers while providing a theoretical analysis comparing verification methodologies including theorem proving, model checking, testing, and runtime verification. The framework uses Interval Temporal Logic (ITL) as its formal foundation alongside its expressive power for specifying complex temporal properties of parallel systems. A detailed exposition of the framework's core components, their operational roles, and their integration within the overall verification architecture is presented, demonstrating the practical applicability of runtime verification techniques for ensuring correctness in parallel computing environments.

Performance and Security Tradeoffs in Microservices Communication: Evaluating Reactive and Virtual-Thread Architectures Under Security-Enabled Systems

Ensuring robust security without compromising performance remains a persistent challenge in microservices architectures. Reactive, non-blocking frameworks are often recommended for high-concurrency workloads, yet the introduction of virtual threads in the Java platform (Project Loom) raises a question of whether reactive programming retains a performance advantage when a blocking REST-based implementation can offload thread management to the JVM. This paper presents and empirically evaluates a reactive microservices architecture integrating multi-layered security mechanisms, including Mutual Transport Layer Security (mTLS), JWT based token binding, Role-Based Access Control (RBAC), and Claim-Based Access Control (CBAC), and compares it against a functionally equivalent REST-based counterpart using virtual threads, Apache Tomcat, and REST/JSON interservice communication under identical security configurations. The system employs RSocket for inter-service communication and Protocol Buffers for low-overhead binary serialization. Load tests with 100, 300, and 500 concurrent users show that virtual threads substantially reduce the end-to-end latency and throughput differences between the two architectures. The reactive implementation consistently achieves lower CPU utilization at the API Gateway, up to six times lower at 300 concurrent users, demonstrating that non-blocking execution remains more resource-efficient even when virtual threads mitigate explicit thread blocking. Both architectures sustain zero failed requests across all load levels. These results indicate that the choice between reactive and virtual-thread-based REST involves a trade-off between resource efficiency and implementation complexity while maintaining high-security guarantees.

Synchronized Transitions Based on Event Streaming ⋆

A Lightweight Verification Framework for RISC-V SoCs Based on RTL Lint and Differential Testing

Multi-Mode Debugging for FRP-Based Embedded Systems

Emfrp is a functional reactive programming (FRP) language designed for small-scale embedded systems. Time-varying values are the primary abstraction mechanism in FRP and enable concise descriptions of reactive behavior. In practice, however, Emfrp programs are compiled into C and combined with platform-dependent input/output components written in C or C++. Consequently, developers must debug the resulting mixed C/C++ program using conventional debuggers such as GDB, even though the application logic is written in Emfrp. This situation creates an abstraction gap between the source-level FRP program and the executable system. This paper presents a multi-mode debugging framework for Emfrp-based embedded applications. The framework supports debugging at the level of Emfrp abstractions while also allowing inspection of platform-specific C/C++ I/O code. Our approach uses a source code mapping technique that relates Emfrp constructs to corresponding locations in the compiled program. A case study on an ESP32 microcontroller using representative debugging scenarios demonstrates improved debugging efficiency.

BTOR2-Based C Program Verification via Hardware Model Checking

Program verification tools often rely on specific intermediate representations and analysis backends, limiting the reuse of verification algorithms and model checkers across frameworks. In contrast, hardware model checking has developed a mature backend ecosystem, where standard formats such as BTOR2 support reusable algorithms for counterexample search and inductive safety proving. Applying these capabilities to C requires translating assertion-based programs into transition systems that hardware model checkers can directly process. We present C2Btor, a method for encoding such verification tasks into BTOR2 models. C2Btor uses a program counter to capture control transfers, represents data states and memory objects with bit-vectors and arrays, and maps assumptions and assertion checks into BTOR2 constraints and bad-state properties. We evaluate C2Btor on SV-COMP C ReachSafety benchmarks and a curated assertion-category benchmark suite, comparing it with representative program verification tools. C2Btor correctly solves 263 tasks, 101 more than CBMC configured with bounded model checking, and is especially effective on bit-vector benchmarks, where it solves 75.5% of the tasks with no wrong verdicts. These results show that the BTOR2 route allows C program verification to benefit from advances in hardware model-checking backends, expanding the available capability for counterexample search, inductive safety proving, and word-level transition-system reasoning.