Areion is a family of wide-block permutations proposed at CHES 2023. For the security against differential attacks of Areion, the designers showed only upper bounds of the differential characteristic probability, which are derived from the lower ...

The configuration space of some systems is so large that it cannot be computed. This is the case with the Linux Kernel, which provides almost 19,000 configurable options described across more than 1,600 files in the Kconfig language. As a result, many ...

This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider ...

The difficulty of factoring large integers into primes is the basis for cryptosystems such as RSA. Due to the widespread popularity of RSA, there have been many proposed attacks on the factorization problem such as side-channel attacks where some bits ...

A good differential is a start for a successful differential attack. However, a differential might be invalid, i.e., there is no right pair following the differential due to some contradictions in the conditions imposed by the differential. In ...

Recent approaches on verification and reasoning solve SAT and QBF encodings using state-of-the-art SMT solvers, as it “makes implementation much easier”. The ease-of-use of these solvers make SAT and QBF solvers less visible to users of solvers—...

Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the ...

We present a hardware-accelerated SAT solver targeting processor/Field Programmable Gate Arrays (FPGA) SoCs. Our solution accelerates the most expensive subroutine of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, Boolean Constraint Propagation (...

SPECK and SPARX are two kinds of block ciphers with an ARX structure. In this paper, we use the SAT-based automatic search tool to search for linear approximations of these two ARX ciphers. As a result, we find a linear approximation for 17-round ...

For several decades, much effort has been put into identifying classes of CNF formulas whose satisfiability can be decided in polynomial time. Classic results are the linear-time tractability of Horn formulas (Aspvall, Plass, and Tarjan, 1979) ...

Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on ...

Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict ...

Linear temporal logic ($\mathsf{LTL}$) and its variant interpreted on finite traces (${\mathsf{LTL}}_{\mathsf{f}}$) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the ...$\mathsf{}$${\mathsf{}}_{\mathsf{}}$$\mathsf{}$${\mathsf{}}_{\mathsf{}}$

The linear structure technique was developed by Guo et al. at ASIACRYPT 2016, notably boosting the preimage attacks on Keccak. This technique transforming the preimage attack into solving algebraic systems allows entire linearization of the ...

Hypertree width is a prominent hypergraph invariant with many algorithmic applications in constraint satisfaction and databases. We propose two novel characterisations for hypertree width in terms of linear orderings. We utilize these ...

We consider semidefinite programming (SDP) approaches for solving the maximum satisfiability (MAX-SAT) problem and weighted partial MAX-SAT. It is widely known that SDP is well-suited to approximate (MAX-)2-SAT. Our work shows the potential of SDP also ...

Feature models are commonly used to specify the valid configurations of product lines. As industrial feature models are typically complex, researchers and practitioners employ various automated analyses to study the configuration spaces. Many of ...

SAT, SMT, MILP, and CP, have become prominent in the differential cryptanalysis of cryptographic primitives. In this paper, we review the techniques for constructing differential characteristic search models in these four formalisms. Additionally, ...

We present an asymptotic improvement in the number of variables (n + m⌊log 2(k − 1)⌋) required for state-of-the-art formulation of (max-)k-SAT problems when encoded as a quadratic unconstrained binary optimization (QUBO) problem. We further show a ...

Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark ...