## WORKING FORMAL METHODS SYMPOSIUM

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

#### VOLKER DIEKERT

University of Stuttgart

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

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 L

_{0}g

_{1}L

_{1}…g

_{t}L

_{t}where all L

_{i}s are rational subsets of N and g

_{i }∈ 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.

#### DRAGOȘ GAVRILUȚ

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

*IoT security: The good the bad and the ugly
*

#### RADU IOSIF

VERIMAG - CNRS - University of Grenoble Alpes

*Local Reasoning about Parameterized Reconfigurable Distributed Systems
*

Joint work with Emma Ahrens and Joost-Pieter Katoen (RWTH Aachen) and Marius Bozga (VERIMAG).

#### VICTOR MITRANA

University of Bucharest

*Group memory complexity of extended finite automata over groups*

#### ANDREI POPESCU

University of Sheffield

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

#### FLORIN STOICAN

Polytechnic University of Bucharest

*On the use of spline functions in motion planning*

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.

## Commitees

#### 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 |

## Registration

The registration fee is 100 Euro.

It covers the symposium kit, refreshments during breaks, lunches, symposium dinner, publication.

The registration form will be available from October 15.

## Program

TBA

## Venue

**Universitatea de Vest din Timișoara**

Bulevardul Vasile Pârvan 4, Timișoara 300223

#### Travel arrangements

#### Accommodation