Publications associées à A Sub-VT 2T Gain-Cell Memory for Biomedical Applications

Scaling Language Features for Program Verification

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Exploration Methodology for BTI-Induced Failures on RRAM-Based Edge AI Systems

David Atienza Alonso, Miguel Peon Quiros, Alexandre Sébastien Julien Levisse, Marco Antonio Rios

Resistive switching memory technologies (RRAM) are seen by most of the scientific community as an enabler for Edge-level applications such as embedded deep Learning, AI or signal processing of audio and video signals. However, going beyond a "simple'' repl ...

IEEE2020

Stoic: Towards Disciplined Capabilities

Martin Odersky, Sandro Stucki, Nada Amin, Fengyun Liu, Paolo Giosuè Giarrusso

Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasonin ...

2020

Contract-Based Resource Verification for Higher-Order Functions with Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...

Assoc Computing Machinery2017

Verification by Reduction to Functional Programs

Régis William Blanc

In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...

EPFL2017

Circuit Designs of High-Performance and Low-Power RRAM-Based Multiplexers Based on 4T(ransistor)1R(RAM) Programming Structure

Giovanni De Micheli, Xifan Tang, Pierre-Emmanuel Julien Marc Gaillardon, Edouard Giacomin

Routing multiplexers based on pass-transistors or transmission gates are an essential components in many digital integrated circuits. However, whatever structure is employed, CMOS multiplexers have two major limitations: 1) their delay is linearly related ...

Ieee-Inst Electrical Electronics Engineers Inc2017