Fully homomorphic encryption (FHE) allows neural network inference to be performed directly on encrypted data and models, preserving end-to-end privacy. One of the most widely used FHE schemes, CKKS, supports approximate arithmetic over real numbers and is well-suited for computing polynomial operations. However, CKKS does not natively support conditional branching, making it unsuitable for non-linear functions such as ReLU, which behaves differently depending on whether the input is negative or nonnegative. To address this, ReLU is typically approximated using polynomials. Unfortunately, this approach introduces two key drawbacks: (1) the approximation is only valid within a certain input range, and (2) identifying this range typically requires prior exposure of cleartext data to perform profiling, thus partially compromising privacy. This requirement is problematic in practice, as small profiling errors can lead to substantial accuracy degradation. On the other hand, the TFHE scheme supports binary gate-level computation, enabling precise implementation of conditional operations such as ReLU. Yet TFHE lacks the SIMD capabilities of CKKS, leading to significant computational latency. This paper explores the use of scheme switching for encrypted neural network inference: leveraging CKKS for polynomial-compatible layers and switching to TFHE for layers that require conditional logic, such as ReLU. We demonstrate that this hybrid approach substantially improves the numerical fidelity of encrypted neural network inference: while polynomial approximations suffer from numerical divergence, scheme switching more closely matches non-encrypted inference.

This paper presents a novel approach to accelerate applications running on integrated CPU-GPU systems. Many integrated CPU-GPU systems use cache-coherent shared memory to communicate. For example, after CPU produces data for GPU, the GPU may pull the data into its cache when it accesses the data. In such a pull-based approach, data resides in a shared cache until the GPU accesses it, resulting in long load latency on a first GPU access to a cache line. In this work, we propose a new, push-based, coherence mechanism that explicitly exploits the CPU and GPU producer-consumer relationship by automatically moving data from CPU to GPU last-level cache. The proposed mechanism results in a dramatic reduction of the GPU L2 cache miss rate in general, and a consequent increase in overall performance. Our experiments show that the proposed scheme can increase performance by up to 37%, with typical improvements in the 5–7% range. We find that even when tested applications do not benefit from the proposed approach, their performance does not decrease with our technique. While we demonstrate how the proposed scheme can co-exist with traditional cache coherence mechanisms, we argue that it could also be used as a simpler replacement for existing protocols.

Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modelling tools like Statemate support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of Statemate enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high-speed train signalling system where the tool has been applied successfully.

This paper considers model checking of Markov reward models (MRMs), continuous-time Markov chains with state rewards as well as impulse rewards. The reward extension of the logic CSL (continuous stochastic logic) is interpreted over such MRMs, and two numerical algorithms are provided to check the reachability of a set of goal states under a time and an accumulated reward constraint. This extends existing model-checking techniques for MRMs with just state rewards, and improves the applicability to thousands of states. Our approach is illustrated by using rewards for energy consumption in the setting of dynamic power management.