ABSTRACT. Gödel’s first incompleteness theorem states that in every consistent system of axioms which contains a modicum of arithmetic and its theorems can be listed by an algorithm, there exist true statements about natural numbers that are unprovable in the system. The second incompleteness theorem states that such a system cannot demonstrate its own consistency. J. von Neumann called them “a landmark which will remain visible far in space and time.”

The talk will briefly show that both incompleteness results follow from the undecidability of the Halting problem. Then we will discuss theoretically whether the incompleteness results give a “coup de grâce” to Hilbert’s Programme. Finally, we will argue that the current practice of mathematics, which uses extensively proof-assistants, is changing the theoretical views about the impact of incompleteness.

ABSTRACT. The talk is based on a joint work with Igor Potapov and Pavel Semukhin (Liverpool, UK). It appeared as a conference abstract at ISSAC 2020. Our results relate numerical problems on matrices over the rationals to symbolic algorithms on words and finite automata. Using exact algebraic algorithms and symbolic computation, we prove new decidability results for 2 × 2 matrices over ℚ. Namely, we introduce a notion of flat rational sets: if M is a monoid and N ≤ M is its submonoid, then flat rational sets of M relative to N are finite unions of the form L0g1L1…gtLt where all Lis are rational subsets of N and gi ∈ M. We give quite general sufficient conditions under which flat rational sets form an effective relative Boolean algebra. As a corollary, we obtain that the emptiness problem for Boolean combinations of flat rational subsets of GL(2;ℚ) over GL(2;ℤ) is decidable. On the other hand, there is some evidence supporting our conjecture that the membership problem for rational subsets of GL(2;ℚ) is undecidable.

ABSTRACT. We consider a simplified 1d problem coupling the diffusion neutronics equations with an equation on the enthalpy of a fluid inside the nuclear core, where the coefficients of the neutronics equation depend on the enthalpy. Our aim is to find the generalized eigenvalue of the coupled problem and the associated unique solution.

Using different methods of interpolating the coefficients, we describe a complete picture of all the cases appearing when the coefficients are known at three values through the elliptic Jacobi equation and perform comparisons between the different approximation methods. It is a follow-up and generalisation of works done in the past 6 years, in particular SYNACS2016 proceedings.

ABSTRACT. This paper is a followup of the paper of Dellacherie et al. in (DOI: 10.1109/SYNASC40771.2016), where we were able to obtain an analytic solution of a monodimensional stationary system coupling two simplified models, one solving the thermohydraulic equations, the other one solving the neutronic diffusion equation with one energy group. An approximation of the analytic solution using incomplete Jacobi elliptic integrals was derived as well as the calculation of the neutron multiplication factor $k_{eff}$, and we use this explicit approximation in a more general case with uncertainties on the data, which are the values of some physical functions (of the temperature $T$) of the fluid characterizing the problem (namely the diffusion coefficient $D$, the absorption cross-section $\Sigma_a$ and the fission cross section $\nu \Sigma_f$). A thorough numerical study has been done. Using it, we demonstrate that the physical hypotheses on these function must hold for any Monte-Carlo sampling of the values, for example the values of the fission cross section must be increasing if the temperature $T$ increases.

ABSTRACT. In this article, we propose new methods to compute multiple roots of polynomials in floating-point arithmetic. We rely on stochastic arithmetic that makes it possible to deal with rounding errors. We develop the concept of stochastic GCD that we use to deflate a polynomial in order to obtain a polynomial with single roots. We can then apply Newton method to get fast and accurate approximations of the roots. Numerical experiments show the effectiveness and efficiency of our methods.

ABSTRACT. A fundamental problem in algebraic geometry is to decompose the solution set of a polynomial system. A numerical description of this solution set is called a numerical irreducible decomposition. Standard algorithms use a sequence of homotopies in a dimension-by-dimension approach. We provide a new approach by pairing a classical result that computes a smooth point on every irreducible component in every dimension using a single homotopy together with the theory of isosingular sets.

ABSTRACT. We present preliminary results towards applications of interactive theorem proving to the field of proof mining. Our contribution is twofold. First, we describe an implementation in the Lean proof assistant of the proof-theoretical tools used in the field, which can provide a foundation for a system of program extraction based on general logical metatheorems. Second, we discuss a Lean formalization of quantitative results from convex optimization obtained as part of the program of proof mining.

ABSTRACT. Secure Multiparty Computation proves to work in every ring, not necessarily associative, commutative or with 1. The possibility to apply it in domains of characteristic 0 is discussed. For commutative fields, including those of characteristicn 0, a scheme with division is proposed. Finally, the Berlekamp-Welch algorithm and the Secure Multiparty Computation with malicious partners prove to work in every field as well, including the non-commutative fields.

ABSTRACT. IoT industry have grown in the last couple of years to the point where many people are now using one or two IoT devices. Analysts like Gartner and Forrester predicted this growth and raised several security concerns (most of them being related to privacy and access to personal data). In particular for consumer users, this may also represent other security ricks such as data exfiltration. This presentation focuses on presenting the risks that come with IoT devices (in terms of privacy and access). As a practical aspect, some newly discovered IoT vulnerabilities ( in IoT devices like web-cameras or baby-monitors) with details on how these vulnerabilities were discovered and how they work will be presented.

ABSTRACT. Automated reasoning, and in particular first-order theorem proving, is one of the earliest research areas within artificial intelligence. It is undergoing a rapid development thanks to its successful use in program analysis and verification, security analysis, symbolic computation, theorem proving in mathematics, and other related areas. Breakthrough results in all areas of theorem proving have been obtained, including improvements in theory, implementation, and the development of powerful theorem proving tools. However, recent developments are not always easily accessible to non-specialists. This short tutorial aims to address this by introducing the audience to first-order theorem proving. The workhorse used for a demonstration of concepts discussed at the tutorial will be our award-winning theorem prover Vampire.

The tutorial will be split in two parts. The first part immediately helps the audience place the work in context by introducing them to an application of theorem proving in Vampire for validating mathematical theorems. The second part introduces the core concepts of automating first-order theorem proving

ABSTRACT. This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs delete or create interactions or components while the system components change state according to their local behaviour. Our proof calculus uses a configuration logic that supports local reasoning and that relies on inductive predicates to describe distributed systems with an unbounded number of components. The validity of reconfiguration programs relies on havoc invariants, assertions about the ongoing interactions in the system. We present a proof system for such invariants in an assume/rely-guarantee style. We illustrate the feasibility of our approach by proving the correctness of self-adjustable tree architectures and provide tight complexity bounds for entailment checking in the configuration logic. Joint work with Emma Ahrens and Joost-Pieter Katoen (RWTH Aachen) and Marius Bozga (VERIMAG).

ABSTRACT. The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean.

ABSTRACT. Alk is an educational programming language in-tended to represent algorithms as simple as possible. The paperis targeting the problem of translating Alk array expressionsinside path conditions, generated by symbolic execution, intothe Z3 engine. Considering the issues caused by the complexityof Alk arrays, through their built-in methods, special operatorsand representation, an extended Z3 array model is designed.This model is meant to define several functions and assertionsto ultimately allow a transparent translation of path conditionscontaining compound data type operations. The solution providedis implemented in the official Alk interpreter and displays correctand efficient translations.

ABSTRACT. Structure editors provide many potential usability benefits to an end-user by allowing them to edit the AST representation of a program rather than a textual representation of it. In addition, they all but remove syntax errors by only allowing the constructing of programs that are syntactically valid. However, structure editors only rarely include undo/redo functionality into the editor itself, and to the best of our knowledge, an underlying, formal specification for undo/redo has yet to be developed. This paper continues previous work on an editor calculus; we extend the calculus with undo and redo and present a history-based operational semantics of the extension. The history used an underlying graph-based structure, containing a history of user actions in the particular structure editor. We study the expressive power of the calculus, give a simple proof of its Turing-power and use the expressiveness result to show how our history-based extension with undo and redo can be expressed in the original editor calculus.

ABSTRACT. We present a unification problem based on first-order syntactic unification which ask whether every problem in a schematically-defined sequence of unification problems is unifiable, so called loop unification. Alternatively, our problem may be formulated as a recursive procedure calling first-order syntactic unification on certain bindings occurring in the solved form resulting from unification. Loop unification is closely related to Narrowing as the schematic constructions can be seen as a rewrite rule applied during unification, and primal grammars, as we deal with recursive term constructions. However, loop unification relaxes the restrictions put on variables as fresh as well as used extra variables may be introduced by rewriting. In this work we consider an important special case, so called semiloop unification. We provide a sufficient condition for unifiability of the entire sequence based on the structure of a sufficiently long initial segment. It remains an open question whether this condition is also necessary for semiloop unification and how it may be extended to loop unification.

ABSTRACT. There have been many task designs for modelling real-time embedded systems in order to capture real-world problems. The traditional approach is when each task has a hard deadline, so all tasks are equally treated when considering the scheduling problem. A recent design is for a task set to have (m, k)-firm deadlines, namely at least m out of any k consecutive tasks must meet their deadlines. Another related model may be defined when a task is allowed to execute in multiple feasible intervals, for which a miss happens when the task does not execute in any of the feasible intervals. Other existing models are represented by soft real-time (SRT) systems, but do not require any deadline to be met. Instead SRT systems require bounded tardiness, where jobs are allowed to miss deadlines as long as the extent of miss is bounded. This paper describes a new task model, similar yet different from all previous existing models, for scheduling single-instance non-preemptive tasks on a multiprocessor platform by considering both a soft and a hard deadline for each task in a given task set. Our motivation is that tasks that finish before their soft deadlines achieve their best performance. Finishing before the hard deadline implies an acceptable and a safe performance, while missing a hard deadline leads to harmful situations. In addition, our paper defines a measure for the feasibility of a task set, where meeting a soft deadline counts twice as much as meeting just a hard deadline of that task. This paper also describes a scheduling algorithm for soft-hard single-instance non-preemptive tasks together with some examples reaching a feasible schedule.

ABSTRACT. A recently proposed methodology for authorship attribution is adapted in the current work for sentiment analysis. Furthermore, it is applied here for a non-English language, i.e. for Romanian. The procedure works at the character level, hence it does not depend on the language, although it is designed only for the languages that use the Latin alphabet. The data set used is taken from financial market news and it contains paragraphs that refer to two particular companies. In order to establish the ground truth for the sentiment scores, the text is translated into English and Vader is further used. The aim of the methodology is to build a regression model that fits the initial paragraphs with text in Romanian to the scores established by Vader and the results are encouraging.

ABSTRACT. The problem of the fake news on the Internet is not new. However, in the case of a global pandemic, this kind of misinformation can be dangerous, confusing, and costly in terms of loss of human lives. The ongoing COVID-19 pandemic has unfortunately shown significant and remarkable spread of fake news, concerning the disease itself, vaccination, number of deaths and so on. It is necessary to develop an effective algorithm that will be able to detect COVID-19 misinformation and help scientists to easily separate fake from the true news. The research presented in this paper proposes an arithmetic optimization algorithm (AOA) - based approach that can improve the classification results by reducing the amount of features and achieve high accuracy. The AOA has been utilized as a wrapper feature selection. The obtained simulation results were subject to a comparative analysis with both world-class classifiers and other nature inspired evolutionary approaches. The results of the simulation indicate better performance of the proposed approach with AOA over other algorithms and that it obtains superior accuracy. Proposed approach with AOA outperforms other algorithms and obtains superior accuracy.

ABSTRACT. From the moment of being excavated till they become a museum exhibit, archaeological artefacts undergo a careful process of restoration, elaborately conducted by human experts with the help of complex devices. After the chemical composition of the object is approximated, the next step of the pathway is to assess the degradation of the surface, i.e. the quantification of corrosion. While earlier work proposed an automation of the step related to the estimation of the chemical concentration, the current study attempts to further offer a computational solution for the detection of corroded areas of the artefact. Iron historical items were considered, stereo microscopy images were produced and the restorers manually roughly delineated the regions containing rust. An U-Net architecture was trained on the annotated collection to recognize rust from clean areas. Even with a preliminary minimal manual delineation of the degraded zones for training, the deep learning model was able to recognize the similar areas in new objects in the test phase.

ABSTRACT. Due to the high interest in the past few years, blockchain technology benefited from a fast increase in adoption rate as well as fast evolution. One of the crucial points in the blockchain space, the consensus mechanism, generally still suffers from lack of development, thus decreasing the adoption of the technology in big scale projects and daily use. Older-established consensus algorithms, such as Proof of Work (PoW) and Proof of Stake (PoS), suffer from various flaws, ranging from the high costs of maintaining a node in the network and generating new blocks, to the risk of being affected by a series of attacks, as well potential of network monopoly by various entities. This paper proposes a model of a democratically-governed consensus algorithm that is focused on a fair distribution of assets, with a fast and secure way of validating and distributing the blocks, while being impervious to a sizeable range of attacks.