Yves Bertot, in his pedagogical wisdom, gives the following simple problem in his introduction to the Rocq Proof Assistant: “Is the product of two consecutive natural numbers even?” This simple problem is a classical exercise in elementary mathematics, but tackling it mobilizes all the growing cognitive faculties of the learner, from decomposing this informal mathematical statement into its components – from what it means for two natural numbers to be consecutive to the nature of even numbers – to formalizing these components, composing the results of these formalizations into a suitably quantified formal mathematical statement, and then proving this statement formally. The problem can be fruitfully generalized to investigating the divisibility properties of the product of three (or four, or five, ...) consecutive natural numbers. Overall, Yves Bertot’s simple problem gives rise to an engaging adventure of mathematical and computational discovery (as well as to one of self-discovery), which the present article describes.
SMT solvers form critical infrastructure for many verification and program analysis systems. Recent fuzzing efforts since 2019 have significantly improved solver robustness, yet these approaches often fall short of systematically probing the diverse semantic subspaces within a formula's satisfiability domain. This paper introduces subspace diversification, which systematically partitions the solution space of seed formulas to guide solvers into exploring different behavioral regions. We instantiate the idea using three general, bounded, and efficient mutation strategies that confine the space with cubes, numerical domains, and quantifiers. An extensive evaluation on Z3 and CVC4 demonstrates the effectiveness of our implementation, Canary, which uncovered 108 confirmed bugs across multiple theories and bug types.
Both the precision and performance of abstract interpreters can be improved greatly through the integration of abstract garbage collection (GC). Unfortunately, for abstract interpreters that do not explicitly model the stack (e.g., abstract definitional interpreters), this integration has proven cumbersome. Existing approaches either fail to exploit the full precision and performance benefits of abstract GC and pushdown control flow, and/or require complicated modifications to the abstract interpreter. In addition, the lack of global store widening, which is incompatible with abstract GC, often remains an obstacle for scalability. In this work, we present delta store semantics (DSS), offering a novel yet simple approach to integrate abstract GC into big-step abstract definitional interpreters. DSS makes a simple change to the standard big-step language semantics, returning a delta store (representing changes to the original store) instead of an updated store, enabling the integration of a single evaluation rule to interleave GC into its semantics. Importantly, we show that DSS not only preserves the advantages of big-step abstract interpreters and abstract GC, but in fact can exploit greater precision benefits (due to more aggressive GC). We formulate this claim as a theorem, for which we provide both a mechanised proof in Rocq, as well as empirical evidence. Finally, we propose a new form of store widening for DSS, which tackles the scalability issues of abstract interpreters employing abstract GC without store widening. The result is similar to the traditional notion of flow sensitivity in data-flow analyses.
Abstract definitional interpreters are an approach to developing abstract interpretation-based static analyses in which language semantics are expressed through monadic recursive interpreters. These interpreters are then instantiated with an abstract value domain and executed in a suitable monadic context that carries abstract program state. Unfortunately, correctly implementing these definitional interpreters remains a difficult task. Moreover, instantiating analyses requires configuring many components. In this tool paper, we present the design of a framework called Monarch that provides reusable components to programmers for implementing abstract definitional interpreters. Our design consists of the following components: abstract domains, a framework for expressing program semantics, and analysis instantiation techniques. Finally, we present an implementation in Haskell and give example instantiations in Scheme and Python to show how these components are used.
Design-by-technique for CESK machines. Intended solely to introduce the concept of soft contract verification, these purpose-built analyses lack configurability. In this paper, we propose a novel static analysis for soft contract verification called abstract concolic execution. We systematically abstract a concolic execution, which is a form of dynamic symbolic execution, into abstract concolic execution, rendering the technique terminating and sound for any program input. To show that our analysis is more configurable than the state-of-the-art analysis supporting soft contract verification, we propose two variations of the analysis. Finally, we show that our approach is comparable to if not more precise than the state of the art at the cost of performance. We find that in 10 out of the 24 benchmark programs, our approach is more precise than the state-of-the-art approach, while being as precise in 9 of them and less precise in 5.
Adversarial examples undermine the reliability of neural networks. To defend against attacks, multiple approaches have been proposed. However, many of them introduce high training overhead or high inference overhead, some significantly decrease the network’s accuracy or insufficiently increase the network’s robustness, and others do not scale to deep networks. To mitigate all these shortcomings, we propose a new form of defense: optimal program synthesis of short repair programs, integrated into a trained network. A repair program modifies a few neurons by using a few other neurons. The challenge is to identify the most successful combination of neurons to enhance the network’s robustness while maintaining high accuracy. We introduce DefEnSyn, a stochastic synthesizer of repair programs. To cope with the exponential number of neuron combinations, DefEnSyn learns the effective combinations by synthesizing repair programs of increasing length. We evaluate DefEnSyn on classifiers for ImageNet and CIFAR-10 and show it enhances the robustness of networks to L_∞ -, L_2 -, and L_0 - black-box adversarial example attacks and to backdoor attacks. DefEnSyn ’s repair programs enhance the networks’ robustness on average by +40% and up to +71% . DefEnSyn decreases the network’s accuracy by only ≈ -1% . We demonstrate that DefEnSyn outperforms existing state-of-the-art defenses based on adversarial training, randomization, and repair, in both robustness and accuracy.
Equality saturation is a semantics-based technique for automatically and efficiently proving that two programs are equivalent modulo a fixed set of equality axioms. In this paper, we extend the equality saturation technique with contextual reasoning in order to perform rewriting under assumptions that are locally valid inside a conditional branch. This is based on a new notion of cyclic e-graphs with contextual annotations. We experimentally validate the efficiency and scalability of this new technique by proving equivalence of several families of programs where contextual reasoning is required.
The software landscape is showing consistent, accelerated growth in the volume of code developed using dynamic languages. These languages are characterized by dynamic typing and more lax preemptive checks, which allow rapid application development and shorter development cycles. The vast majority of these languages are interpreted; that is, programs are executed by an interpreter in a managed runtime environment. Such interpreters incur significant performance hits, and, to counter that, modern runtime environments usually employ some sort of optimization. The most common one is Just-in-Time compilation (JIT), which translates source code on-demand into native code that can run much faster. Some notable JIT engines (such as V8 for JavaScript) exhibit impressive speedups. Still, in most realistic scenarios, they cannot surpass the performance of hand-crafted native code written in a low-level language like C. There are inherent reasons for why Ahead-of-Time compilation (AOT) is rarely practiced with dynamic languages. Since variables are dynamically typed, this will require most of the type-checking to be done at runtime still, thus limiting the range of optimization that can be performed ahead of time, consequently limiting the benefit of AOT compilation. We propose an approach that utilizes static analysis for the purpose of sound type inference, which can then be leveraged for code generation requiring a minimal amount of runtime type checks. Unlike previous work in this area, our approach eliminates the need for the JIT at runtime. Indeed, for programs that avoid using inherently dynamic features (such as or reflection) we can eliminate the need for a managed runtime altogether. Our preliminary results show that programs compiled ahead-of-time using our approach achieve substantial speedups compared to execution in a purely interpreted environment. These speedups are greater than previous efforts in that area. In some cases, our results even come close to execution times using an interpreter with a JIT compiler. This lets us believe that, with further improvements, this methodology can be utilized to surpass JIT speedups.
We establish a formal relation between quantitative and semantic approximations-formalized by pre-metrics and upper closure operators (ucos), respectively-by means of Galois connections. This connection reveals that it is far from trivial for a pre-metric to uniquely identify a uco, highlighting the structural constraints and, more generally, the distinct identity inherent to semantic approximations. Building on this foundation, we introduce a general composition of semantic and quantitative approximations. This allows us to define a new confidentiality property, called Partial Abstract Non-Interference, that measures bounded variations in program behavior over abstract properties of data. We then relate this property to Partial Completeness in abstract interpretation, revealing a deeper connection between static analysis precision and security guarantees.
We present PyRAT, a tool based on abstract interpretation to verify the safety and robustness of neural networks. PyRAT uses multiple abstractions to find the reachable states of a neural network starting from its input. Its analysis is fast and accurate. PyRAT has already been used in several industrial and academic collaborations, to ensure safety guarantees, with its second place at the VNN-Comp 2024 showcasing its performance.
The eBPF verifier ensures the safety of user-supplied programs before they are executed in the Linux kernel, relying on abstract interpretation. While the verifier's analysis must be sound, its utility hinges on precision. An overly conservative abstract operator can routinely cause the verifier to reject safe programs. In this paper, we introduce a framework for systematically comparing and validating the precision of competing abstract operator implementations used within the verifier. We provide a formal specification of the precision relationship between two abstract operators across all valid abstract inputs. However, reasoning about all valid abstract inputs over-approximates what is actually reachable in real verifier executions. This is because the eBPF verifier performs verification from a specific set of initial abstract states. Hence, many abstract inputs used in theoretical comparisons may never arise in practice. To address this gap, we propose SMT-based program synthesis to automatically generate concrete eBPF witness programs, explicitly demonstrating observable precision differences in actual verifier executions. Using these techniques and tools, we crafted a more precise multiplication abstract operator in the verifier, bpf_mul. Our multiplication patch has been upstreamed to the Linux kernel where the witness produced by our approach provided demonstration to the kernel developers. We have also used these techniques to check the precision of numerous kernel patches related to abstract operators in the eBPF verifier.
We present AURA, a novel abstract interpretation for obtaining sound, precise bounds on the posterior distributions computed by probabilistic programs. AURA allows programmers to specify interval bounds that capture uncertainty or perturbations of the observed data. AURA abstractly computes the infinite set of posteriors that would result from performing inference for any possible data value in the specified perturbation range. AURA then certifies precise bounds on probabilistic queries over that set of posteriors. AURA's precision stems from a novel gradient-based optimization leveraging the structure of probabilistic programs. Our evaluation across 11 benchmarks with data perturbation shows that AURA improves precision by an order of magnitude (12.8x on average) over the interval-based abstract interpreter, within a run time of 3.1 s (geomean), using a GPU parallel implementation.
This paper formalizes future conditions, which complement traditional pre- and post-conditions to provide a more comprehensive specification of each function's behaviour and expectation. Pre-conditions govern the required states before each function call, while post-conditions define the immediate outcomes (post-states) upon completion. Future conditions extend this paradigm by specifying expected temporal behaviors and states that manifest after the function call has finished, potentially affecting subsequent operations or program states. Together, these three types of conditions form a robust specification mechanism for reasoning about API behaviors across various temporal contexts. However, existing techniques for reasoning about future conditions have three key limitations: inefficient entailment checking, under-approximation of program behaviors, and bounded loop unrolling. To address these challenges, we propose a set of over-approximating Hoare-style forward rules that accommodate future conditions that are processed once per method declaration. Moreover, we propose a novel solution for modelling recursive behaviors via a bag of future conditions, which can be heuristically synthesized and verified in the verification system. We formally prove the soundness of our proposal in Coq and use experimental results to demonstrate its effectiveness in detecting non-trivial, real-world API misuses.
Long Range Wide Area Networks (LoRaWANs) have become a popular candidate for energy efficient networks like the Internet of Things (IoT). For the connection of remote regions, satellites in Low Earth Orbit (LEO) can be used to support the terrestrial LoRaWAN. LEO enables transmission from IoT devices with a very low transmit power. However, it also leads to high Doppler shifts as well as high Doppler rates. Both effects deteriorate the Long Range (LoRa) communications performance tremendously. Whereas new LoRa technologies are developed for systems with high Doppler effects, they are not backward compatible, i.e., they cannot be used for LoRa sensors which have already been deployed. In this paper, we propose a Doppler rate mitigation method which reduces these negative effects by subtracting an estimated Symbol Error (SE). Here, estimation is based on an adaptive linear regression method exploiting all LoRa symbols of a packet, compared to state-of-the-art techniques whose linear regression approachs are only using preamble symbols. Simulation results show that the proposed method tremendously outperforms state-of-the-art techniques, especially at high Doppler rates.
Reconfigurable intelligent surface (RIS) is a promising technology to enhance the spectral and energy efficiency in B5G/6G systems. Channel estimation in RIS-aided systems is quite challenging due to the passive architecture of the RIS. Since RIS consists of a large number of reflecting elements, we need many phase shift allocations during the channel estimation phase to estimate the RIS-associated channels perfectly. In the absence of a sufficient number of pilot or phase shift sequences during the training phase, we get imperfect channel state information (CSI), which can significantly degrade the overall performance of the system. In this work, we analyse the effects of limited pilot and phase shift sequences on the asymptotic performance of the RIS-aided systems. We also optimise the achievable sum-rate of the system in the absence of full pilot and phase shift sequences.
Unmanned aerial vehicle (UAV)-aided communications may suffer from the coexistence with existing network infrastructure and the spectrum scarcity. Underlay cognitive radio technology should be employed to manage the secondary UAV-aided networks with the existing primary networks using the same frequency spectrum, where the interference to the primary network should be bounded. In this paper, we focus on the problem of multi-UAV-assisted underlay cognitive radio for multiple secondary users (SUs) and primary users (PUs). We establish an optimization problem to maximize the minimum throughput among SUs with respect to multi-UAV deployment locations, power and service ratio allocation. The problem is highly intractable due to its mixed-integer and non-convex nature. The problem is solved by decomposing it into two nested optimization problems. The inner problem involves joint power and service ratio allocation given the deployment location and UAV-SU allocation, which we transform equivalently into a convex optimization problem. The outer problem determines the multi-UAV deployment locations and UAV-SU allocation, solved via a metaheuristic method. Via this decomposition with the inner problem optimally solvable in polynomial time by a convex optimization solver, the search space of the metaheuristic algorithm is drastically reduced, resulting in an efficient nearoptimal algorithm for the complex problem. Numerical results demonstrate that the proposed approach achieves significant throughput improvement compared to baseline methods.
Combining sensing and communication into a single system allows the integration of radar sensors mounted on locally installed road side units into future intelligent transportation systems. These units have great potential to improve safety in dense intersection scenarios. However, this combined functionality is limited due to their potential interference. This paper investigates the influences of antenna characteristics on sensing and communication performance in crossing scenarios at 77 GHz. Different antenna characteristics are compared in ray-tracing simulations. The radar sensing performance is evaluated based on the maximum peak detection in the range-Doppler map, while the communication is evaluated based on the channel characteristics. The different antenna types achieve either a higher detection power in the angular region or a higher antenna focus. The communication is compared with respect to the root mean square delay spread and the minimum timing delay for an interferencefree frequency-modulated continuous wave (FMCW) sensing. The power of the line-of-sight path between the radar-equipped road side units varies over 20 dB between the different antennas. The alignment with each other results in even higher gains and losses. The results show that coordinating the different RSUs with an additional time or frequency scheduling is necessary. In the future, the intersection scene will be improved with more road users to investigate the antenna characteristics' impacts further.
This paper provides a solution for the joint activity detection and channel estimation (JADCE) problem in grant-free access with correlated device activity patterns. In particular, we consider a massive machine-type communications (mMTC) network operating in an event-triggered traffic mode. To this end, to encode the prior information about the correlated sparse activity pattern, the paper proposes a first-order Markov chain coupled with a sparsity-promoting spike and slab to capture the sparse and correlated activity pattern. Furthermore, we drive a hierarchical Bayesian parameter estimation using Markov chain Monte Carlo (MCMC) sampling to provide an efficient solution to the JADCE problem. Numerical results highlight improved activity detection accuracy and channel estimation quality performance.
In this paper, we introduce a novel time domain correlation based channel sounder that operates at 485 GHz. The channel sounder targets the Y-band ($330 \text{GHz}-500 \text{GHz}$) and covers a center frequency up to 500 GHz. The setup has been validated in the laboratory for conducted and over-the-air measurements. The conducted measurements report a dynamic range of around 80 dB without spurious peaks, and a linear behavior between added attenuation and dynamic range with constant relative noise floor. The over-the-air measurements report a match of the line-of-sight path's propagation length and normalized received power.
This paper outlines an advanced characterization procedure for a D-band dielectric lens made of polytetrafluoroethylene (PTFE), utilizing a WR6 waveguide probe as the feeding antenna. The proposed measurement setup is designed to effectively measure the radiation pattern for various source positions relative to the lens with a precision of $5 \mu\mathrm{m}$, enabling a comprehensive analysis of individual array elements in conjunction with the lens, for which it was measured a gain of 15.6 dBi at 150 GHz. By measuring complex scattering parameters at each position, the setup emulates a phased array configuration, and the coupling matrix is integrated from previously acquired simulated data. The emulated radiation patterns derived from the measurement results demonstrate strong correlation with fullwave electromagnetic simulations of the complete array, both for uniform and for linear-phase-shifted excitations. These findings validate the effectiveness of the technique for conducting arrayintegrated lens measurements, thereby contributing valuable insights for future antenna and lens design in high-frequency applications.
