Challenges and Perspectives of Formal Methods for Trustworthy Software is a series of seminars that will be held by well-known speakers, organised by the PhD in Computer Science of University of Pisa in collaboration with IMT Lucca, as part of their Research Topics in Software Quality series.
Software artifacts are challenging to develop and reason about. Not surprisingly, there have been many efforts in formally specifying, modeling and verifying software artifacts. This seminar series aims at enabling conversations and solutions cutting across the variety of techniques and tools developed by the formal methods communities, leveraging the complementary strengths of these solutions. We also recognize that formal methods education is an integral component of the dissemination of research ideas for industrial-scale verification projects. Therefore, another important objective of these seminars is to draw up a plan to train and teach relevant formal methods to students.
To get the credits for this seminar series, each PhD student must attend 80% of the seminars.

To participate in the seminars please contact gian-luigi.ferrari@unipi.it or chiara.bodei@unipi.it.

• March, 5, at 16:00: Gabriele Tedeschi
  Location: Sala Seminari Ovest online.
  Title: Symbolic Verification of Quantum Protocols: Quantum Probabilities to the Rescue
  Abstract:The field of Quantum Communication has produced numerous Quantum Protocols, addressing problems like key distribution, leader election, bit commitment and many more. Yet, there is no established verification framework to check the correctness and security of these protocols, as the well-studied techniques for probabilistic systems are often inadequate in the quantum setting. We will explore a new semantic model made of "Quantum Distributions" and "Quantum Transition Systems", instead of probability distributions and probabilistic LTSs. This provides a symbolic, input-independent semantics for a simple quantum process calculus, and an efficient algorithm to check equivalence of symbolic systems. Finally, we prove the symbolic equivalence to be sound and complete with respect to the known ground, probabilistic behaviour of quantum processes.
  Short Bio: Gabriele Tedeschi is a postdoctoral researcher in Computer Science, working on Quantum Computation and Communication. His research focuses on automated verification of quantum communication protocols, combining Formal Methods techniques with the mathematical language of Quantum Theory. He is a Science Communication enthusiast, organizing teaching activities and outreach events on Computer Programming and Quantum Technologies.


• March, 17, at 14:00: Giuseppe Bisicchia
  Location: Sala Seminari Ovest online.
  Title: From Requirements to Runtime: QoS-Aware Orchestration in Quantum Software Engineering
  Abstract:Quantum Software Engineering (QSE) applies established software-engineering practices (such as requirements, architecture, testing, reliability, and performance engineering) to the development and operation of quantum applications spanning heterogeneous hardware and cloud platforms. Building on this foundation, this talk first frames the main obstacles that make such rigor necessary: hybrid quantum-classical workflows, hardware variability and noise, resource constraints, and rapid platform evolution. It then grounds these challenges in a concrete QSE use case: shot-wise distribution, where shots are distributed across multiple QPUs to improve throughput, reduce latency, and increase robustness to device-level fluctuations. We discuss how to balance statistical accuracy, cost, and runtime while coping with backends that differ in capabilities and queue dynamics. To make these trade-offs systematic rather than ad hoc, the talk introduces a second, complementary theme: Quality-of-Service (QoS) derived from user requirements. We discuss how constraints on time, budget, and accuracy can be stated explicitly and translated into scheduling and shot-allocation decisions across the available QPUs. Finally, we present a high-level DSL that connects intent to execution by capturing QoS goals and orchestration policies (e.g., latency–fidelity trade-offs, device preferences, and allocation rules), enabling portable, auditable multi-QPU execution.
  Short Bio: Giuseppe Bisicchia is a postdoctoral researcher at the University of Pisa in the field of Software Engineering. His research focuses on the design and analysis of complex, distributed systems, with particular attention to the integration of emerging technologies and their impact, such as Quantum Computing. Alongside his scientific work, he is actively involved in STEAM education, from primary school to university level, designing and delivering training programs and hands-on workshops. He also organizes public outreach events focused on quantum technologies, including the Quantum Festival.


• March, 26, at 16:00: Francesco Tosoni
  Location: Sala Seminari Ovest
  online.
  Title: The Software Heritage Open Science Ecosystem: Preserving software as executable knowledge.
  Abstract: Modern science does not merely use software; it is increasingly encoded within it. Source code represents executable knowledge, documenting the precise logic of experiments and the provenance of discoveries. Yet, this knowledge is remarkably fragile, threatened by platform volatility and the lack of formal archival standards. This lecture explores Software Heritage (SWH), the world’s largest public archive of software source code. Launched by Inria in partnership with UNESCO, SWH has captured over 27 billion unique files from 421 million projects (as of January 2026). We will examine the technical foundation of the archive: a massive, deduplicated Merkle Directed Acyclic Graph (DAG). This architecture enables planetary-scale empirical research into software evolution, vulnerability propagation, and contributor ecosystems, supporting digital sovereignty and the development of open and transparent AI models. We will further discuss how SWH addresses the four pillars of software as scholarly output—archival, reference, description, and citation—using Persistent Identifiers (SWHIDs). By integrating with open-access repositories like Zenodo and HAL, SWH provides a shared foundation for reproducible research across disciplines. The session will conclude with a look at frontiers in large-scale code search and storage efforts within the CodeCommons initiative. Research Opportunity: Following the lecture, a Master’s thesis proposal will be presented: "From Code Archival to Knowledge Graph: Integrating Software Heritage into the Semantic Web via COAR Notify." The project aims to bridge the "semantic gap" by linking SWH with Wikidata, creating a unified, queryable knowledge graph for the global research community.
  Short Bio: Francesco Tosoni is a Postdoctoral Researcher at the Sant’Anna School of Advanced Studies, where his work focuses on the intersection of compressed data structures, green algorithm engineering, and large-scale code archives. He earned his PhD from the University of Pisa in 2024, following a joint Master’s degree from the University of Pisa and the Sant’Anna School—a thesis for which he received the 2020 Best Master’s Thesis Award from con.Scienze. His research is driven by the challenge of "computation-friendly" compression: developing techniques that allow for direct operations on compressed data without the overhead of decompression. Beyond the lab, he is a Wikimedia technical volunteer: he serves as a translation administrator on Meta-Wiki, a contributor to the Diff blog, and is a member of the Indic MediaWiki developers group. Whether optimising I/O-efficient indexing for Software Heritage or contributing to Wikidata, his goal remains the same: making open data more efficient, accessible, and sustainable.

• Chiara Bodei: chiara.bodei@unipi.it
• Gian-Luigi Ferrari: gian-luigi.ferrari@unipi.it