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

• April, 8, at 16:00: Giovanni Denaro
  Location: only online.
  Title: Exploiting Symbolic Analysis for Automatically Generating Test Cases
  Abstract:This seminar will introduce the use of symbolic analysis and dynamic symbolic execution for automatically generating test cases, highlighting recent applications for vulnerability detection. We will then delve into some of the challenges and research efforts undertaken by our team in extending classic techniques for testing heap-manipulating programs and mitigating the costs of constraint solving by reusing solutions across multiple constraints.
  Short Bio: Giovanni Denaro received his PhD in Computer Science and Engineering from Politecnico di Milano in 2002 and is currently an Associate Professor of Computer Science at the University of Milano-Bicocca. His research interests include software testing and analysis, formal methods for software verification and cybersecurity, blockchains, and software metrics. He has been investigator in several European and National projects and has developed projects in collaboration with leading universities and companies. He serves as Associate Editor for IEEE Transactions on Software Engineering and is regularly involved in the organization of major software engineering conferences.


• April, 15, at 16:00: Gianluigi Zavattaro
  Location: only online.
  Title: Reachability Analysis of Function-as-a-Service Scheduling Policies
  Abstract:Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. Reachability analysis of FaaS scheduling policies is fundamental to check relevant properties like the possibility for a safety critical function to be scheduled on an untrusted worker, or verifying whether one function operating on sensitive data can be co-located with a function developed by a third-party. We discuss the complexity of reachability analysis for the FaaS scheduling specification languages APP and aAPP, where the latter extends the former with the possibility to check, before allocating a function on a worker, the presence/absence of a given affine/anti-affine function on that worker. It turns out that reachability analysis has linear time complexity in APP, while the addition of affinity-awareness makes reachability PSPACE in aAPP.
  Short Bio: Gianluigi Zavattaro is a full professor in Computer Science at the Department of Computer Science and Engineering, University of Bologna, Italy. He is also member of the INRIA OLAS team, Sophia Antipolis, France. His main research interests include formal methods for concurrent and distributed programming languages with a specific focus on service-oriented and cloud computing.


• April, 29, at 16:00: Ezio Bartocci
  Location: only online.
  Title: Advancing Automatic Analysis of Probabilistic Loops
  Abstract:TProbabilistic programming is an emerging paradigm enabling software developers to model uncertainty of real data and to support suitable inference operations directly into computer programs. Probabilistic programs find applications in security/privacy, randomized algorithms, data prediction, generative and probabilistic machine learning and in modeling stochastic dynamical systems. A very challenging task is how to automatically analyze statically the behavior of probabilistic programs with loops that can generate a continuous and infinite-state space. We provide an overview of the main results of ProbInG, an interdisciplinary project between computer science and statistics that aims to develop novel techniques for automatically analysing the behavior of program random variables in probabilistic loops.
  Short Bio: Ezio Bartocci is a full professor for Formal Methods in Cyber-Physical Systems Engineering at TU Wien's Faculty of Computer Science, where he leads the Trustworthy Cyber-Physical Systems (TrustCPS) group and chairs the Doctoral College in Trustworthy Autonomous CPS. He earned a B.Sc. in Computer Science, an M.Sc. in Bioinformatics and (in 2009) a Ph.D. in Information Science & Complex Systems from the University of Camerino, Italy, followed by post-doctoral appointments at Stony Brook University (USA) before joining TU Wien in 2012 and being promoted to full professor in 2020. Bartocci’s research develops formal and runtime-verification methods - such as extensions of Signal Temporal Logic and lightweight monitoring frameworks - to guarantee safety, security and energy-efficiency in AI-enabled cyber-physical systems. Among several distinctions, his papers received the ETAPS 2022 Best Software Science Paper Award, Radhia Cousot Young Researcher Best Paper Award at SAS 2022 and the QEST 2022 Best Paper Award.


• May, 14, at 11:00: Paola Inverardi
  Location: Sala Gerace and online.
  Title: Exosoul: reconciling Human moral values with autonomous technology
  Abstract: We are increasingly surrounded by digital autonomous systems, powered by AI technologies. They operate on our behalf and interact and mediate interactions with us, the humans, thus raising concerns of ethical nature about their impact on the individual, social and economic sphere. Since a few years there has been a growing interest in understanding the ethical implication of the AI revolution. In this talk I focus on autonomous technologies and consider the perspective of a user, an individual interacting with ASs. The talk highlights the ethical threats that such interactions can pose on the individual values each one of us has. The talk then discusses how these same technologies can help us remaining humans in a digital world. Challenges and preliminary results conclude the talk.
  Short Bio: Rector of the Gran Sasso Science Institute (GSSI). Previously Rector of the University of L'Aquila where she also led the Software Engineering and Architecture Research Group. Paola Inverardi's main research area is in the application of rigorous methods to software production in order to improve software quality. In the last decade her research interests concentrated in the field of software architectures, mobile applications and adaptive systems. Inverardi serves in the editorial boards of the IEEE Transaction of Software Engineering, Springer Computing and Elsevier Computer Science Review. She has been general chair or program chair of leading conferences in software technology (i.e. ASE08, ICSE09, ESEC/FSE03). She is Chair of the ICSE Steering Committee, member of the ACM Europe Council and member of Academia Europea. She has received a Honorary Doctorate at Mälardalen University Sweden. Paola Inverardi received the prestigious 2013 IEEE TCSE Distinguished Service Award for outstanding and sustained contributions to software engineering community.


• May, 16, at 11:00: Marco Gori
  Location: Cappella Guinigi (IMT, Lucca). and online.
  Title: The Collectionless AI
  Abstract: AI is revolutionising not only the entire field of Computer Science, but nearly all fields of Science. However, while application contexts explode and LLMS display embarrassing cognitive qualities, the entire AI research field seems headed toward saturation of the fundamental ideas that have enabled today's spectacular results of large companies. Is the infamous "AI winter" perhaps creeping into the research field? In this talk, I argue that the time is ripe for a fundamental rethinking of AI methodologies to migrate intelligence from the cloud to the growing global population of devices with on-board CPUS. To support learning schemes inspired by mechanisms found in nature, I propose developing intelligent systems within the UnAIverse platform that enable social mechanisms and foster learning processes over time, without the need for data storage. A few insights are given on new foundations for learning over time within UnAIverse.
  Short Bio: Marco Gori received the Ph.D. degree in 1990 from University of Bologna, Italy, working partly at the School of Computer Science (McGill University, Montreal). He is currently full professor of computer science at the University of Siena, where he is leading the Siena Artificial Intelligence Lab. He is mostly interested in Machine Learning with emphasis on Neural Computation. The impact of his research on neural networks emerged mainly from the growing interest in Graph Neural Networks. He introduced the first ideas in the paper "A New Model for Learning in Graph Domains", by M. Gori, M. Monfardini and F. Scarselli (IJCNN2005) where the key-word Graph Neural Network was coined. A few years later, the most significant paper "Graph Neural Networks," IEEE-TNN, 2009 provided a more robust analysis and an accurate experimental evaluation. To date, the paper has received nearly 11,000 citations (about 6-7 citations/day in the last months). Professor Gori has been the chair of the Italian Chapter of the IEEE Computation Intelligence Society and the President of the Italian Association for Artificial Intelligence. He is a Fellow of IEEE, EurAI, IAPR, and ELLIS.


• May, 15, at 14:00: Carlo Furia
  Location: only online online.
  Title: Deductive Verification at the Level of JVM Bytecode
  Abstract: Automated deductive verification has made significant progress in recent years, but it still struggles to keep up with the fast evolution of modern programming languages. Take the example of Java: even state-of-the-art deductive Java verifiers such as KeY and OpenJML lack support for many features that have been part of the language since Java 8. To address these limitations, this talk presents ByteBack: an approach to Java deductive verification that works at the level of bytecode (instead of source code). By working at the level of bytecode, ByteBack supports recent versions of Java, and can even verify programs written in (subsets of) other JVM languages, such as imperative subsets of Scala and Kotlin.
  Short Bio: Carlo A. Furia is an associate professor in the Software Institute at the Università della Svizzera italiana. He has a PhD from the Politecnico di Milano; before joining USI he spent time as an associate professor at Chalmers University of Technology, and as a senior researcher at ETH Zurich. His main research interests are often at the intersection of software engineering and formal methods, with the ultimate goal of developing rigorous techniques and tools to analyze and improve the quality, correctness, and reliability of software (and software-intensive systems).


• May, 22, at 12:00: Rob van Glabbeek
  Location: Aula Seminari Est and online online.
  Title: Mutual Exclusion: verification and impossibilities
  Abstract: The mutual exclusion problem is one of the cornerstones of distributed computing. It deals with parallel processes that need to perform tasks that may not interfere with each other, such as updating records in a shared database. The sensitive parts of each process' code are collected in so-called critical sections, and the task of a mutual exclusion protocol is to make sure that two or more processes can never be in their critical section at the same time. Many mutual exclusion protocols have been proposed since this problem was posed in 1965, and it is generally believed that the mutual exclusion problem has been solved. Yet, whether a mutual exclusion protocol operates correctly depends on the hardware on which it will be running. Today I will formulate six alternative assumptions that one could make on the way the hardware implements shared registers, and check to what extent classical solutions to the mutual exclusion problem actually yield correct protocols under each of these assumptions. I report both on automated verification and on theoretical work. Regarding the latter, I will show that under the assumptions made in the original paper posing the mutual exclusion problem (namely, speed independence and atomicity), no correct mutual exclusion protocol is possible. This observation contradicts 50 years of research on mutual exclusion. I will also show how mutual exclusion can be achieved when dropping any of these assumptions. As for the automated verification, we employed a model checker to exhaustively analyse the state space of more than a dozen of the most popular mutual exclusion protocols, and automatically verify their correctness under each of the six hardware assumptions discussed. It turns out that several well-known algorithms do not live up to their promises: they have subtle flaws that never showed up during behavioural analysis, yet were found by our model checker.


• May, 22, at 15:00: Daniele Gorla
  Location: Aula Seminari Ovest and online: online.
  Title: Ensuring Properties of Smart Contracts by Typing
  Abstract: In this talk, I'll present TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. I'll start with a big-step operational semantics and use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, the two properties are actually incomparable. Nevertheless, I'll present a type system for noninterference and show that well-typed programs satisfy call integrity as well. Then, I'll extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. I'll then present a type system guaranteeing that well-typed programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker. This talk contains material from two papers, accepted at ECOOP'24 and at ISOLA'24. Both are joint work with Luca Aceto and Stian Lybech from Reykjavik University (Iceland)
  

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