The Eighth Congress of Romanian Mathematicians

General Information
Organizing Committee
Sections and Scientific Committees
Local Organizing Board
Registration and Fee
List of Communications
Past editions
Satellite conferences
Admin Area

List of talks

I. Algebra and Number Theory

Special session: Local rings and homological algebra. Special session dedicated to Prof. Nicolae Radu

II. Algebraic, Complex and Differential Geometry and Topology

Special session: Geometry and Topology of Differentiable Manifolds and Algebraic Varieties

III. Real and Complex Analysis, Potential Theory

IV. Ordinary and Partial Differential Equations, Variational Methods, Optimal Control

Special session: Optimization and Games Theory

V. Functional Analysis, Operator Theory and Operator Algebras, Mathematical Physics

Special session: Spectral Theory and Applications in Mathematical Physics

Special session: Dynamical Systems and Ergodic Theory

VI. Probability, Stochastic Analysis, and Mathematical Statistics

VII. Mechanics, Numerical Analysis, Mathematical Models in Sciences

Special session: Mathematical Modeling of Some Medical and Biological Processes

Special session: Mathematical Models in Astronomy

VIII. Theoretical Computer Science, Operations Research and Mathematical Programming

Special session: Logic in Computer Science

IX. History and Philosophy of Mathematics

Theoretical Computer Science, Operations Research and Mathematical Programming 

(this list is in updating process)

AMAN Bogdan
Romanian Academy, Institute of Computer Science, Romania
Title: Mobility Types for Cloud Computing (details)
We propose a mobility type system for description and verification of distributed systems in which processes are asked to move between locations where important local interactions are required. We use a simple version of distributed pi-calculus to define mobility types. The novelty of this approach is that we point out sequences of migrations as global types, and investigate scenarios in which processes are required to follow such a sequence of migrations along several locations. The typing system ensures certain properties including type soundness.
INRIA Lille-Nord Europe, France
Title: Language Independent Symbolic Execution (details)
The modern world is shifting from the traditional workmanship to a more automated work environment, where software systems are increasingly used for automating, controlling and monitoring human activities. In many cases, software systems appear in critical places which may immediately affect our lives or the environment. Therefore, the software that runs on such systems has to be safe. This requirement has led to the development of various techniques to ensure software safety. In this work, we introduce a language-independent framework for emph{symbolic execution}, which is a particular technique for testing, debugging, and verifying programs. The main feature of this framework is that it is parametric in the formal definition of a programming language. We formally define programming languages and symbolic execution, and then we prove that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. This relationship between concrete and symbolic executions allow us to perform analyses on symbolic programs, and to transfer the results of those analyses to concrete instances of the symbolic programs in question. As applications of symbolic execution we focussed on verification using both Hoare Logic and Reachability Logic. A prototype implementation of our symbolic execution framework has been developed within the K framework (version 3.4). We use this prototype for verifying some nontrivial programs belonging to different programming languages in order to emphasise its genericity.
BARONI Marian Alexandru
Dunarea de Jos University of Galati, Romania
Title: Order locatedness and strong extensionality in constructive mathematics (details)
Several conditions of order locatedness are examined within the framework of Bishop's constructive mathematics. Although order locatedness is vacuously true in classical mathematics, its significance is revealed under constructive scrutiny. For example, upper locatedness is a necessary condition for the existence of the constructive supremum. Order locatedness is also related to order convergence and to strong extensionality. Every function is classically strongly extensional but not constructively. However, it turns out that each function that maps convergent sequences to order located sequences is strongly extensional.
BARONI Mihaela Carmen
Dunarea de Jos University of Galati, Romania
Title: Phylogenetic networks: mathematical models and algorithms (details)
In the last fifteen years there has been considerable interest in using phylogenetic networks to represent non-tree-like evolution. Several mathematical models and algorithms for constructing and analysing these networks will be presented.
BAZGAN Cristina
Université Paris Dauphine, France
Title: Most vital elements of graphs (details)
We study the identification of critical entities which can be determined with respect to a measure of performance or a cost associated to the system. By critical infrastructure we mean a set of points/links whose damage causes the largest increase in the cost within the network. Modeling this network by a weighted graph, identifying a vulnerable infrastructure amounts to finding a subset of nodes/edges whose removal from the graph causes the largest inconvenience to a particular property of a graph. In the literature this problem is referred to as the k most vital nodes/edges problem and its complementary version as the min node/edge blocker problem. We present results we obtained on complexity and approximation of the k most vital nodes (edges) and min node (edge) blocker for several classical problems like assignment, minimum spanning tree, p-median, p-center, vertex cover, independent set.
Faculty of Computer Science, University "Al. I. Cuza" Iasi, Romania
Title: Proving Program Equivalence (details)
Two programs are equivalent when they have the same behaviour, Depending on what is understood by behaviour, several definitions of program equivalence exist. We introduce some possible definitions of equivalence and we show how to prove that two programs are equivalent in a language-independent matter. Our proof system for program equivalence is parameterized by the semantics of the languages in which the two programs are written.
Romanina Academy, Iasi branch, Romania
Title: Probabilistic Logic for Timed Migration (details)
When modelling distributed systems it is useful to have an explicit notion of location, local clocks, timed migration and interaction. After introducing the timed distributed pi-calculus, we introduced and studied a process algebra called TiMo having exactly these features. A probabilistic extension of TiMo assigns probabilities to the transitions that describe the behaviour of TiMo networks by solving the nondeterminism involved in the movement and in the communication of processes, as well as in the selection of active locations. The main reason for creating a probabilistic extension of TiMo is to gain the ability to verify quantitative properties of TiMo distributed systems networks, such as the probability that a certain transient or steady-state behaviour occurs. It is natural to have a probabilistic temporal logic for expressing such properties over networks of located processes. Unfortunately, quantitative logics as PCTL or aPCTL are not immediately compatible with all or most of the distinguishing features of TiMo. As a result, we define a novel logic called PLTM (Probabilistic Logic for Timed Mobility). The new probabilistic temporal logic PLTM is able to describe certain aspects that are not commonly found in other logics, such as the ability to check properties which make explicit reference to specific locations and processes, to impose temporal constraints over local clocks (finite or infinite upper bounds, for each location independently), to define complex action guards over multisets of actions and properties for transient and steady-state behaviours. Finally, we present a verification algorithm for PLTM, and determine its time complexity. Given that PLTM operates at the level of discrete-time Markov chains, it can also be applied to other process algebras which involve locations, timers, process movements and communications.
Mathematical Institute, University of Bern / Faculty of Mathematics and Computer Science, University of Bucharest, Switzerland / Romania
Title: Automata, Logic and Stone Duality (details)
The aim of this talk is to explain the role of Stone duality for defining a dictionary capable of translating finite automata (considered as set-theoretical objects) into the language of classical propositional logic. According to this translation, finite automata correspond to objects in classical propositional logic, called classical fortresses, which have the same power as finite automata: they accept regular languages. Furthermore, classical fortresses allow easy generalizations of finite automata in the context of non-classical logics. We explain our method for Godel logic.
DIMA Catalin
LACL, Université Paris-Est, France
Title: The automata-logic duality for temporal epistemic frameworks (details)
We present a number of recent results on expressiveness and decidability of temporal epistemic logics in which automata theory plays an important role.
Department of Computer Science, Brown University, USA, United States
Title: On Humans, Plants and Disease: Algorithmic Strategies for Haplotype Assembly Problems (details)
On Humans, Plants and Disease: Algorithmic Strategies for Haplotype Assembly Problem Sorin Istrail Department of Computer Science, Brown University This talk is about a set of computational problems about haplotypes reconstruction from genome sequencing data for diploid organisms, such as humans, and for ployploid organisms, such as plants. Polyploidy is a fundamental area of molecular biology with powerful methods of Nobel prize recognition: polyploidy inducement for cell reprogramming, mosaicism for aneuploid chromosome content as the constitutional make-up of the mammalian brain, and the polyploidy design for highly thoughtafter agricultural crops and animal products. On the medical side, polyploidy refers to changes in the number of whole sets of chromosomes of an organism, and aneuploidy refers to changes in number of specific choromosomes or of parts of them. We will present an algorithmic framework, HapCOMPASS for these problems that is based on graph theory. The software tools implementing our algorithms (available from the Istrail Lab) are already in use, by many users, and recongized as among the leading tools in the areas of human genome haplotype assembly, plant polyploidy haplotype assembly, and tumor haplotype assembly. We will also present a number of unresolved computational problems whose solutions would advance our understanding of human biology, plant biology and human disease. To introduce the application areas, and a hint at the type of combinatorial problems of that biological import, a short primer follows. Humans, like most species whose cells have nuclei, are diploid, meaning they have two sets of chromosomes—one set inherited from each parent. In the genome era, the genome sequencing technologies are generating big data-bases of empirical patterns of genetic variation within and across species. A SNP (single nucleotide polymorphism) is a DNA sequence variation occuring commonly (e.g. 3%) at a fixed site on the genome within a population in which a single nucleotide A, C,G or T differs between individuals of a species, or between the mother-father chromosomes of a single individual. The different nucleotide bases at the SNP site are called alleles. SNPs account for large majority of genetic variation of species. For humans, there are about 10 million SNPs, so conceptually the SNPs variation of any individual is captured by two allele vectors (each with 10 million components), one inherited from mother and one from the father. Our approach to haplotype assembly is based on graph theoretical modeling of sequencing reads linking SNPs and assembling whole haplotypes based on such basic read-SNPs linkings. Polyploid organisms have more than two sets of chromosomes. Although this phenomenon is particularly common in plants (e.g., seedless watermelon is 3x, wheat 6x, strawberries 10x), it is also present in animals (e.g. fish could have 12x and up to 400 haplotypes), and in humans (e.g., some mammalian liver cells or heart cells or bone marrow cells are polyploid). While polyploidy refers to numerical change in the whole set of chromosomes, aneuploidy refers to organisms in which a part of the set of chromosomes (e.g. a particular chromosome or a segment of a chromosome) is under- or over- represented. Polyploidy and aneuploidy phenomena are recognized as disease mechanisms. Examples for polyploidy: triploidy birth conceptions end in misscariages, although mixoploidy, when both diploid and triploid cells are present, could lead to survival; triploidy, as a result of either digyny (the extra haploid set is from the mother by failure of one meiotic division during oogenesis) or diandry (mostly caused by reduplication of paternal haploid set from a single sperm or dispermic fertilization of the egg) could have parent-of-origin (genomic imprinting) medical consequences: diandry predominate amoung preterm labor miscarrieges while digyny predominates into survival into fetal period, although with a poor grown fetus and very small palcenta). Eamples for aneuploidy: trisomy in the the Down syndrome, cells with one chromosome missing while others with an extra copy of the chormosome, cells with unpredictably many chromosomes of a given type; mosaicism (when two or more populations of cells with different genotypes derived from a single individual) aneuploidy occurs in virtually all cancer cells. Work in collaboration with Derek Aguiar (Brown University) and Wendy Wong (INOVA Translational Medicine Institute)
Universitatea "Alexanfru Ioan Cuza", Romania
Title: Proving Reachability Properties by Circular Coinduction (details)
Circular coinduction is a generic name associated to a series of algorithmic techniques to prove behavioral equivalence mechanically. In this talk we discuss how the circular induction can be used for proving reachability properties.
Holon Institute of Technology, Israel
Title: The independence polynomial of a well-covered graph at -1 (details)
If a graph G has s_{k} independent sets of size k, then I(G; x) = s_{0}+s_{1}x+...+s_{α}x^{α} is the independence polynomial of G, where α is the size of a maximum independent set (Gutman and Harary, 1983). It is known that |I(G; -1)| ≤ 2^{d(G)} ≤ 2^{c(G)}, where d(G) is the decycling number and c(G) is the cyclomatic number (Engström, 2009; Levit, Mandrescu, 2011, 2013). Recall that G is a well-covered graph if all its maximal independent sets are of the same size (Plummer, 1970). In this talk we show that I(G; -1) ∈ {-1,0,1} for every unicycle well-covered graph G ≠ C_{3}, while I(G; -1) = 0 for every connected well-covered graph G of girth ≥ 6, C_{7} ≠ G ≠ K_{2}. We demonstrate that the bounds {-2^{c(G)}, 2^{c(G)}} are sharp for I(G; -1) and discuss other possible values of I(G; -1) belonging to [-2^{d(G)}, 2^{d(G)}] (Cutler, Kahl, 2014).
Aalborg University, Denmark
Title: Stone Dualities for Markov Processes (details)
We present a series of duality results involving Markov processes (MPs) and a special class of Boolean algebras with operators corresponding to (the non-compact) Markovian logics. The first duality extends the classical Stone duality. The second duality takes into account a richer universe where between MPs we do not consider only behavioural equivalences (bisimulations) but also pseudometrics that measure their similarities. On the Boolean algebra side we will involve, correspondingly, a concept of norm. The talk summarizes a series of results obtained in collaboration with Dexter Kozen (Cornell Univ. USA), Kim G. Larsen (Aalborg Univ. Denmark) and Prakash Panangaden (McGill Univ. Canada) and presented at LICS2013 and MFPS2014.
MINEA Marius
Politehnica University of Timișoara, Romania
Title: Modeling and verification of security for web applications and services (details)
In this talk we will first present how protocols and services with security properties can be modeled by a combination of symbolic transition systems for their workflow, together with Horn clauses for policies. Then we will comparatively describe different approaches for verifying them by model checking. Finally, we will present how to automatically infer state models of web applications by crawling and use SAT checking to detect security vulnerabilities due to unintended workflows.
Turku Centre for Computer Science and Ã…bo Akademi University, Finland
Title: Modeling with Exploration Systems (details)
\documentclass{llncs} \newcommand{\cA}{\mathcal{A}} \mainmatter \title{Modeling with Exploration Systems} \author{Ion Petre %\inst{1} } \institute{Computational Biomodeling Laboratory\\ Turku Centre for Computer Science and \AA bo Akademi University\\ Turku 20520, Finland\\ \email{}} %\author{Authors here} \begin{document} \maketitle \emph{Reaction systems} were introduced in~\cite{7.4} as a new modelling framework inspired by the functioning/bio-energetics of the living cell. %It differs drastically from the traditional modelling frameworks (such as ordinary differential equations (ODEs), stochastic processes, Boolean networks, state machines) in focusing on reactions and in having the environment as an integral part of the model. %Reactions in reaction systems are enabled through facilitation and inhibition: %, see~\cite{3.1}: A reaction $r$ in reaction systems can facilitate a reaction $s$ by providing some of the reactants needed by $s$, or $r$ can inhibit $s$ by producing an inhibitor of $s$. The formal notion of a reaction system is an abstract set-theoretical notion $\cA=(S,A)$; it allows any set $S$ as the background set, and the set of reactions $A$ specifies state transitions in the state space of $\cA$, i.e., the set of all subsets of $S$. %Reaction systems are based on two main principles. The first one, called the \emph{threshold principle} makes reaction systems a qualitative framework by stating that if available, a resource (reactant) is available abundantly. In other words, reactions cannot limit each other through a quantitative competition on resources. The second principle, called the \emph{non-permanency principle}, states that a resource or reactant vanishes unless sustained by a reaction. That is to say, the next state of a reaction system is only obtained from the output of the reaction enabled in the previous state plus the contribution of the environment. Reaction systems capture two important features of biology: the \emph{non-perma\-nency} of its entities, and the \emph{open system} aspect of the living cells. \emph{Zoom structures} were introduced in~\cite{p7} to capture another important feature of biological systems: their \emph{hierarchical organization}. The notion of zoom structures is based on well-founded partial orders; a zoom (formally a walk against/along the edges of the partial order) allows the investigation of a system in increasing/decreasing level of detail, thus integrating multi-level knowledge about the system. Zoom structures and reaction systems together form the framework of \emph{exploration systems} for modeling biological (and other types of) systems. Zoom structures represent the \emph{static}, multi-level knowledge about the system and reaction systems capture the \emph{dynamic} processes in the system as state transitions between zooms. We give a brief introduction to reaction systems, zoom structures and exploration systems. We illustrate these notions with examples from biology (heat shock response and intermediate filament assembly) and from particle physics. The talk is based on recent results from~\cite{azimi2014reaction}, \cite{if-rs}, and \cite{p5}. \footnotesize \bibliographystyle{plain} \bibliography{referrences} \end{document}
PETRE Luigia
Ã…bo Akademi University, Finland
Title: A Theory of Service Composition (details)
Service composition has become commonplace nowadays, in large part due to the increased complexity of software and supporting networks. Composition can be of many types, for instance sequential, prioritizing, non-deterministic. However, a fundamental feature of the services to be composed consists in their dependencies with respect to each other. Dependency can also be of several types, for instance we can think of type and format dependencies between data producers and data consumers or of signature and semantic dependencies between service providers and service users. In this paper we propose a theory of service dependency, modelled around a dependency operator in the Action Systems formalism. We analyze its properties, composition behaviour, and refinement conditions with accompanying illustrative examples. We also set the stage for proposing a dependency theory in the related theory plugin of the Rodin Platform.
Middlesex University, London, United Kingdom
Title: A Conference Management System with Verified Document Confidentiality (details)
Conference management systems in current use occasionally exhibit embarrassing integrity and confidentiality flaws: authors learning about confidential comments by the PC members, authors receiving bogus acceptance notifications, etc. In general, a multi-user web-based system (such as a conference system) is a complex input-output automaton where even stating, let alone verifying, the correct behavior w.r.t. information flow is a daunting task. I describe our experience with implementing, fully verifying, and using CoCon, a conference system that comes with confidentiality guarantees. The formal specification and verification have been performed using the proof assistant Isabelle.
POLITEHNICA University of Bucharest, Romania
Title: Semantic variants of (truely) perfect recall in Alternating-Time Temporal Logic (details)
Alternating-Time Temporal Logic extends traditional temporal logics for program verification with means for expressing abilities of agents. Different assumptions regarding their (perfect/imperfect) recall and information render different semantics for ATL. However, when perfect recall is assumed, agents may still forget past observations when nested coalitional operators are used. We briefly introduce ATL with perfect recall, illustrate the no-forgetting phenomenon and put forward a semantics of truely perfect recall.
IMAR, Romania
Title: Recurrent many-dimensional sequences over finite alphabets (details)
Recurrent many-dimensional sequences over finite alphabets are considered. Aspects of symmetry, automaticity, generability by context-free substitutions and power of expressions are discussed. Many aspects maybe also of interest for the section "Algebra and Number Theory".
ROSU Grigore
University of Illinois at Urbana-Champaign, USA
Title: Matching Logic (details)
{\em Matching logic}, is a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the {\em patterns}, are constructed using {\em variables}, {\em symbols}, {\em connectives} and {\em quantifiers}, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that {\em match} it), in contrast to FOL where functions and predicates map into a domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, but it also admits its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages which have a rewrite-based operational semantics.
Inria, France
Title: Towards the synthesis of helper formulas in reachability logic-based program verification (details)
One major difficulty one faces when formally verifying programs with respect to Hoare-style logics is finding adequate helper formulas (e.g., inductive invariants for loops). In this talk I will describe progress in this direction for Reachability Logic, a recently introduced, language-independent logic of programs. I will show that reachability-logic formula verification can be reduced to standard abstraction-based verification techniques, and that reachability-logic formula synthesis can be reduced to Counter Example Guided Abstraction Refinement (CEGAR). Hence, the ongoing steady progress in abstraction-based verification and in CEGAR translates to progress in reachability-logic formula verification and synthesis.
University of Bucharest, Romania
Title: Pushdown Model Checking in the K Frammework (details)
University Politehnica of Bucharest, ROMANIA
Title: Statistical tests in cryptographic evaluation (details)
Statistical tests are an efficient tool for establishing the ownership of a set of independent observations to a specific population or probability distribution; they are used in the field of cryptography, specifically in randomness testing. Statistics can be useful in showing a proposed system is weak. Thus, one criterion in validating ciphers is that there is no efficient method for breaking it that brute force. That is, if we have a collection of cipher texts (and eventually the corresponding plain texts) all the keys have the same probability to be the correct key, thus we have uniformity in the key space. If we are analyzing the output of the cipher and find a non-uniform patterns than it can be possible to break it. But if we cannot find these non-uniform patterns no one can guarantee that there are no analytical methods in breaking it. This talk is about requirements for validating the security of cryptographic primitives by statistical methods, construction of statistical tests and sample requirements for testing cryptographic functions.
SIPOS Andrei
Institutul de Matematica al Academiei Romane, Romania
Title: Codensity and Stone spaces (details)
Codensity monads are a standard construction in category theory and/or functional programming that has been used to reduce the asymptotic performance of functional code, but also to provide a natural description of concepts like ultrafilters or ultraproducts. This talk has as its goal to lay bare similar "inevitability" results for Stone spaces and sober spaces. The category of Stone spaces will be characterized as the essential image of the codensity monad of the inclusion of the category of finite sets into the category of topological spaces. To obtain sober spaces, the category of finite sets will be replaces by another category for which we will provide the motivation.
TACHE Rozica - Maria
Faculty of Mathematics and Computer Science, University of Bucharest, Romania
Title: Extremal cacti graphs for general sum-connectivity index and Narumi-Katayama index (details)
Topological indices are molecular structure descriptors that play a fundamental role in QSAR, QSPR modeling. Denoting $d(u)$ the degree of a vertex $u\in V(G)$, we define the general sum-connectivity index of a graph $G$ as $\chi_\alpha(G)=\sum_{uv\in E(G)} \Bigl(d(u)+d(v)\Bigr)^\alpha$ with $\alpha$ a real number and Narumi-Katayama index as $NK(G)=\prod_{u\in V(G)} d(u)$. In this paper we determine the extremal cacti graphs for general sum-connectivity index and Narumi-Katayama index, with given girth or number of pendant vertices.
TIPLEA Ferucio Laurentiu
Department of Computer Science, "Alexandru Ioan Cuza" University of Iasi, Romania
Title: Symbolic and computational models for security policies and protocols (details)
Security policies and protocols are central to security and pervasive in computer systems. They can be found in many applications such as operating systems, firewalls, or protocols to secure network traffic. Although security policies and protocols may appear as conceptually straightforward, they are both very complex and error-prone in practice. Over the years, many efforts have been dedicated to a better understanding (specification and verification) of them. This talk is an (partial) informal survey and discussion of the logical and computational models developed so far to reason about security policies and protocols.
ZARA Catalin
UMass Boston, United States
Title: Tolerance Distances on Minimal Coverings (details)
We define distances on the space of minimal coverings of a finite set that generalize entropy distances on partitions, and establish connections between these spaces. The metric space of minimal coverings has multiple applications in machine learning and data mining, in areas such as multilabel classifications and determination of frequent item sets. (Joint work with Dan Simovici)