IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas

Charlas Invitadas

Albert Rubio

Monday, February 13, 2023

11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @s3)

Albert Rubio, Professor, Universidad Complutense de Madrid, España

Circom: Scalability and security for building ZK proving systems

Abstract:

The most widely studied language for expressing statements in the context of Zero-Knowledge (ZK) proofs is arithmetic circuit satisfiability. In this talk we present circom, a programming language and a compiler that allows the programmer to provide a low-level description of the arithmetic circuit together with an effective way to execute it. Challenging constraint manipulation and analysis problems will be introduced as well as some safety properties of circom programs that need to be checked. New language features focused on enhancing security will be discussed.


Time and place:
11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Pierre Sutra

Tuesday, February 7, 2023

11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @s3)

Pierre Sutra, Associate Professor, Telecom SudParis, Francia

J-NVM: Off-heap Persistent Objects in Java

Abstract:

Non-volatile main memory (NVMM) is a new tier in the memory hierarchy that offers jointly the durability of spinning disks, near-DRAM speed and byte addressability. This talk presents J-NVM, a fully-fledged interface to use NVMM in the Java language. J-NVM relies on proxy objects that intermediate direct off-heap access to NVMM. We present the internals of J-NVM and how to use it in the context of a modern distributed data store. This talk is based on a paper in SOSP'21: http://www-public.it-sudparis.eu/~thomas_g/research/biblio/2021/lefort-sosp-jnvm.pdf


Time and place:
11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Sebastian Uchitel

Thursday, February 2, 2023

11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @s3)

Sebastian Uchitel, Professor, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad De Buenos Aires, Argentina.

Runtime Synthesis for Self-Adptation

Abstract:

Self-adaptation is often defined as the ability of systems to alter at runtime their behaviour in response to changes in their environment, capabilities and goals that were unforseen at design time. I will discuss why I believe one interesting route to achieving self-adaptation is to endow systems with the capability of synthesising at runtime discrete event controllers.I will provide an overview of the work we have done in this direction and some of the challenges that remain, covering software architectures, modelling and learning approaches for defining novel discrete event cotrol problems, and algorithms to solve them.


Time and place:
11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Dmitry Chistikov

Tuesday, January 31, 2023

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: @s3)

Dmitry Chistikov, Associate Professor, Universidad de Warwick, Reino Unido

Subcubic certificates for the CFL reachability problem

Abstract:

The context-free language (CFL) reachability problem on graphs (as well as a closely related problem of language emptiness for pushdown automata) is a core problem for interprocedural program analysis and model checking. It can be solved in cubic time but, despite years of efforts, there is no truly sub-cubic algorithm known for it.

We study the related certification task: given a problem instance, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that there exist succinct certificates, of quadratic size, which can be checked in subcubic (matrix multiplication) time.

In this talk, I will introduce CFL reachability and standard algorithms for it and discuss our certification results. I will also discuss the question of whether faster algorithms for CFL reachability could lead to faster algorithms for other combinatorial problems such as SAT (a "fine-grained complexity" question).


Time and place:
11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: @s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Sebastian Uchitel

Monday, January 30, 2023

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: @s3)

Sebastian Uchitel, Professor, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad De Buenos Aires, Argentina.

Predicate Abstractions for Smart Contract Validation

Abstract:

Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to hire independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this talk, I will discuss our experience using predicate abstraction to construct models which can be used by auditors to explore and validate smart contact behaviour at the function call level by proposing predicates that expose different aspects of the contract.


Time and place:
11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: @s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Charlas Invitadas - 2022