





List of talks 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) 1.
ARUSOAIE Andrei andrei.arusoaie@inria.fr
INRIA LilleNord Europe, France Title: Language Independent Symbolic Execution (details) Abstract:
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 languageindependent 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. 2.
BARONI Marian Alexandru marianbaroni@yahoo.com
Dunarea de Jos University of Galati, Romania Title: Order locatedness and strong extensionality in constructive mathematics (details) Abstract:
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. 3.
CIOBACA Stefan stefan.ciobaca@gmail.com
Faculty of Computer Science, University "Al. I. Cuza" Iasi, Romania Title: Proving Program Equivalence (details) Abstract:
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 languageindependent matter. Our proof system for program equivalence is parameterized by the semantics of the languages in which the two programs are written. 4.
CIOBANU Gabriel gabriel@iit.tuiasi.ro
Romanina Academy, Iasi branch, Romania Title: Probabilistic Logic for Timed Migration (details) Abstract:
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 picalculus, 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 steadystate 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 steadystate behaviours. Finally, we present a verification algorithm for PLTM, and determine its time complexity. Given that PLTM operates at the level of discretetime Markov chains, it can also be applied to other process algebras which involve locations, timers, process movements and communications. 5.
DIACONESCU Denisa denisa.diaconescu@gmail.com
Mathematical Institute, University of Bern / Faculty of Mathematics and Computer Science, University of Bucharest, Switzerland / Romania Title: Automata, Logic and Stone Duality (details) Abstract:
The aim of this talk is to explain the role of Stone duality for defining a dictionary capable of translating finite automata (considered as settheoretical 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 nonclassical logics. We explain our method for Godel logic. 6.
DIMA Catalin dima@upec.fr
LACL, UniversitÃ© ParisEst, France Title: The automatalogic duality for temporal epistemic frameworks (details) Abstract:
We present a number of recent results on expressiveness and decidability of temporal epistemic logics in which automata theory plays an important role. 7.
LUCANU Dorel dlucanu@info.uaic.ro
Universitatea "Alexanfru Ioan Cuza", Romania Title: Proving Reachability Properties by Circular Coinduction (details) Abstract:
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. 8.
MARDARE Radu mardare@cs.aau.dk
Aalborg University, Denmark Title: Stone Dualities for Markov Processes (details) Abstract:
We present a series of duality results involving Markov processes (MPs) and a special class of Boolean algebras with operators corresponding to (the noncompact) 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. 9.
MINEA Marius marius@cs.upt.ro
Politehnica University of TimiÈ™oara, Romania Title: Modeling and verification of security for web applications and services (details) Abstract:
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. 10.
PETRE Luigia lpetre@abo.fi
Ã…bo Akademi University, Finland Title: A Theory of Service Composition (details) Abstract:
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, nondeterministic. 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. 11.
POPESCU Andrei a.popescu@mdx.ac.uk
Middlesex University, London, United Kingdom Title: A Conference Management System with Verified Document Confidentiality (details) Abstract:
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 multiuser webbased system (such as a conference system) is a complex inputoutput 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. 12.
POPOVICI Matei matei.popovici@cs.pub.ro
POLITEHNICA University of Bucharest, Romania Title: Semantic variants of (truely) perfect recall in AlternatingTime Temporal Logic (details) Abstract:
AlternatingTime 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 noforgetting phenomenon and put forward a semantics of truely perfect recall. 13.
PRUNESCU Mihai mihai.prunescu@gmail.com
IMAR, Romania Title: Recurrent manydimensional sequences over finite alphabets (details) Abstract:
Recurrent manydimensional sequences over finite alphabets are considered. Aspects of symmetry, automaticity, generability by contextfree substitutions and power of expressions are discussed. Many aspects maybe also of interest for the section "Algebra and Number Theory". 14.
ROSU Grigore grosu@illinois.edu
University of Illinois at UrbanaChampaign, USA Title: Matching Logic (details) Abstract:
{\em Matching logic}, is a firstorder 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 powerset 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 offtheshelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly wellsuited for reasoning about programs in programming languages which have a rewritebased operational semantics. 15.
RUSU Vlad Vlad.Rusu@inria.fr
Inria, France Title: Towards the synthesis of helper formulas in reachability logicbased program verification (details) Abstract:
One major difficulty one faces when formally verifying programs with respect to Hoarestyle 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, languageindependent logic of programs. I will show that reachabilitylogic formula verification can be reduced to standard abstractionbased verification techniques, and that reachabilitylogic formula synthesis can be reduced to Counter Example Guided Abstraction Refinement (CEGAR). Hence, the ongoing steady progress in abstractionbased verification and in CEGAR translates to progress in reachabilitylogic formula verification and synthesis. 16.
SERBANUTA Traian traian.serbanuta@fmi.unibuc.ro
University of Bucharest, Romania Title: Pushdown Model Checking in the K Frammework (details) Abstract:
TBD 17.
SIPOS Andrei andrei.v.sipos@gmail.com
Institutul de Matematica al Academiei Romane, Romania Title: Codensity and Stone spaces (details) Abstract:
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. 18.
TIPLEA Ferucio Laurentiu fltiplea@info.uaic.ro
Department of Computer Science, "Alexandru Ioan Cuza" University of Iasi, Romania Title: Symbolic and computational models for security policies and protocols (details) Abstract:
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 errorprone 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. 