FROM2021

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

CFP – September 20, 2021

Invited Speakers

VOLKER DIEKERT
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 L₀g₁L₁…g_tL_t where all L_is 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

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.

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

ANDREI POPESCU
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.

FLORIN STOICAN
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.

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 is open until November 1, 2021. The registration form is available here.

Program

Wednesday, December 8th

11:00-11:50 Session 9: FROM Invited Talk (1)

CHAIR:

Mircea Marin

LOCATION: Room FROM

11:00

Volker Diekert

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

CHAIR:

Adrian Craciun

LOCATION: Room FROM

12:10	Horatiu Cheval Applications of the Lean theorem prover to proof mining (abstract)
12:30	Mihai Prunescu Secure Multiparty Computation in arbitrary rings (abstract)

14:00-14:50 Session 12: SYNASC and FROM Invited Talk (5)

CHAIR:

Ciprian Pungila

LOCATION: Room SYNASC – main

14:00

Dragos-Teodor Gavrilut

IoT security: The good the bad and the ugly (abstract)

15:10-16:00 Session 13B: FROM Invited Talk (3)

CHAIR:

Andrei Arusoaie

LOCATION: Room FROM

15:10

Radu Iosif

Local Reasoning about Parameterized Reconfigurable Distributed Systems (abstract)

16:20-17:00 Session 14: FROM Session (2)

Working Formal Methods Symposium

CHAIR:

Florin Craciun

LOCATION: Room FROM

16:20	Ioana Leuștean and Bogdan Macovei DELP: Dynamic Epistemic Logic for Security Protocols (abstract)
16:40	Alexandru-Ioan Lungu Alk Compound Data Types Translation in Z3 (abstract)