December 8-9, 2021, Timișoara, Romania

In conjunction with SYNASC 2021

Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and/or make the formal methods to work by creating or using software tools that apply theoretical contributions. Formal methods emphasize the use of mathematical techniques and rigor for developing software and hardware. They can be used to specify, verify, and analyse systems at any stage in their life cycle: requirements engineering, modeling, design, architecture, implementation, testing, maintenance and evolution. This assumes on one hand the development of adequate mathematical methods and frameworks and on the other hand the development of tools that help the user effectively apply these methods/frameworks.

FROM symposiums are  organized by the Faculty of Mathematics and Computer Science of the University of Bucharest, the Faculty of Mathematics and Computer Science of the Babes-Bolyai University of Cluj-Napoca, the Faculty of Computer Science of the Alexandru Ioan Cuza University of Iasi, and the  Faculty of Mathematics and Computer Science of the West University of Timișoara.

FROM 2021 is the fifth event in a yearly workshop series. The first edition was held in 2017 in Bucharest, the second edition was held in 2018 in Iaşi, the third edition was held in 2019 in Timişoara, while the fourth edition was organized in Cluj-Napoca as a virtual event due to the COVID-19 pandemic.

FROM 2021 is an associated workshop of  SYNASC 2021.

The program of the symposium includes invited lectures and regular contributions. Submissions on the general topics of formal methods, theoretical computer science, logic and applications are welcome.

Important Dates

  • September 29, 2021: Deadline for full paper submission.
  • October 7, 2021: Notification of acceptance.
  • October 15 2021: Submission of revised papers.
  • October 15, 2021: Registration.
  • December 8-9 2021: Symposium days.

Call for papers

Invited Speakers

University of Stuttgart

Decidability of membership problems in 2 × 2 matrices over rational numbers

The talk is based on a joint work with Igor Potapov and Pavel Semukhin (Liverpool, UK). It appeared as a conference abstract at ISSAC 2020. Our results relate numerical problems on matrices over the rationals to symbolic algorithms on words and finite automata.
Using exact algebraic algorithms and symbolic computation, we prove new decidability results for 2 × 2 matrices over ℚ. Namely, we introduce a notion of flat rational sets: if M is a monoid and N ≤ M is its submonoid, then flat rational sets of M relative to N are finite unions of the form L0g1L1…gtLt where all Lis are rational subsets of N and gi ∈ M. We give quite general sufficient conditions under which flat rational sets form an effective relative Boolean algebra.
As a corollary, we obtain that the emptiness problem for Boolean combinations of flat rational subsets of GL(2;ℚ) over GL(2;ℤ) is decidable. On the other hand, there is some evidence supporting our conjecture that the membership problem for rational subsets of GL(2;ℚ) is undecidable.

Bitdefender and "Alexandru Ioan Cuza" University of Iași

IoT security: The good the bad and the ugly

IoT industry have grown in the last couple of years to the point where many people are now using one or two IoT devices. Analysts like Gartner and Forrester predicted this growth and raised several security concerns (most of them being related to privacy and access to personal data). In particular for consumer users, this may also represent other security ricks such as data exfiltration. This presentation focuses on presenting the risks that come with IoT devices (in terms of privacy and access). As a practical aspect, some newly discovered IoT vulnerabilities ( in IoT devices like web-cameras or baby-monitors) with details on how these vulnerabilities were discovered and how they work will be presented.

VERIMAG - CNRS - University of Grenoble Alpes

Local Reasoning about Parameterized Reconfigurable Distributed Systems

This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs delete or create interactions or components while the system components change state according to their local behaviour. Our proof calculus uses a configuration logic that supports local reasoning and that relies on inductive predicates to describe distributed systems with an unbounded number of components. The validity of reconfiguration programs relies on havoc invariants, assertions about the ongoing interactions in the system. We present a proof system for such invariants in an assume/rely-guarantee style. We illustrate the feasibility of our approach by proving the correctness of self-adjustable tree architectures and provide tight complexity bounds for entailment checking in the configuration logic.
Joint work with Emma Ahrens and Joost-Pieter Katoen (RWTH Aachen) and Marius Bozga (VERIMAG).

University of Sheffield

Types-to-Sets for Theorem Proving in Higher-Order Logic

Users of interactive theorem provers based on Higher-Order Logic (such as HOL4 and Isabelle/HOL) find it very convenient to "ride" the HOL type system when defining concepts and reasoning about them -- within a paradigm that can be called *type-based reasoning*. However, to achieve higher flexibility, users often need to resort to *set-based reasoning*, which is more bureaucratic and less supported by automation. In previous work with Ondrej Kuncar, I developed a mechanism called Types-to-Sets that allows one to make the best of both worlds by offering a bridge between the simpler type-based theorems and the heavier set-based ones. In recent work jointly with Dmitriy Traytel I show that, contrary to the previous belief, the rules for moving from types to sets are admissible in the standard Higher-Order Logic used in theorem provers, so no extension of the axiomatization base is required. In this talk, I will motivate and introduce the Types-to-Sets framework, and will present the recent admissibility result and its connection to other concepts such as Reynolds-style parametricity and compositional (co)datatypes.

Polytechnic University of Bucharest

On the use of spline functions in motion planning

B-spline and NURBS functions are popular choices for describing trajectories associated with nonlinear dynamics and for imposing continuous-time constraint validation. Exploiting their properties (local support, convexity and positivity) usually leads to sufficient conditions which are conservative and difficult to handle as part of an optimization problem.
In this talk I will present several methods which reduce the conservatism and complexity of the approach. First, I will make use of knot refinement strategies to improve arbitrarily-well on the sufficient conditions. Second, I will provide approximate solutions which reduce significantly the computational effort at the price of a moderate loss in performance. The approaches are validated for a motion planning problem where off-line trajectories with obstacle(s) avoidance guarantees are generated.


Program Commitee

Andrei Arusoaie, Alexandru Ioan Cuza University of Iași
Adrian Crăciun, West University of Timișoara
Florin Crăciun, Babeș-Bolyai University of Cluj-Napoca
Cătălin Dima, Université Paris-Est Créteil
Ioana Leuştean, University of Bucharest
Laurențiu Leuştean, University of Bucharest (Co-chair)
Dorel Lucanu, Alexandru Ioan Cuza University of Iași
Mircea Marin, West University of Timișoara (Co-chair)
Simona Motogna, Babeș-Bolyai University of Cluj-Napoca
David Nowak, CNRS & University of Lille
Grigore Roşu, University of Illinois at Urbana-Champaign
Vlad Rusu, INRIA Lille Nord Europe
Viorica Sofronie-Stokkermans, University Koblenz-Landau

Organising Commitee

Isabela Drămnesc, West University of Timișoara
Mircea Marin, West University of Timișoara (Chair)
Natalia Ozunu (Moangă), University of Bucharest


The registration fee is 100 Euro.
It covers the symposium kit, refreshments during breaks, lunches, symposium dinner, publication.
The registration is open until November 1, 2021. The registration form is available here.


Wednesday, December 8th
11:00-11:50 Session 9: FROM Invited Talk (1)
Decidability of membership problems in 2 × 2 matrices over rational numbers (abstract)
12:10-12:50 Session 11: FROM Workshop (1)

Working Formal Methods Symposium

Applications of the Lean theorem prover to proof mining (abstract)
Secure Multiparty Computation in arbitrary rings (abstract)
14:00-14:50 Session 12: SYNASC and FROM Invited Talk (5)
IoT security: The good the bad and the ugly (abstract)
15:10-16:00 Session 13B: FROM Invited Talk (3)
Local Reasoning about Parameterized Reconfigurable Distributed Systems (abstract)
16:20-17:00 Session 14: FROM Session (2)

Working Formal Methods Symposium

DELP: Dynamic Epistemic Logic for Security Protocols (abstract)
Alk Compound Data Types Translation in Z3 (abstract)
Thursday, December 9th
14:00-14:50 Session 18B: FROM Invited Talk (4)
On the use of spline functions in motion planning (abstract)
15:10-16:00 Session 19: FROM Invited Talk (5)
Types-to-Sets for Theorem Proving in Higher-Order Logic (abstract)
16:20-17:00 Session 21: FROM Session (3) + Round Table

Working Formal Methods Symposium

Software Testing Using Formal Methods (abstract)


Universitatea de Vest din Timișoara

Bulevardul Vasile Pârvan 4, Timișoara 300223

Travel arrangements