LOS Seminar

Andra Băltoiu (LOS)
Dictionary Learning Heuristics Control Through Adaptive Strategies and Applications to Anomaly Detection

Abstract: Dictionary learning has two model-dependent heuristics: sparsity level and dictionary size. Both are highly dependent on the signals and there are few applications in which an informed, accurate choice is possible. Particular problems, such as classification, entail further parameters that interfere with learning. We present several adaptive strategies that are aimed at finding the optimal values for these heuristics or at avoiding the choice altogether. We also discuss the implications on anomaly detection, which we treat as a special case of classification.

Paul Irofti (LOS)
Anomaly Detection ABC

Abstract: We briefly revisit and discuss the standard methods for anomaly detection, such as One Class SVM, SVDD, Isolation Forrest, and Gaussian Mixtures. For each method we analyze the optimization problem, its anomaly detection applications, and the improvements gained by introducing non-linear transformations to the inputs via kernel methods (connecting the anomaly detection field to Hilbert spaces). The papers of interest can be found in the ABC directory here.

Andrei Pătraşcu (LOS)
Inexact Proximal Point Algorithm for Convex Optimization under Holderian Growth

Abstract: Proximal Point Algorithm (PPA) gained a long-lasting attraction for both abstract operator theory and numerical optimization communities. Even in modern applications, researchers still use proximal minimization theory to design scalable algorithms that overcome nonsmoothness. Remarkable works established tight relations between the convergence behaviour of PPA and the regularity of the objective function. In this talk we present nonasymptotic iteration complexity of exact and inexact PPA to minimize convex functions under Holderian growth. In particular, we recover well-known results on PPA: finite convergence for sharp minima and linear convergence for quadratic growth, even under presence of inexactness. However, without taking into account the concrete computational effort paid for computing each PPA iteration, any iteration complexity remains abstract and purely informative. Therefore, based on an inner (proximal) gradient/subgradient method subroutine that computes inexact PPA iteration, we secondly present computational complexity bounds of a restarted inexact PPA, that are available when no information on the growth of the objective function is known.

Ruxandra Bălucea (LOS)
Low-level Attacks and Software Mitigations on RISC-V

Abstract: RISC-V is a modern open-source architecture developed in 2013 at the University of Berkeley. It maintains the old features of the classic RISC (Reduced Instruction Set Computer) architectures, but tries to remove the vulnerabilities discovered in the past years. In this context, the main goal of RISC-V is to evolve without compromise, improving the performance of the chips only if this is done completely safely. In this context, we introduce some of the most popular attacks like Buffer Overflow, ROP and we present some variants of Spectre, a famous family of attacks reproduced on a speculative RISC-V core named BOOM. We also present a software mitigation for one of these variants and other future directions.

Horațiu Cheval (LOS)
Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration

Abstract: We compute quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration in W-hyperbolic spaces. This iteration is an extension to a nonlinear setting of the modified Mann iteration defined recently by Bot, Csetnek and Meier in Hilbert spaces. We obtain these quantitative results by applying methods from proof mining.
This is joint work with Laurențiu Leuștean.

Mihai Adamescu (University of Bucharest)
Interdisciplinarity and transdisciplinary

Abstract: Ecology, sustainability science, drones, sensors, HPC, HCI, ioT, complexity science, digital humanities, mathematics, and sociology. What do all of them have in common? How can we answer even more complex questions that society has? How can we address some of these questions? Why is our thinking so fragmented? How can we find common ground?
A short presentation of the Research Center in Systems Ecology and Sustainability, the Research Infrastructures (eLTER, LifeWatch, ICOS, BIOSCAN) that we are promoting, and the need to cooperate, including possible cooperation themes.

Alin Ştefănescu (University of Bucharest)
River: fuzz testing using AI for binaries and IoT

Abstract: We present RIVER, a tool using AI and formal methods for software testing. We start with the first version of the tool that implemented reversible instructions for concolic execution of binary files. Then we show the evolution of the RIVER framework that included fuzzing and AI. Finally, we discuss the current adaptation to Internet of Things domain and future plans.
(This is joint work with Ciprian Paduraru and other colleagues that contributed to the development of the framework.)

Grigore Roşu (University of Illinois at Urbana Champaign and Runtime Verificarion)
Matching Logic: The Foundation of the K Framework

Abstract: The K framework is an effort in realizing the ideal language framework, where programming languages must have formal semantics and all language tools are automatically generated from the formal semantics. Until recently, K has been developed as an engineering endeavor driven by challenges such as formalizing the complete semantics of large languages (C, Java, JavaScript, Python, etc), but deriving its semantics from translations to various formalisms, such as rewriting logic, graph transformations, or Coq. This semantics borrowing approach came not only at a notational cost, where the original language meaning was ``lost in translation'', but also at a foundational cost: the target formalisms were more complicated than necessary, yet more restricted due to their prescribed ways to define language semantics.
In this talk I will present matching logic as the new and direct foundation of K. I will also discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, reachability logic and thus Hoare logics, and separation-logic-style recursive predicates and patterns. Matching logic can therefore be regarded as an expressive foundation for programming languages, and K as a best effort implementation. An appealing aspect of matching logic's Hilbert-style proof system is that it admits a small proof checker, in the order of 200 LOC including parsing.

Claudia Chiriță (LOS)
The mysterious case of a waning algebraic specification

Abstract: Join me in a brief foray into algebraic specification. We'll first look at the recent and not so recent history of a field that has had a tremendous impact on several areas in mathematical logic and formal software development. Although it is no longer as actively studied as it used to be, algebraic specification continues to foster new ideas in fields such as artificial intelligence and formal methods. I will share with you the reason why I am doing research in this field, how my work fits into the landscape of formal specification and verification, and some ongoing and future research efforts.

Mihai Adamescu (University of Bucharest)
Interdisciplinarity and transdisciplinary II

Abstract: Ecology, sustainability science, drones, sensors, HPC, HCI, ioT, complexity science, digital humanities, mathematics, and sociology. What do all of them have in common? How can we answer even more complex questions that society has? How can we address some of these questions? Why is our thinking so fragmented? How can we find common ground?
A short presentation of the Research Center in Systems Ecology and Sustainability, the Research Infrastructures (eLTER, LifeWatch, ICOS, BIOSCAN) that we are promoting, and the need to cooperate, including possible cooperation themes.

Paul Irofti (LOS)
Analysis of executables: Designing an emulator a decade ago

Abstract: In my past life I’ve been researching the field of dynamic analysis in regards to emulating obfuscated and/or malevolent binaries. The result was an emulator that translates code blocks of binary samples from different platforms (operating systems and machine types) into an intermediate representation where information retrieval, data analysis and behaviour observations are made.
This work was also presented at two Dagsthul Seminars:
(12051) Analysis of Executables: Benefits and Challenges, 2012
(14241) Challenges in Analysing Executables: Scalability, Self-Modifying Code and Synergy, 2014

The talk takes place at the Runtime Verification (RV) Bucharest headquarters (Popa Tatu 18).

Traian Şerbănuţă (LOS and Runtime Verification)
Specifying and verifying concurrent programs using the K framework - current status and open problems

Abstract: The first part of this presentation will show (through toy examples) that K seems like an ideal framework to describe concurrency and memory models. The second part will present the current status of verifying concurrent programs in K, identify limitations, and discuss possible ways of addressing them

This a special seminar dedicated to presentations of students' research projects.

George Bodea (University of Bucharest)
Secret sharing schemes - map of properties

George Blănar (University of Bucharest)
Robust Deep Autoencoders in anomaly detection

Theodor Moroianu (University of Bucharest)
L0-SVDD and R-SVDD analysis and Lagrange multipliers

Felix Puşcaşu (University of Bucharest)
Analysis of GMM and Deep-GMM anomaly detection methods

Constantin Drăgancea (University of Bucharest)
SVDD and Deep-SVDD analysis

Radu Ştefan (University of Bucharest)
Danger of spectre attacks

Ion Tifui (University of Bucharest)
Analysis of attacks of type Meltdown and Spectre

Andrei Arusoaie (Alexandru Ioan Cuza University of Iaşi)
Certifying Findel derivatives for blockchain

Abstract: Findel is a composable DSL for financial derivatives that can be executed on the blockchain. The language is simple and expressive enough to express complex derivatives. However, compared to its competitors, Findel does not guarantee that contracts progress properly. There is no default refund mechanism, and the economic enforcement is not handled by the language itself. Given the immutability of the blockchain, more caution should be taken in order to avoid undesired situations. In this presentation, we address the formal verification of financial derivatives written in Findel. We define a formal semantics of Findel in Coq and we test it against the existing Findel test suite. We enrich our semantics with means to interactively formalise and prove properties about Findel contracts. The goal is to avoid mistakes in Findel contracts that may have a negative impact (e.g., stuck contract executions, money losses). The derived infrastructure is used to certify non-trivial contract examples that cover the most common types of derivatives (forwards/futures, swaps, options).

References:
[1] A. Arusoaie, Certifying Findel derivatives for blockchain, Journal of Logical and Algebraic Methods in Programming 121, 100665 (2021)

Adriana Nicolae (Babeş-Bolyai University)
Alternating projections and convexity-like properties

Abstract: In this talk we discuss some local geometric features which, imposed on two closed sets, allow us to prove even in nonlinear settings the local linear convergence of the method of alternating projections for finding a point in the intersection of the two sets.

Florin Stoican (Polytechnic University of Bucharest and LOS)
A mixed-integer MPC with polyhedral potential field cost for collision avoidance

Abstract: This work pertains to the use of polyhedral potential fields which take into account the obstacles' shape through their associated sum function. As contributions, we extend the polyhedral sum function notion to the multi-obstacle case and show that the polyhedral support of its piecewise affine representation comes from an associated hyperplane arrangement. We exploit the obtained combinatorial structure to provide equivalent mixed-integer representations and model a repulsive potential term for subsequent use in a Model Predictive Control (MPC) formulation. The advantages are related to a decrease in the computational complexity and a coherent description of the repulsive potential, regardless of the cluttered environment's complexity.

Elena Burceanu (Bitdefender)
Self-Supervised Learning in Multi-Task Graphs through Iterative Consensus Shift

Abstract: The human ability to synchronize the feedback from all their senses inspired recent works in multi-task and multi-modal learning. While these works rely on expensive supervision, our multi-task graph requires only pseudo-labels from expert models. Every graph node represents a task, and each edge learns between tasks transformations. Once initialized, the graph learns self-supervised, based on a novel consensus shift algorithm that intelligently exploits the agreement between graph pathways to generate new pseudo-labels for the next learning cycle. We demonstrate significant improvement from one unsupervised learning iteration to the next, outperforming related recent methods in extensive multi-task learning experiments on two challenging datasets.
References:
[1] E. Haller, E. Burceanu, M. Leordeanu, Self-Supervised Learning in Multi-Task Graphs through Iterative Consensus Shift. The 32nd British Machine Vision Conference (BMVC), 12 pages (2021)

The talk is organized jointly with Runtime Verification (RV) and takes place at the RV Bucharest headquarters (Popa Tatu 18).

Ana Pantilie (Runtime Verification)
A general overview of the K Framework's symbolic execution engine

Abstract: One of the main tools offered by the K Framework is its symbolic execution engine, which allows one to automatically prove program specifications. This presentation will go over the internal language of the prover and how it relates to matching logic, how the prover interprets this language and attempts to satisfy reachability claims. The goal of this presentation is to bridge the gap between K definitions and specifications and what happens behind the scenes when one executes the K prover.

Daniel Peptenatu, Aurel Băloi, Ion Andronache (University of Bucharest)
A presentation of the Research Center for Integrated Analysis and Territorial Management (CAIMT)

• Attracting funds to support advanced research programs in integrated analysis and land management.
• Dissemination of scientific results at the level of the international flow of publications.
• Imposing a scientific standard in advanced research and land management, in line with established international standards.
• Development and promotion of integrated land analysis methodologies.
• Development of national and international partnerships.

• Daniel Peptenatu - A perspective on research management
• Aurel Băloi - The power of location. Ups and downs in our society
• Ion Andronache - Fractal analysis. An interdisciplinary perspective

George Jiroveanu (Siemens Advanta Brașov)
From local to global consistency in distributed monitoring of Petri Net models

Abstract: In this technical note we consider a distributed analysis of a plant given by local Petri Net models (components) that interact via shared transitions. For each component, there is a local agent that performs local calculations and exchanges information with its neighbours for monitoring the plant. We relax the standard requirement that the interaction graph between components is a tree and, for the general case, we investigate under which conditions the local consistency of the local estimates implies their global consistency. Moreover, we show that if the information exchanged between agents incorporates additional information related to the execution time intervals of the shared transitions, the globally consistent estimates become equal to the results derived in a centralized setting.
References:
[1] G. Jiroveanu, R. K. Boel, From local to global consistency in distributed monitoring of Petri Net models. IEEE Transactions on Automatic Control (2022). DOI: 10.1109/TAC.2022.3141708

Huu Thinh Do (LCIS, Grenoble INP)
Benefits of differential flatness for optimal profile generation and trackings

Abstract: Motion planning problems benefit greatly from the properties of differential flatness, which are widely employed for trajectory generation and controller design. This work aims to highlight the fact that various flat representations of a system can have different implications in the trajectory generation and tracking objectives. In particular, we consider a fixed-wing UAV (Unmanned Aerial Vehicle) and analyze various flat representations. We reformulate the trajectory generation and tracking problem in terms of different flat outputs and analyze the optimal cost, constraints satisfaction, tracking error and computational complexity. Insights on the future work complete the analysis. The research shows promising directions, especially in the area of disturbance rejection and robust control.

and

Vincent Marguet (LCIS, Grenoble INP)
Reliable motion planning and coordination for a team of aerial drones

Abstract: This thesis aims to provide a reliable framework in which information from a cluttered environment is gathered through a mesh of fixed ground sensors and a mobile team of Unmanned Aerial Vehicles (UAVs). Communication and power-limited sensors gather and store information about the environment. A motion planning mechanism provides trajectories which ensure data-collection from sensors, avoids forbidden regions while minimizing time and energy costs. Precision agriculture applications are used as benchmarks (e.g., disease assessment, crop yield, terrain features/topography). After a literature review about different applications using trajectory planning, communication handling, constraints handling and task assignment, this talk will address some preliminary work on the use of Bezier and Bspline curves for multiple trajectory generation while keeping a certain formation for the drones. Simulations and some first experimental results using nano-drones pave the way for future work.

Vicenç Puig (Universitat Politècnica de Catalunya)
Optimization, Safety and Security in Critical Infrastructures

Abstract: This talk will present different how optimization, safety and security of critical infrastructures could be addressed. In particular, the use of optimization will be illustrated in the context of economic optimal control of such infrastructures considering user demands and operational costs. Safety aspects will be shown introducing the need of fault diagnosis and fault-tolerant control. Techniques to deal with both problems will be illustrated with some practical applications in the context of water networks. Finally, the problem of security will be presented in the context of cyberphysical attacks affect a critical infrastructure. In this case, the need of combined approaches that are able to deal with both the physical and cyber security will be described.

Miruna Roșca (Bitdefender)
Byzantine agreement

Abstract: This is an introductory talk to byzantine agreement. I will first define it and then motivate our interest in it. In the end, I will discuss the main key points of Algorand [1], a real life practical application using byzantine agreement.
References:
Jing Chen and Silvio Micali, Algorand , arXiv:1607.01341 [cs.CR], 2017.

Bogdan Dumitrescu (Polytechnic University of Bucharest and LOS)
Designing Incoherent Frames

Abstract: Matrices whose columns are as far as possible one from another have applications in coding and communications, but their design is interesting as a sheer optimization problem. We will present some of the main ideas for designing incoherent frames, insisting on the algorithms that are scalable and can give good results for large frames. The focus is on an own contribution, which is an algorithm using the shifted power method as basic operation, thus containing only matrix-vector multiplications. It is the fastest algorithm and has excellent results for overcomplete frames, although no theoretical guarantees exist.
References:
B. Dumitrescu, Designing incoherent frames with only matrix-vector multiplications, IEEE Signal Process. Lett., vol. 24, no. 9, pp. 1265–1269, Sep. 2017.

Radu-Ioan Boţ (University of Vienna)
Fast Augmented Lagrangian Method in continuous and discrete time

Abstract: In this talk, we address the minimization of a continuously differentiable convex function under linear equality constraints.
First, we consider a second-order dynamical system with asymptotically vanishing damping term formulated in terms of the Augmented Lagrangian associated with the minimization problem ([1]). We show fast convergence of the primal-dual gap, the feasibility measure, and the objective function value along the generated trajectories, and also asymptotic weak convergence of the primal-dual trajectory to a primal-dual optimal solution of the underlying minimization problem.
By appropriate time discretization of the dynamical system we derive an inertial algorithm ([2]) with a general rule for the inertial parameters that covers the three classical rules by Nesterov, Chambolle-Dossal and Attouch-Cabot used in the literature in the context of fast gradient methods. We show that the algorithm exhibits in the convex regime convergence rates of order $O(1/k^2)$ for the primal-dual gap, the feasibility measure, and the objective function value. In addition, for the Chambolle-Dossal and Attouch-Cabot rules, the generated sequence of primal-dual iterates converges weakly to a primal-dual optimal solution.
For the unconstrained minimization of a convex differentiable function, we rediscover all convergence statements obtained in the literature for Nesterov’s accelerated gradient method.
References:
[1] R.I. Boţ, D.-K. Nguyen. (2021). Improved convergence rates and trajectory convergence for primal-dual dy- namical systems with vanishing damping, Journal of Differential Equations 303, 369–406.
[2] R.I. Boţ, E.R. Csetnek, D.-K. Nguyen. (2021). Fast Augmented Lagrangian Method in the convex regime with convergence guarantees for the iterates, arXiv:2111.09370.

• LOS Seminar in 2020/2021