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

Logic in Computer Science (special session) 

(this list is in updating process)

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.
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.
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.
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.
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)
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.
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.