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.

Challenges and Perspectives of Formal Methods for Trustworthy Software and Research Topics in Software Quality is a series of seminars that will be held by well-known international 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.
The first part of these seminars will also be offered to MS students within the course "Laboratory for Innovative Software".
To get the credits for this seminar series, each PhD student must attend 80% of the seminars.
The seminars address methods and techniques that foster the security of applications and systems from their design and implementation, by focusing on formal methods and the features and properties of programming languages.

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

• February, 29, at 16:00: Elena Di Lavore
  
  Location: Aula Seminari Ovest, Computer Science Department and online
  Title: Effectful trace semantics via effectful streams
  Abstract:I will introduce effectful streams, a coinductive semantic universe for effectful dataflow programming and traces. As an example, we formalise the stream cipher cryptographic protocol. In monoidal categories with conditionals and ranges, effectful streams particularize to families of morphisms satisfying a causality condition. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; bisimulation implies effectful trace equivalence. This is recent joint work with Filippo Bonchi and Mario Román.
  
  Short Bio: I am a postdoctoral researcher at the University of Pisa, working with Filippo Bonchi. Until November 2023, I was a PhD student in the Compositional Systems and Methods group at Tallinn University of Technology under the supervision of Paweł Sobociński.
  I am interested in (categorical) semantics of programming languages. I have worked on a partial version of Markov categories, and stochastic and effectful dataflow. For my thesis, I have worked on monoidal width, a measure of computational complexity for morphisms in monoidal categories.



• March, 21, at 16:00: Arend Rensink
  
  Location: Aula Seminari Ovest, Computer Science Department and online
  Title: Graph transformation for modelling and verification
  Abstract: Artefacts in many domains, including software, are naturally represented using graphs or diagrams, which in their most basic form consist of (labelled) nodes and arrows. Changes to such artefacts can then be systematically captured by transformation rules. This gives rise to the modelling paradigm of graph transformation, in which graphs and transformation rules are the fundamental concepts. In this presentation, after recalling the fundamental concepts, we show how graph transformation systems (a set of rules applied to a start graph) can be used for modelling (i) grammars, (ii) relations and (iii) behaviour. Each type of model has its own characteristics, and we show some of the analysis techniques that come into play. In particular, we discuss how state space exploration and model checking can be used for behavioural analysis. Where relevant, we will demonstrate the concepts in the presentation using the tool GROOVE (Graphs for Object-Oriented Verification).
  
  Short Bio: Arend Rensink is full professor at University of Twente. He said about himself: I am fascinated and inspired by how systems work, in their composition from small interacting building blocks. To understand the behaviour of both the building blocks and their composition, modelling is the first step. For me, the search for understanding therefore starts with the search for the right modelling paradigm. This is closely followed by a desire to make that paradigm applicable, which means scalability and, in particular, tool support. As a field of application, I typically look at software systems and their functional behaviour, while not ignoring the connection with other types of (quantitative multi-paradigm) modelling. This means that my research interest can be circumscribed as foundations of model-driven software engineering. This applies to all phases of the engineering life cycle, from analysis and design to implementation, validation and maintenance. After having studied various aspect of process algebra (in particular action refinement) in the more distant past, in the last twenty years I have based most of my research on graph transformation as the basis for model-driven software development. Within that specialisation, while taking note of the beautiful deep embedding in category theory, my focus on applicability has led me to study the us of graph transformation to generate models that can then be formally verified. This goes hand in hand with tool support, and I have been the prime mover behind the graph transformation tool GROOVE, which has over the decades grown out to be one of the more widely used (academy-ware) graph transformation tools in both research and education.



• April, 4, at 16:00: Lorenzo Ceragioli
  
  Location: Aula Seminari Ovest, Computer Science Department and online
  Title: Specifying, Verifying and Comparing Information Flow Control in SELinux Configurations 
  Abstract: Security Enhanced Linux (SELinux) is a security architecture for Linux implementing Mandatory Access Control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. However, its application is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. Despite CIL’s high level features, CIL configurations are hard to understand as different constructs interact in non-trivial ways. Moreover, there is no mechanism to ensure that a given configuration obeys desired information flow policies. To remedy this, we enrich CIL with a formal semantics, and we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements. Using IFCIL, administrators can express confidentiality, integrity, and non-interference properties.
  
  Short Bio: Lorenzo Ceragioli is assistant professor at IMT Lucca, and part of the SySMA research group. He obtained a master degree “cum laude” in Computer Science at the University of Pisa, in 2018. In the same year Lorenzo started a Ph.D course in computer science in Pisa, which was dedicated to language-based security as a student of Pierpaolo Degano and Letterio Galletta. In collaboration with research groups from Ca’ Foscari, ETH Zurich and King’s College, he focused on the application of formal methods to real-world scenarios of security, targeting widespread technologies for access control: firewalls, operating systems and collaborative distributed environments. After receiving the Ph.D in 2022, Lorenzo started working as a research fellow with Fabio Gadducci on assessing behavioural equivalence for quantum processes, at the Department of Computer Science of the University of Pisa. Lorenzo Ceragioli is co-supervisor of Giuseppe Lomurno and Gabriele Tedeschi (in Pisa), and of Edoardo Lunati (IMT Lucca). His research interests include modeling and verification of quantum systems and formal methods for computer security, in particular applied to Access Control.



• April, 17, at 16:00: Andrea Vandin
  
  Location: Aula Seminari Ovest, Computer Science Department and online
  Title: Bisimulation in the wild: efficient reductions for biological and dynamical systems
  Abstract: Bisimulation is a concept widely used in theoretical computer science to reduce models while preserving properties of interest or comparing the behaviour described by models. It has been originally developed for qualitative models, and later extended to quantitative ones rediscovering results from lumping of Markov chains. This seminar aims to provide an overview of several results regarding the development of new notions of bisimulations to reduce models from various domains. The domains considered in this study range from biology to computer science and engineering and beyond, covering popular formalisms such as ordinary differential equations, chemical reaction networks, networks, Boolean networks, and Markov chains. The results have been collected in a tool called ERODE (www.erode.eu), which features a modern graphical user interface. These findings have been presented at various esteemed venues in computer science, bioinformatics, control engineering, and beyond, including LICS, POPL, Bioinformatics, CDC, IEEE TAC, and PNAS.
  
  Short Bio: Andrea Vandin is an Associate Professor in Computer Science within the Department of Excellence L'EMbeDS and the Institute of Economics at Sant'Anna School for Advanced Studies, Pisa, Italy. He also is an Adjunct Associate Professor at DTU Technical University of Denmark. Andrea pursues interdisciplinary research with societal impact.
  Andrea has: - Published more than 70 peer-reviewed publications in some of the best venues in Computer Science and beyond - Obtained 4 grants (3 as PI, 1 co-PI) for about 660K EUR - Extensive experience in some of the best-reputed universities in Europe - Extensive experience in designing courses for (under)graduate and PhD students in Computer Science, Engineering, Social Sciences, and Life Sciences. - Has (co)-supervised 5 PhD students, and is (co)-supervising 5 PhD students
  Before joining Sant'Anna, Andrea was an Associate Professor in Quantitative Formal Methods at DTU. Previously, Andrea has been an Assistant Professor at IMT Lucca, and a Senior Research Assistant at Southampton University, UK. Andrea received a PhD in Computer Science and Engineering from IMT Lucca and graduated cum laude in Computer Science at the University of Pisa, Italy.



• April, 18, at 16:00: Marco Carbone
  
  Location: online
  Title: An Introduction to Session Types
  Abstract: Session types are type annotations used by programmers for typing communication interactions between endpoints in a concurrent system. In the last decade, session types have been studied thoroughly, both from a theoretical and from a practical viewpoint. In this introduction, I will give a gently introduction to session types in general and discuss current ongoing work by the session type community.
  
  Short Bio: Marco Carbone is an Associate Professor at the Computer Science Department, IT University of Copenhagen, a member of the Programming, Logics and Semantics research group and the Center of Information Security and Trusts. Marco's core research interests are within applications of semantics, type theory, and linear logic to concurrency. In particular, he has been working on the theory of the pi-calculus, session types, and choreographies.



• April, 23, at 16:00: Luca Padovani
  
  Location: Aula Seminari Ovest, Computer Science Department and online
  Title: Fair termination of binary sessions
  Abstract: Sessions are private communication channels that enable the compositional static analysis of distributed systems. Well-typed sessions enjoy a number of desirable properties, such as communication safety, protocol fidelity and deadlock freedom. In this talk we will see a session type system aimed at ensuring lock freedom, namely that every pending input/output action within a session is eventually performed. The type system is based on the observation that lock freedom is implied by the conjunction of deadlock freedom and of fair termination, the latter being a termination property that holds under a given fairness assumption: in principle, a fairly terminating process may have an infinite execution; in practice, all of its fair (i.e. "realistic") executions are finite. We will focus on one particular formulation of the type system that uses the correspondence between session types and linear logic propositions with fixed points.
  
  Short Bio: Luca Padovani is associate professor of Computer Science at the University of Camerino. Before he has been researcher and then associate professor at the University of Urbino and the University of Torino. He studied at the University of Bologna where he defended a PhD thesis on digital typography of mathematical documents. After that, his research interests shifted to concurrency theory and type systems for distributed systems. He is now an active member of the community working on session types. On clear nights, Luca Padovani is an amateur astrophotographer.



• May, 7, at 16:00: Mila Dalla Preda
  
  Location: online
  Title: Measuring the (im)-precision of program analysis
  Abstract: Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In program analysis, this corresponds to the release of false alarms that represent the imprecision in the analysis introduced by the approximation. Program analysis tools have to deal with false alarms, and it is very important to have methods to control them. In this work, we focus on static program analysis by abstract interpretation and we provide a framework for estimating the imprecision accumulated during the analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise, namely it produces no false alarms, when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness, the abstract interpreter may produce a bounded number of false alarms.
  
  Short Bio: Mila Dalla Preda è Professore Associato di Informatica presso il Dipartimento di Informatica delll'Università di Verona. I suoi interessi di ricerca affrontano:
  • Studio e sviluppo di soluzioni software per la protezione della proprietà intellettuale e l'integrità del codice. In particolare, tecniche di offuscamento del codice, tecniche di marcatura/firma del codice (SW watermarking) e tecniche di identificazione di violazioni del codice (tamper proofing)
  • Studio e progettazione di strumenti automatici per il riconoscimento di comportamenti malevoli sfruttando proprietà semantiche del codice
  • Studio e progettazione di strumenti automatici per l'analisi di similarità del codice seguendo sia approcci statici che dinamici
  • Studio del comportamento di codici auto-modificanti, ovvero che cambiano durante l'esecuzione



• May, 16, at 16:00: Emilio Tuosto
  
  Location: online
  Title: Behavioural Specifications and Quantitative Techniques
  Abstract: This talk gives a bird-eye view of the literature at the intersection between quantitative techniques and behavioural specifications. More precisely, following the chronological order, the talk surveys the papers concerned with resource awareness, time, and probabilities. The talk strives to succinctly highlight the main contributions of each paper and distill some interesting open problems. Although related to the topic of the talk, data-awareness was intentionally left out of the exposition in order to maintain the focus centred on quantitative approaches.
  
  Short Bio: Emilio Tuosto is a full professor in Computer Science at the Gran Sasso Science Institute (GSSI) in L'Aquila (Italy), which he joined in 2019. From 2005 to 2019 Emilio worked at the Department of Computer Science of the University of Leicester (UK) initially as lecturer and then as an associate professor. Before moving to UK, Emilio had been a research associate from 2003 to 2005 at the University of Pisa where he also got his PhD and MSc in Computer Science. Emilio's main research interests are in foundations of concurrent and distributed computations. Recently Emilio has been active in the area of behavioural specifications and distributed computations. In particular, Emilio is interested in the development of theories and formal methods for the coordination of distributed systems.



• May, 28, at 16:00: Ugo Dal Lago
  
  Location: online
  Title: From Equivalences to Metrics, Effectfully
  Abstract: Program equivalence is one of the fundamental concepts in the theory of programming languages. In defining the underlying relation, one always strives for compositionality, so that the principle of substitution of equals by equals holds and equational reasoning remains sound. Would it be possible to make equational reasoning compatible with natural generalizations of the notion of equivalence, and with notions of program distance in particular? In this talk, we describe a series of situations in which quantitative reasoning is desirable, together with some proposals for notions of program distance in the style of logical relations and applicative bisimilarity. In doing so, we will focus on higher-order calculi exhibiting some form of computational effect, such as probabilistic choice and cost. In this context, the need for quantitative reasoning is even more urgent, but considerable technical difficulties tend to emerge.
  
  Short Bio: Ugo Dal Lago is full professor of Computer Science at the University of Bologna, since 2019 and a faculty member of the Computer Science Lab, since 2006. Before that, he has been a postdoc in Verona and Paris. He has been involved in many international research projects. Until recently, he was the principal investigator of the ERC CoG project "Differential Program Semantics". He co-authored more than 150 publications which appeared in journals and conference proceedings. He is the winner of the prize for the best Italian doctoral thesis in theoretical computer science (2006), of the Kleene Award (2006) and of the prize for the best young researcher in theoretical computer science (2015). He is member of the Academy of Sciences of Bologna Institute.



• July, 2, at 11:00: Gabriele Costa
  
  Location: online
  Title: Don't date the robots: the bad marriage between ML and Cybersecurity
  Abstract: Machine Learning is a family of powerful techniques that are revolutionizing our society in many ways. As a result, several activities that once were regarded as prerogatives of the human brain, can now be delegated to computers. Among these activities, those related to cybersecurity are also receiving attention. In many fields such as intrusion detection, malware analysis and even vulnerability assessment and penetration testing, researchers are experimenting whether ML-based systems can make the difference. Unfortunately, for the time being, the results seem to be extremely disappointing and, among many others areas, cybersecurity appears to be the most impermeable to ML. In this talk we will discuss the main reasons behind this phenomenon by also considering two case studies. In the first one, we will consider a classical network intrusion detection scenario, that of Web Application Firewalls (WAFs) and we will observe how well trained systems regularly fail against a not-so-smart adversary. The, we will focus on a more recent trend, i.e., Federated Learning, for understanding the impact of inadequate threat modeling. Finally, we will draw conclusions about the true potential of ML for cybersecurity and the recurring mistakes that we should avoid.
  
  Short Bio: Gabriele Costa is an Associate Professor in Computer Science at SySMA research unit of IMT School for Advanced Studies Lucca. His previous appointments include a position as Assistant Professor at the Department of Computer Science and System Engineering (DIBRIS) of the University of Genova and as researcher at the Institute of Informatics and Telematics (IIT) of the National Research Council of Italy (CNR). In 2016-17 he spent a period as a visiting researcher at the Information Security Group of ETH Zurich. He is co-founder of the Computer Security Laboratory (CSec Lab) of the University of Genova, co-founder and CRO of a SME, UNIGE spin-off, called Talos https://www.talos-sec.com/, and co-founder of the CTF team born2scan. His main research field is cybersecurity. In particular, his research interests include (but are not limited to) formal verification of software and systems, vulnerability detection mechanisms, attacker models and methodologies, security protocols, and innovative methods for effective security training. In 2020 Gabriele Costa collaborated in discovering two severe vulnerabilities in Rapid7 Metasploit Pro that went under CVE-2020-7354 and CVE-2020-7355.

• Chiara Bodei: chiara.bodei@unipi.it
• Lorenzo Ceragioli: lorenzo.ceragioli@unipi.it
• Gabriele Costa: gabriele.costa@imtlucca.it
• Pierpaolo Degano: pierpaolo.degano@unipi.it
• Gian-Luigi Ferrari: gian-luigi.ferrari@unipi.it
• Letterio Galletta: letterio.galletta@imtlucca.it