This article presents the first systematic study to evaluate a suite of automated fuzzing techniques for Maximum Satisfiability (MaxSAT) solvers. It combines large-scale stress testing with a novel MaxSAT-specific delta debugging method to assess and improve solver robustness. A parallel framework orchestrates the generation of millions of structured MaxSAT instances. It efficiently isolates failure-inducing input and distills failing cases into minimal counterexamples for precise failure localization. Over a 100-hour fuzzing effort, this approach revealed previously unknown failures in almost all 43 solvers from recent MaxSAT competitions and in three certificate-producing solvers. Failures ranged from crashes and incorrect optimality bounds to severe performance slowdowns. Notably, a critical soundness error was identified in one certified solver. The resulting corpus of minimal counterexamples was published as a public regression suite. This suite was adopted as a mandatory check in the 2024 MaxSAT Evaluation, helping cut average solver failure rates by more than half. The MaxSAT community quickly embraced these resources: some solver development teams have already integrated our fuzzer into their workflows. The complete tool chain and benchmark corpus are available at Zenodo (Paxian 2025a). Our study demonstrates that systematic fuzz testing coupled with targeted debugging can significantly raise the reliability standards of MaxSAT solvers and provide valuable resources for future solver development.

Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.

Throughout device testing, one key parameter to be considered is the switching activity (SWA) of the circuit under test (CUT). To avoid unwanted scenarios due to excessive power consumption during test, in most cases the SWA of the CUTs must be retained to a minimal value when the test stimulus is applied. However, there are specific cases where the opposite, namely, the SWA maximization within the CUT, or a certain submodule of it, can be proven beneficial. For example, during dynamic burn-in testing we aim at maximizing the internal stress by applying suitable stimuli. This can be done in a functional manner by following the software-based self-test paradigm. However, generating such suitable programs represents a costly and arduous task for the test engineers. We consider the case where the CUT is a pipelined processor core and we aim to maximize the SWA of certain core submodules. We present a comprehensive methodology based on formal methods, able to automatically generate the best two-instruction stress-inducing sequence for the targeted processor module. The generated stimulus is composed of a short, arbitrarily long repeatable sequence of a pair of assembly instructions, thus, guaranteeing the maximum possible constant SWA. The proposed method was applied to the OpenRISC 1200 and the RI5CY (PULP) processor cores demonstrating its effectiveness when compared to other methods. We show that the time for generating the best repeatable instruction sequence is limited in most cases, while the generated sequence can always achieve a significantly higher repeatable and constant SWA than other solutions.

In this article, we revisit the topic of generalizing proof obligations (POs) in bit-level property directed reachability (PDR). We provide a comprehensive study which: 1) determines the complexity of the problem; 2) thoroughly analyzes limitations of existing methods; 3) introduces approaches to PO generalization that have never been used in the context of PDR; 4) compares the strengths of different methods from a theoretical point of view; and 5) intensively evaluates the methods on various benchmarks from the hardware model checking as well as from AI planning.

During device testing, one of the aspects to be considered is the minimization of the switching activity of the circuit under test in order to steer clear of introducing problems due to device overheating. Nevertheless, there are also certain scenarios during which the maximization of switching activity of the circuit under test (CUT) or of certain parts of it could be proven beneficial e.g., during Burn-In (BI), where internal stress is often produced by applying suitable stimuli. This can be done in a functional manner based on Software-based Self-Test in order to avoid possible damages to the CUT and/or any kind of yield loss. However, the generation of suitable test programs for this task represents a non-trivial task. In this paper we consider a scenario where the circuitry to be stressed is a pipelined processor. We present a methodology, based on formal techniques, able to automatically generate the best functional stress stimuli, i.e., a short and repeatable sequence of assembly instructions, which is guaranteed to induce the maximum switching activity within a given target processor module over a pre-defined time period. For the purposes of our experiments we used the OpenRISC 1200. The gathered experimental results demonstrate the effectiveness of the developed method. In particular, we show that the time for generating the best instruction sequence is limited in most cases, while the generated sequence can always achieve a significantly higher sustained toggling activity than any other solution.

Reconfigurable Scan Networks (RSNs) allow flexible access to embedded instruments for post-silicon validation and debug or diagnosis. However, the increased observability and controllability can be exploited by an attacker to manipulate or read out sensitive data, if no adequate precautions are taken by the designer. For large RSNs taking those precautions without algorithmic support is virtually impossible. This work proposes a method to automatically generate “minimal witnesses” demonstrating security weaknesses w.r.t. data flow in RSNs. The method provides condensed information to the designer on how to prevent data flow attacks, e.g. by locally modifying the RSN or by preventing active scan paths which contain those minimal witnesses. Experimental results confirm the applicability of the proposed method to diverse benchmark sets, including large designs. Additionally, the benefit of generating “minimal witnesses” for security weaknesses is shown.

The evaluation of fault attacks on security-critical hardware implementations of cryptographic primitives is an important concern. In such regards, we have created a framework for automated construction of fault attacks on hardware realization of ciphers. The framework can be used to quickly evaluate any cipher implementations, including any optimisations. It takes the circuit description of the cipher and the fault model as input. The output of the framework is a set of algebraic equations, such as conjunctive normal form (CNF) clauses, which is then fed to a SAT solver. We consider both attacking an actual implementation of a cipher on an field-programmable gate array (FPGA) platform using a fault injector and the evaluation of an early design of the cipher using idealized fault models. We report the successful application of our hardware-oriented framework to a collection of ciphers, including the advanced encryption standard (AES), and the lightweight block ciphers LED and PRESENT. The corresponding results and a discussion of the impact to different fault models on our framework are shown. Moreover, we report significant improvements compared to similar frameworks, such as speedups or more advanced features. Our framework is the first algebraic fault attack (AFA) tool to evaluate the state-of-the art cipher LED-64, PRESENT and full-scale AES using only hardware-oriented structural cipher descriptions.