Mathematical Structures in Formal System Development and Analysis

a special session organized by Răzvan Diaconescu and Ionuț Țuțu of

The Ninth Congress of Romanian Mathematicians

July 2–3, 2019, in Galați, Romania

photo by Nica George; adapted Licenţa Creative Commons

The purpose of the session is to provide a forum of discussions for recent developments in advanced algebraic theories and techniques that are central to the use of formal methods for the specification, implementation, verification and certification of systems. The term systems is meant to be interpreted in its widest sense, encompassing software and hardware systems, as well as hybrid constructions. All the ideas discussed are expected to have a solid mathematical content and great potential for applicability.

Key mathematical themes to be discussed include, but are not limited to, category theory, model theory, (co)algebraic specification languages, methods and environments, term rewriting, proof systems, proof assistants, and interactive or automated deduction.

This event is organized with the support of the Simion Stoilow Institute of Mathematics of the Romanian Academy (IMAR). The organizers and many of the invited speakers and participants are former professors or master students at Şcoala Normală Superioară Bucureşti (SNSB) – who later studied and obtained PhD degrees at universities in Germany, Japan, UK and USA.

invited speakers

  • Daniel Găină
    Institute of Mathematics for Industry, Kyushu University

    Daniel Găină is an assistant professor at the Institute of Mathematics for Industry at Kyushu University, Japan. He received his PhD degree from the Japan Advanced Institute of Science and Technology (JAIST) in 2009, and continued his career at JAIST until 2017. During that time, he worked on the algebraic specification language CafeOBJ, providing support for Observational Transition Systems and enhancing its modularity. He joined the Institute of Mathematics for Industry in the spring of 2017.

    His current research focuses on the use of advanced model theory and category theory in order to develop solid mathematical foundations for the reconfiguration paradigm, which includes the design and implementation of a verification method for transition systems.
  • Andrei Pavelescu
    University of South Alabama

    Andrei Pavelescu is an assistant professor in the Mathematics Department at University of South Alabama. He received his Ph.D. degree from USC in 2012 under the supervision of Dr. Robert Guralnick.

    His main research focus lies within the realm of (finite) group theory and graph theory, although he also had encounters with number theory, ring theory and orderable groups.
  • Andrei Popescu
    Middlesex University London
    United Kingdom

    Andrei holds Ph.D. degrees in computer science from the University of Illinois at Urbana-Champaign and in mathematics from the University of Bucharest. Between 2010 and 2014 he worked as a postdoc at the Technical University of Munich. From 2014, he has been a Senior Lecturer at Middlesex University London. His research interests include theorem proving, (co)inductive datatypes, syntax with bindings, logical foundations, proof-assistant automation and verification of information-flow security. One of his main research vehicles is the Isabelle proof assistant. Together with colleagues, he has been developing Isabelle/HOL's infrastructure for (co)inductive datatypes and the verified conference management system CoCon. In the past, he worked on abstract model theory and fuzzy logic.
  • Ferucio Laurențiu Țiplea
    Alexandru Ioan Cuza University of Iași

    Ferucio Laurențiu Țiplea is a professor at the Alexandru Ioan Cuza University of Iași, Romania. He received his MSc and PhD degrees from the Alexandru Ioan Cuza University of Iași in 1986 and 1993, respectively. From 1990 to 1991 he was a member of the Faculty of Mathematics of the Alexandru Ioan Cuza University. He joined the Faculty of Computer Science in the autumn of 1991.

    His research interests include the high-level modelling, design and analysis of systems; cryptography and computer security; and algebraic foundations of computer science.
  • Uwe Egbert Wolter
    University of Bergen

    Uwe E. Wolter is associate professor at the University of Bergen, Norway. He received his PhD degree in 1989 from the Technical University Magdeburg, Germany. He was awarded with the Medal of Honour from the East-German Society of Mathematics for the best PhD thesis of the year. He held positions at Humboldt-University Berlin and Technical University Berlin before joining the Department of Informatics at the University of Bergen in 2000.

    His research interests can be characterized in two ways: Foundation of Formal Specifications, the broad topic, and Applied Category Theory, the method. He contributed to areas like Algebraic Specification, Abstract Model Theory, Graph Transformation, Coalgebra, Process Calculi and Knowledge Engineering. The last decade his research focuses on the foundation of model-driven software engineering.


tuesday, 2nd July

Registration & Opening
Andrei Popescu

Higher-Order Logic (HOL) is the foundation of some major proof assistants in current use. A crucial characteristic of developments in HOL-based proof assistants is the definitional approach: Whenever possible, concepts are introduced by definitions rather than arbitrary axioms. I will discuss the significance of following the definitional approach for the logical trustworthiness of formal developments. Then I will describe mathematical formulations of trustworthiness, having different degrees of strength – safety, conservativity and consistency – and I will compare and contrast model-theoretic and proof-theoretic techniques to prove them.

General congress activities & Lunch break
Uwe Egbert Wolter

Based on experiences in areas like Algebraic Specifications, Institutions, Graph Transformations, Coalgebras and Foundations of Model Driven Software Engineering, I will discuss the use of indexed and fibred structures in specification formalisms – their relationship as well as their advantages and disadvantages. Especially, I will address the topics model amalgamation, Grothendieck construction, van-Kampen square and (deep) meta-modeling. As a sample specification formalism, I will outline the Diagram Predicate Framework, a variant of the "generalized sketch" framework.

Tea/coffee break
Ferucio Laurențiu Țiplea

The quadratic residuosity problem is the problem to distinguish between the distributions of quadratic residues and quadratic non-residues modulo a composite integer. The intractability of the quadratic residuosity problem is the basis for the security of numerous constructions in cryptography, such as public-key and identity-based encryption schemes, pseudo-random generators, or cryptographic protocols. The aim of this talk is to provide a general overview on quadratic residuority problem and its applications to cryptography. Aspects related to the gap group of signed quadratic residues will also be discussed.

Adriana Balan

The familiar adjunction between ordered sets and completely distributive lattices can be extended to generalised metric spaces, that is, categories enriched over a quantale. The crucial point is an appropriate distributive law between the "down-set" monad and the "up-set" monad on the category of quantale-enriched categories. If the base quantale is a finite MTL-algebra, this distributive law can be concretely formulated in terms of operations, equations and choice functions, similar to the familiar distributive law of lattices.

Claudia Chiriță

We present two important features of the Haskell programming language, polymorphism and type-class polymorphism, to the dwellers of the model-theory universe. We start from higher-order logic with Henkin semantics (HNK), which allows us to capture some basic Haskell concepts and programs. Then, building on ideas from existing work on dealing with type-class polymorphism in an institutional setting, we outline a way of extending HNK to allow for parametric data types and polymorphic functions.

Daniel Găină

The concept of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the definition of hybrid institution captures the concept of hybrid logic, i.e. a type of modal logic expressive enough to allow references to the states of the models. In formal methods, hybrid logics are recognized as being suitable for describing reconfigurable systems. The present contribution sets the foundation of a formal verification methodology for reconfigurable systems by defining a proof calculus in an arbitrary hybrid institution. In order to prove completeness, the paper introduces the forcing technique for hybrid institutions and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the general results are instantiated to several benchmark examples of hybrid logical systems.

wednesday, 3nd July

Ionuț Țuțu

In universal algebra, the notion of congruence captures precisely those equivalence relations that allow for a natural algebraic structure to be defined on equivalence classes. This provides an important basic tool for building initial models and for proving completeness results in equational logics. In this talk, we take a category-theoretic route to defining congruences on Kripke structures by exploring a connection with universal constructions such as that of kernel pair and quotient object. The end result is a universal property of Kripke quotients, which we then use to show that every set of equational statements (in a suitable hybrid logic) admits an initial Kripke model.

Andrei Pavelescu

A simple graph is called intrinsically linked if every embedding of it into $R^3$ contains a non-trivial link. Campbell et al. showed that a graph on $n \geq 6$ vertices and at least $4n − 9$ edges is intrinsically linked because it contains a $K_6$; this implies that for a graph $G$ with $n \geq 15$ vertices, either $G$ or its complement is intrinsically linked. We improve this result by proving that given any simple non-oriented graph $G$ with at least thirteen vertices either $G$ or its complement is intrinsically linked. In the process, we discuss the de Verdière invariant, an algebraic construction which yields surprising results about the topological properties of a graph. We also discuss some constructions which attain maximal Hadwiger number for self complementary graphs.

Mihai Codescu

We present a tool for the specification and verification of reconfigurable systems. These are systems that have different modes of operation and commute between those modes during their execution as response to events. The foundation of the tool is provided by a generic method of adding features characteristic to hybrid logic, both at the syntactic and the semantic level, over an arbitrary base institution, via a process called hybridisation. Automated proof support for the logic thus obtained is provided via a generic methodology of proof-by-translation, where a conjecture is first translated to first-order logic then verified there using automated first-order provers. We describe how the hybridisation method and a language for specification of reconfigurable systems are implemented in an extension of the Heterogeneous Tool Set.

Tea/coffee break
Type theory or Model theory?
Andrei Popescu interviewed by Răzvan Diaconescu
General guidelines for the audience

  1. The interview will consist of a dialogue between Andrei Popescu and Răzvan Diaconescu.
  2. This means that there will be absolutely no verbal interaction with the audience.
  3. However, the members of the audience are welcome to submit questions or comments for the interviewer to consider and introduce into the dialogue at the most appropriate moment.
  4. All questions or comments should be submitted in written form either by e-mail to Răzvan Diaconescu before the interview (which is highly encouraged), or on a small piece of paper during the event.
  5. These rules will be *observed strictly*. For those who find them inconvenient, in order to avoid a personal discomfort, it would be worth considering not to participate.

Conclusions & Lunch break


If you have any questions or inquiries, you can contact the organizers via e-mail: