Principles of Abstract Interpretation
Lecturers: Roberto Bruni (UNIPI), Roberta Gori (UNIPI), Francesco Logozzo (Meta)
Schedule: February 20 (9am-11am), February 21 (2pm-4pm), February 22 (9am-11am and 2pm-4pm), February 24 (2pm-4pm), February 28 (4pm-6pm), March 1 (9am-11am), March 2 (4pm-6pm), March 3 (9am-11am and 2pm-4pm) – all in “sala seminari est”
Computer systems are pervasive in all aspects of modern societies, from healthcare and financing to entertainment and transportation. Inevitably, computer programs are riddled with inconvenient flaws that, at worst, may have extremely severe consequences. The ultimate objective of formal methods is to exploit the rigor mathematics and logics to verify the correctness and reliability of computer systems (both their software and hardware components) against some formal specification, possibly in a fully automatic way, using computers themselves.
Undecidability results poses a severe limitation: no computer can correctly answer with finite time and memory resources every question relative to the correctness of an arbitrary computer system. Therefore some compromises are necessary to provide answers in finite time on undecidable questions: automated theorem proving requires human guidance and assistance, which can involve tremendous efforts; model-checking must deal with memory explosion; static program analysis is often not precise enough to answer the desired questions. The principles of abstract interpretation establish the foundations of many formal verification methods, from their design to their applicability.
The course focuses on exact and approximate semantic property abstraction with applications in (semantics of) programming languages; design of deductive methods and static analysis techniques and their applications in an intensive software development context (Facebook). References: “Introduction to Static Analysis”, Xavier Rival and Kwangkeun Yi, MIT press, 2020 and “Principle of Abstract Interpretation”, Patrick Cousot, MIT press, 2021.
Computational Modeling for Systems Biology
Lecturers: Paolo Milazzo (UNIPI)
Schedule: March 21 and 22 from 10am to 1pm, March 23 from 2pm to 4pm, March 28 and 29 from 10am to 1pm, March 30 from 2pm to 4pm (all in room “sala seminari est”)
The course will deal with several aspects of the in-silico analysis of dynamical properties of biological systems. We will focus, in particular, on mechanistic modeling approaches aiming at creating executable representations of the biological mechanisms and processes underlying cell functioning. After providing a few notions of biochemistry and cell biology, we will examine modeling methods for gene regulatory networks with particular emphasis on Boolean network models and rule-based approaches. Next, we will present approaches suitable for the analysis of metabolic and cell-signaling processes, ranging from differential equations, to stochastic modeling and simulation methods, to hybrid approaches. Finally, we will briefly survey emerging methods in computational structural biology, such as methods for protein structure prediction, molecular docking and molecular dynamics simulation, and we discuss how these techniques could be integrated with the previous ones in order to evaluate the impact of mutations or synthetic proteins on cell functioning.
Pathways to Green ICT
Lecturers: Antonio Brogi (UNIPI), Stefano Forti (UNIPI)
Schedule: May 2, 3, 4, 5, 29, 30, 31 and June 1, 11am – 1pm, sala seminari ovest
As the world experiences environmental problems due to increasing carbon emissions, national and EU initiatives target the compelling need of our society to achieve sustainability goals. According to recent estimates, ICT systems produce 2% to 6% of the global carbon emissions throughout their lifecycle. On the other hand, ICT can contribute to reducing carbon emissions in other sectors (e.g. agriculture, building management, transportation) through digitalisation.
The course aims at introducing students to fundamentals of Green ICT, providing them with a toolbox to consider sustainability aspects in their research. The lectures will introduce:
- The concepts of sustainability and the types of environmental impact of the lifecycle of ICT systems (power consumption, carbon emissions, e-waste)
- Methodologies to assess the environmental impact of ICT systems (from production to operation and maintenance to disposal)
- Methodologies to decrease the environmental impact of ICT systems (orthogonality of QoS and environmental goals, hardware selection and PUE reduction, energy-aware programming, green software engineering, energy-aware system deployment)
- Use cases and open research challenges
Programming Tools and Techniques in the Pervasive Parallelism Era
Lecturers: Patrizio Dazzi (UNIPI), Marco Danelutto (UNIPI),
Schedule: May 15, 16, 18, 19; 22, 23, 24, 25 – from 11am to 1pm – in Sala Seminari Est
The course covers techniques and tools (already existing or that are in the process of being moved to mainstream) suitable to support the implementation of efficient parallel/distributed applications targeting small scale parallel systems as well as larger scale parallel and distributed systems, possibly equipped with different kind of accelerators. The course follows a methodological approach to provide a homogeneous overview of classical tools and techniques as well as of new tools and techniques specifically developed for new, emerging architectures and applicative domains. Perspectives in the direction of reconfigurable coprocessors and domain-specific architectures will also be covered.
Mixed Integer Non Linear Optimization: Methods and Applications
Lecturers: Claudia D’Ambrosio (CNRS and École Politechnique, France)
Schedule: June 12: 4pm-6pm, June 13, 14, 15: 9am-11am and 2pm-4pm, June 16: 9am-11am – in Sala Seminari Est
After a short refresher about mathematical optimization, linear optimization, and mixed integer linear optimization, the course will focus on the class of optimization problems called mixed integer non linear optimization (MINLO). This class of problems is one of the most general and real-world applications from a wide variety of fields can be modelled as MINLOs.
The lectures will cover:
- fundamentals of MINLO: what makes them challenging problems, why MILP methods cannot solve them, formulations, reformulations, relaxations, and restrictions
- convex MINLO: what characterizes them, how to recognize problems that are “evidently” convex MINLOs, main methods solving them exactly
- non convex MINLO: why methods for convex MINLOs cannot solve nonconvex ones exactly, global optimization, spatial branch-and-bound
- exploiting mathematical properties of special classes of MINLOs: the case of piecewise convex MINLOs. Formulations, their properties, strengthening through perspective reformulation.
In each lecture one or more real-world applications will be presented, e.g.:
- challenging problems in energy systems like the power production optimization and optimal power flow
- problems arising in finance like the robust portfolio optimization
- air traffic management problems like the tactical deconfliction, aimed at identifying and solving potential conflicts between pairs of aircraft whose trajectory traverses the same portion of the sky (applied to standard air transportation or urban air mobility)
- how to combine machine learning and MINLOs to solve the problem of algorithm configuration, aimed at optimizing the algorithm performance
In the practical sessions, an algebraic modelling language will be used, coupled with open-source or commercial solvers.
3D Geometry Representation and Processing for Deep Learning
Lecturers: Paolo Cignoni (CNR-ISTI), Massimiliano Corsini (CNR-ISTI), Daniela Giorgi (CNR-ISTI), Luigi Malomo (CNR-ISTI)
Period: October 2023
Schedule: October 11, 13, 18, 20: 9am-11am and 2pm-4pm – All classes will be held in Sala Seminari Est – but for the morning class of the 18th and for the afternoon class of the 20th, which will be held in Sala Seminari Ovest.
Computer Graphics and Geometry Processing are the main disciplines dealing with 3D data such as meshes and point clouds. In turn, Artificial Intelligence and Deep Learning are fundamental paradigms to manage visual data. Nevertheless, applying traditional learning paradigms on 3D data requires rethinking architectural building blocks designed for 2D images, such as convolution and pooling operators, as well as attention layers.
In this course, we will introduce different representations for 3D data, and basic geometry processing techniques that intervene in deep learning pipelines (sampling, remeshing, conversion, …). Then, we will introduce methods able to learn tasks on 3D data. We will describe different architectures to process complex geometric domains, and the novel mechanisms introduced in the literature to preserve by design their intrinsic properties. Examples include graph learning techniques, augmented with geometric and topological information; attention modules to process unordered point sets and mesh data; transformer-like architectures for unstructured data.
In the second part of the course, we will discuss different applications where the interplay between Computer Graphics/Geometry Processing and Deep Learning is opening up to exciting results, including Computational Fabrication, Architectural Geometry, Aesthetic analysis of 3D models, and Environmental Monitoring.