IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series (S3)

Software Seminar Series (S3)

Isabel García

Wednesday, July 21, 2021

Isabel García, PhD Student, Instituto IMDEA Software

A scalable static analysis framework for reliable program development exploiting incrementality and modularity

Abstract:

Automatic static analysis tools allow inferring properties about software without executing it and without the need for human interaction. When these tools are based on formal methods, the properties are guaranteed to hold and come with a mathematical proof. The usage of these tools during the coding, testing, and maintenance phases of the software development cycle helps reduce efforts in terms of time and cost, as they contribute to the early detection of bugs, automatic optimizations, or automatic documentation. The increasing importance of the reliability of evolving software is evidenced by the current number of tools and on-line platforms for continuous integration and deployment. In this setting, when changes happen fast, analysis tools are only useful if they are precise and, at the same time, scalable enough to provide results before the next change happens. In this thesis we study scalable analyses in the context of abstract interpretation. Since a way to improve scalability is to perform coarser abstractions, we first inspect what effect this may have in effectively proving the absence of bugs. Second, we present a framework for scalable static analyses which is generic, that is, independent of the data abstraction of the program. We present several algorithms for incrementally reanalyzing whole programs in a context-sensitive manner, reusing as much as possible previous analysis results. A key novel aspect of the approach is to take advantage of the modular structure of programs, typically as defined by the programmer, while keeping a fine-grained relation between the analysis result and the source program. Additionally, we present a mechanism for the programmer to help the analyzer in terms of precision and performance by means of assertions. We show that these assertions together with incremental analysis are specially useful when analyzing generic code. All these algorithms have been implemented and evaluated for different abstract domains within the CiaoPP framework. Lastly, we present an application of the analysis framework to perform on-the-fly assertion checking, providing continuous and almost instantaneous feedback to the programmer as the code is written. Here the incrementality and modular nature of the presented algorithms, and the locality of the changes, are key to achieving fast response times.


Nicolas Mazzocchi

Tuesday, June 29, 2021

11:00am Online via Zoom: Zoom3 - https://zoom.us/j/3911012202

Nicolas Mazzocchi, Post-doctoral Researcher, Instituto IMDEA Software

Decomposing Permutation Automata

Abstract:

Compositionality is a fundamental notion in numerous fields of computer science. This principle can be summarised as follows: Every system should be designed by composing simple parts such that the meaning of the system can be deduced from the meaning of its parts, and how they are combined. For instance, this is a crucial aspect of modern software engineering: a program split into simple modules will be quicker to compile, easier to maintain and allowing concurrency. A deterministic finite automaton (DFA) A is composite if its language L(A) can be decomposed into an intersection L(A1) ∩ L(A2) ∩ ... ∩ L(Ak) of languages of smaller DFAs. Otherwise, A is prime. This notion of primality was introduced by Kupferman and Mosheiff in 2013, and while they proved that we can decide whether a DFA is composite, the precise complexity of this problem is still open, with a doubly-exponential gap between the upper and lower bounds. In this presentation, we focus on permutation DFAs, i.e., those for which the transition monoid is a group. By the use of structural criteria we are able to decide in NPTIME whether a permutation DFA is composite. Moreover, we investigate the class of commutative permutation DFAs for which we provide an NLOGSPACE procedure. Despite this low complexity (compared to the general case), we show that complex behaviours still arise in this class: we provide a family of commutative permutation DFAs each composite and requiring polynomially many factors with respect to its size.


Time and place:
11:00am Online via Zoom: Zoom3 - https://zoom.us/j/3911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Emanuele Giunta

Tuesday, June 22, 2021

11:00am Online via Zoom: Zoom3 - https://zoom.us/j/3911012202

Emanuele Giunta, PhD Student, Instituto IMDEA Software

Efficient and Universally Composable Single Secret Leader Election from Pairings

Abstract:

Single Secret Leader Election (SSLE) protocols allow a set of users to elect a leader among them so that the identity of the winner remains secret until she decides to reveal herself. This notion was formalized and implemented in a recent result by Boneh, et al. (ACM Advances on Financial Technology 2020) and finds important applications in the area of Proof of Stake blockchains. In this paper we propose new solutions to the problem that advance the state of the art both from a theoretical and a practical perspective. On the theoretical front, we propose a definition of SSLE in the uni- versal composability framework. We believe this to be the right setting for highly concurrent contexts such as those of many blockchain-related applications. Next, we propose a UC-realization of SSLE from public key encryption with keyword search (PEKS) and based on the ability of dis- tributing the PEKS key generation and encryption algorithms. Finally, we present an efficient MPC-friendly PEKS that allows us to efficiently instantiate the abstract scheme. Our concrete construction compares favorably with previous work (both in terms of computational costs and in terms of overall communication overhead) while guaranteeing much stronger composability guarantees.


Time and place:
11:00am Online via Zoom: Zoom3 - https://zoom.us/j/3911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Invierno 2021