The 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 by creating or using software tools that apply theoretical contributions.
Please register by filling in this form. Participants are encouraged to register by September 14, although registration will remain open until and during the conference. The registration fee is 300 euros. Payment information. If you are not an invited speaker or you have a fee waiver, please transfer the registration fee to the following account (mention your name and "FROM 2025" in the transfer):
Account holder: ASOCIATIA ROMANA DE LINGVISTICA COMPUTATIONALA Account holder address: Iancu Bacalu street, no. 3, Iasi, Romania Bank : BRD – GROUPE SOCIETE GENERALE Bank address: Iasi Branch, P-ta Unirii nr.2 Bl. B10 Iasi, Romania SWIFT: BRDEROBU Account EURO: IBAN RO19BRDE240SV00697012400If you would like to apply for a registration fee waiver, please contact us at andrei.arusoaie@uaic.ro.
See the list of accepted papers with abstracts.
A sequence of elements is said to be bad for a quasi-order if no element of the sequence is larger than or equal to a previous element. A quasi-order is said to be well if every bad sequence is finite. Well-quasi-orders (wqo for short) is a central notion for proving some decidability results. For instance, the termination of the Karp and Miller algorithm relies on a wqo. Intuitively, the proof of termination is obtained by observing that if the algorithm does not terminate, ultimately, it should compute an infinite bad sequence. Wqo can also be used for proving complexity results. By controlling with a function the way elements of a sequence can grow respectively to its position in the sequence, bounds on the maximal length of a bad sequence can be derived. As an example, the length of a bad sequence of vectors of natural numbers for the component-wise ordering is bounded by an Ackermann function for linearly controlled functions. Recently wqo was also used for explaining the data-structures computed by the KLM algorithm, an algorithm for deciding the reachability problem for Petri nets. Intuitively, the data-structures computed by the KLM algorithm are related to the classical notion of decomposition of downward-closed sets into ideals.
In this talk, we will survey past and recent results about wqo with a special focus on the reachability problem for Petri nets.
Almost sure termination, or termination with probability one, is the core liveness property for randomized algorithms.
It is the probabilistic analogue of program termination.
We study proof rules for almost sure termination. While many proof rules for termination were proposed over the years, none were known to be both sound and complete.
This was in contrast to the non-probabilistic setting, for which we have known complete proof rules for many years.
We show a sound and complete proof rule for almost sure termination.
Using our proof rule, we study some classical randomized distributed algorithms and show how to construct termination proofs.
Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated function parameters. One inherent limitation of existing specification mechanisms is its reliance on only two stages: an initial stage to denote the precondition at the start of the method and a final stage to capture the postcondition. Such two-stage specifications force abstract properties to be imposed on unknown function parameters, leading to less precise specifications for higher-order methods.
To overcome this limitation, we introduce a novel extension to Hoare logic that supports multiple stages for a call-by-value higher-order language with ML-like local references.
In this talk, we introduce our staged logic with its semantics, and show how it can be used to handle higher-order imperative programs, including those that arise from the use of delimited continuations (from algebraic effects).
Zero-knowledge (ZK) proof systems have received increasing attention in recent years, driven in large part by applications in blockchain and privacy-preserving computation. While many advances have focused on certifying the correctness of computations with partial information hidden from the verifier, recent efforts–such as zkUNSAT[1], zkSMT[2], and zkPi[3]–have begun to explore the use of ZK techniques to certify mathematical proofs themselves.
This talk introduces a new general-purpose language for expressing proofs and computations, grounded in principles from logic programming, and designed to enable the efficient construction of arithmetic circuits suitable for zero-knowledge proof systems. The language is implemented as part of PiSquared’s Proof-of-Proof framework and aims to bridge declarative proof development with low-level ZK-friendly circuit representations.
We illustrate the approach through a case study on certifying unsatisfiability refutations, yielding a tool comparable in functionality to zkUNSAT. The derivation methodology and circuit-generation process will be illustrated through concrete examples, highlighting both expressiveness and performance.
References
[1] Luo, N., Antonopoulos, T., Harris, W. R., Piskac, R., Tromer, E., & Wang, X. (2022, November). Proving UNSAT in Zero Knowledge. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 2203-2217).
[2] Luick, D., Kolesar, J. C., Antonopoulos, T., Harris, W. R., Parker, J., Piskac, R., ... & Luo, N. (2024). zkSMT: A VM for Proving SMT Theorems in Zero Knowledge. In 33rd USENIX Security Symposium (USENIX Security 24) (pp. 3837-3845).
[3] Laufer, E., Ozdemir, A., & Boneh, D. (2024, December). zkPi: Proving Lean Theorems in Zero-Knowledge. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security (pp. 4301-4315).
The presentation reveals how Continental chose to pursue the endeavor of automated synthesis of correct-by-design in-vehicle system architectures. Aspects related to types of problems solved, use-cases, necessary models, annotations, typical constraints and optimization objectives are discussed for a realistic automotive system. Implementation alternatives are showcased and thoughts on upcoming challenges are shared with the audience.
FROM 2025 is organied by:
The Faculty of Computer Science, Alexandru Ioan Cuza University, Iași,
Romania
in collaboration with:
Asociația Română de Lingvistică Computațională (The Romanian Association for Computational Linguistics)
under the aegis of the Alexandru Ioan Cuza University of Iași.
FROM 2025 is organized by the Faculty of Computer Science in Iaşi, and it is part of a series of symposiums organised on a rotating basis by the Faculty of Mathematics and Computer Science of the University of Bucharest, the Faculty of Mathematics and Computer Science of the Babeș-Bolyai University of Cluj-Napoca, the Faculty of Computer Science of the Alexandru Ioan Cuza University of Iași, and the Faculty of Mathematics and Computer Science of the West University of Timișoara
Alexandru Ioan Cuza University
Faculty of Computer Science
Room: TBA
General Berthelot St, 16, Iași, România
You can reach Iaşi by plane (check the Iași Airport page for details), by train (tickets available via CFR Călători), or by car (the distance to Bucharest is ~400km, 6 hours).
We plan to arrange accommodation at Gaudeamus University Hotel, but availability is limited. However, nearby hotels include Hotel Unirea, Hotel Traian, and Apartment Hotel Prestige.
Email one of the organizers at andrei.arusoaie@uaic.ro or stefan.ciobaca@uaic.ro.