Concept
Tableau de bits
Publications associées (37)
On algebraic array theories
Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...
New York2023Bit-Line Computing for CNN Accelerators Co-Design in Edge AI Inference
David Atienza Alonso, Giovanni Ansaloni, Alexandre Sébastien Julien Levisse, Marco Antonio Rios, Flavio Ponzina
By supporting the access of multiple memory words at the same time, Bit-line Computing (BC) architectures allow the parallel execution of bit-wise operations in-memory. At the array periphery, arithmetic operations are then derived with little additional o ...
2023Overflow-free compute memories for edge AI acceleration
David Atienza Alonso, Giovanni Ansaloni, Alexandre Sébastien Julien Levisse, Marco Antonio Rios, Flavio Ponzina
Compute memories are memory arrays augmented with dedicated logic to support arithmetic. They support the efficient execution of data-centric computing patterns, such as those characterizing Artificial Intelligence (AI) algorithms. These architectures can ...
2023Combinatory Array Logic with Sums
We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combi- natory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragment ...
2023On Verified Scala for STIX File System Embedded Code using Stainless
We present an approach for using formal methods in embedded systems and its evaluation on a case study. In our approach, the developers describe the system in a restricted subset of the high-level programming language Scala. We then use 1) a verification s ...
2022Horizontal side-channel full key recovery on ephemeral SIKE
Natacha Yolande Emmanuel Marie Linard de Guertechin, Aymeric Genet, Novak Kaluderovic
This paper describes the first practical single-trace side-channel power analysis of SIKE. The attack exploits the nature of elliptic curve point addition formulas which require the same function to be executed multiple times. We target the three point lad ...
2021