A knowledge base is a database together with an ontology, which contains rules that can be used to infer new facts not explicitly present in the data. In the general case, this fact-generating procedure can run forever, creating infinitely many versions of the original database of possibly infinite size. When answering queries, all these possible worlds must be considered when computing the result. This version of query answering is called “query entailment”. More formally, we say that a query is entailed by a database if it is true in all of its extensions.

To bring query entailment closer to database theory-style query answering, where the data is always finite, a finite version of query entailment has been considered for many classes of queries and rule languages. In the context of “finite query entailment”, a query is said to be entailed by a database if it is true in all of its finite extensions. Unfortunately, this finite semantics can lead to a loss of intended meaning, creating nonsensical databases that do not correspond to the user's intuition.

In this talk, I will introduce a new partially finite semantics, and its corresponding “partially finite query entailment” problem, that aims to reduce the disparity described above by allowing users to choose which part of the data must remain finite. I will show how the problem differs from its unrestricted and finite variants, and that it does not cause an increase in computational complexity, for the logic S.

The talk will contain an introduction to the query entailment formalism and should be accessible to those without a background in Description Logics/Knowledge representation.

In this talk, we tackle the reachability analysis problem of binary code that manipulate the part of memory that is just above the stack pointer. To model such programs, we use Upper Stack PushDown Systems (UPDS), an extension of Pushdown systems (PDS), to simulate the stack operations of assembly codes. UPDS is a kind of PDS with two stacks called upper stack and lower stack where the lower stack works as a normal PDS stack and the upper stack works as the memory space above the stack. We propose several algorithms to perform the reachability analysis of this model. To this aim, we represent regular potentially infinite sets of configurations using finite state automata. The reachability sets of UPDSs being in general not regular, we propose two semi-algorithms for computing accurately the sets of predecessors pre* and successors post* of regular sets of configurations of UPDS. We provide interesting subclasses for which our semi-algorithms are guaranteed to terminate. We show that our approach has several interesting applications like stack overflow detection, stack string detection, return address anomaly detection, etc.

This is a joint work with Tayssir Touili.

Almost-complex geometry is the study of spaces that lie between the complex and real ones. In the smooth category, it becomes a refinement of real differential geometry and an extension of complex differential geometry. Although there are numerous results in the field, almost-complex geometry does not yet have a clear theory unlike its real and complex counterparts. I will discuss an almost-complex specialization/extension program that we will implement with a proof assistant through an example, namely the Taylor series of a metric in normal coordinates. The Taylor coefficients are related to the curvature of the metric, which illustrates the general phenomenon of curvature obstructing the integrability of a geometric structure.

The edge list model is arguably the simplest input model for graphs, where the graph is specified by an unordered list of its edges. In this model, we study the quantum query complexity of k-cycle finding, and its connections with k-distinctness. Specifically, given any graph with low maximum degree, such as a typical random sparse graph, we prove that the quantum query complexity of finding a length-k cycle in its length-m edge list is m^{3/4-1/(2^{k+2}-4) ± o(1)}, which matches the best-known upper bound for the quantum query complexity of k-distinctness on length-m inputs up to an m^{o(1)} factor. We prove the lower bound by developing new techniques within Zhandry's recording query framework (cryptology eprint: 2018/276) as generalized by Hamoudi and Magniez (arxiv: 2002.08944). These techniques extend the framework to treat any non-product distribution that results from conditioning a product distribution on the absence of rare events. We prove the upper bound by adapting Belovs's learning graph algorithm for k-distinctness (arxiv: 1205.1534). Finally, assuming a plausible conjecture concerning only cycle finding, we show that the lower bound can be lifted to an essentially tight lower bound on the quantum query complexity of k-distinctness, which is a long-standing open question.

Program equivalence is a central topic in the study of programming languages. Certifying that compiler transformations do not change the semantics of a program is needed to formally prove correct compilers.

This thesis aims at further developing the theory of program equivalences for the untyped pure λ-calculus, on several viewpoints.

We suggest to switch from program equivalences to program preorders, which is a usual switch in the study of programming languages but perhaps not something fully accepted at the level of the λ-calculus. We show that some central concepts in the λ-calculus may be reformulated to simple properties on preorders for λ-terms.

Contextual equivalences are the most natural notion of comparison for programs: contextual comparison is about testing programs in any execution environment and checking that they behave in a similar way. This equivalence is mostly unusable to provide proof of equivalences for expressive enough programming languages, because of the universal quantification over execution environments—akin to testing for all possible inputs.

We introduce a quantitative refinement of contextual equivalence, trying to obtain a cost-sensitive program equivalence as natural as contextual comparison. Interaction equivalence tests programs in any execution environment, checks that their behavior is similar but also takes into account the number of communications (or interactions) between the program and its environment.

Finally, we explore program equivalences for another evaluation paradigm, namely call-by-value. Call-by-value is more efficient and closer to the actual evaluation mechanism used by programming languages despite it being less studied than the original evaluation of the λ-calculus. It leads to a wide range of program equivalences, usually studied with effects added to the language. We study it here in a pure setting and show that call-by-value is a rich framework with many different notions of equivalences.

We provide a unifying view of all these program equivalences and their main properties, abstracting over the evaluation mechanisms considered.

​The economy of scale principle, where the cost per unit decreases as the scale of operation increases, is a foundational concept in economics. It naturally arises in diverse real-world systems, from logistics and infrastructure planning to data summarization and information propagation. In such systems, grouping resources, demands, or actions often leads to more efficient outcomes. This behavior is reflected in mathematical models through properties such as submodularity, which captures diminishing returns on the value side, and subadditive capacity cost functions, which formalize buy-at-bulk effects on the cost side. In submodular optimization problems, the economy of scale appears as diminishing marginal gains: each additional element contributes less marginal gain as the solution grows. This framework captures key phenomena, including information redundancy and influence propagation. In the buy-at-bulk facility location problem, the economy of scale manifests on the cost side: satisfying a larger demand becomes cheaper per unit due to amortized setup costs. By leveraging this shared structure, this thesis explores the design of approximation and streaming algorithms for these two classes of problems that capture the principle of economy of scale. We develop algorithmic techniques with provable performance guarantees for problems with complex constraints, across different computational models. These results contribute to the broader understanding of scalable algorithms for decision making tasks where gains or costs exhibit diminishing return structures.

We consider the LTL model-checking problem of concurrent self modifying code, i.e., concurrent code that has the ability to modify its own instructions during execution time. This style of code is frequently utilized by malware developers to make their malicious code hard to detect. To model such programs, we consider Self-Modifying Dynamic Pushdown Networks (SM-DPN). A SM-DPN is a network of Self-Modifying Pushdown processes, where each process has the ability to modify its current set of rules and to spawn new processes during execution time. We consider model checking SM-DPNs against single indexed LTL formulas, i.e., conjunctions of separate LTL formulas on each single process. This problem is non trivial since the number of spawned processes in a given run can be infinite. Our approach is based on computing finite automata representing the set of configurations from which the SM-DPN has a run that satisfies the single-indexed LTL formula. We implemented our techniques in a tool and obtained promising results. In particular, our tool was able to detect concurrent, self-modifying malware.

This is a joint work with Tayssir Touili.