Curriculum
Computer Science for Societal Challenges and Innovation, XL series
Grant sponsor
Università degli Studi di Padova
Supervisor

Paolo Baldan
Co-supervisor
s
to be defined
Contact
diletta.rigo@phd.unipd.it

Project description
Abstract model checking uses partitioning abstractions to tackle state space explosion; the goal of the project is to explore the possibility of approaching Model Checking as an instance of program verification to reuse the vast theory and toolset of Abstract Interpretation. In particular, we aim to exploit more general abstractions than partitioning ones, possibly automatically inferred by a procedure called Abstract Interpretation Repair that defines a counterexample-guided automated refinement of the abstraction driven by local completeness. The ultimate goal of the research is the application of this framework to Machine Learning models, in particular for the verification of fairness and robustness properties, namely of the capacity of a model to perform consistently well across different conditions, such as noisy inputs or perturbations in the data.