> ========================================================================================================= > OBIETTIVI FORMATIVI E RISULTATI DI APPRENDIMENTO ATTESI > I risultati di apprendimento attesi specificano conoscenze (teoriche) > e abilità (pratiche, metodologiche, applicate, ecc.) che lo studente > dovrà acquisire con il corso. Indicare quindi gli scopi specifici che > si prefigge il corso, dettagliando ciò che ci si attende lo studente > “conosca” e “sappia fare” al termine delle lezioni. > Dettaglio OBIETTIVI FORMATIVI E RISULTATI DI APPRENDIMENTO ATTESI I > risultati di apprendimento attesi specificano conoscenze (teoriche) e > abilità (pratiche, metodologiche, applicate, ecc.) che lo studente > dovrà acquisire con il corso. Indicare quindi gli scopi specifici che > si prefigge il corso, dettagliando ciò che ci si attende lo studente > “conosca” e “sappia fare” al termine delle lezioni. NOTA IMPORTANTE: Dall'AA 2024/25 il corso "Formal Methods" ha cambiato nome in "Automated Reasoning and Formal Verification". Il corso "Automated reasoning and Formal Verification" (precedentemente chiamato "Formal Methods") è diviso in due moduli consecutivi: Modulo I: "Automated Reasoning" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] Modulo II: "Formal Verification" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] che sono rispettivamente mutuati come singoli corsi * Automated Reasoning [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] * Formal Verification [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] dal c.d.l. in Artificial Intelligence Systems. Il primo modulo/corso costituisce prerequisito per il secondo. All'interno di entrambi i moduli/corsi è prevista una parte di laboratorio, per complessivi 3 CFU (1.5 CFU Automated Reasoning + 1.5 CFU Formal Verification) Il primo modulo/corso "Automated Reasoning" comincierà quindi all'inizio del semestre e terminerà a metà semestre, mentre il secondo modulo/corso "Formal Verification" comincierà a metà semestre e terminerà a fine semestre. Modulo/corso "Automated Reasoning" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] Le tecniche di ragionamento (logico) automatico sono ampiamente utilizzate in svariati campi, principalmente in Intelligenza Artificiale --come "motori" di svariati sistemi di ragionamento, inferenza e pianificazione automatica-- e nel campo della specifica e verifica formale si sistemi complessi --come "motori" sopra i quali sono costruiti i principali sistemi di verifica automatica. Il Modulo/corso "Automated Reasoning" presenta un'introduzione alle principali metodologie e agli strumenti per il ragionamento (logico) automatico. Gli studenti sperimenteranno in laboratorio l'uso di tool di automated reasoning, in particolare ad esempio, SAT o SMT solvers. Al termine del modulo/corso, lo studente: - conoscera` le principali tecniche di automated reasoning - sara` in grado di modellare semplici problemi e risolverli tramite automated reasonin tools, quali ad esempio SAT e SMT solvers. Modulo/corso "Formal Verification" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] I metodi di specifica e verifica formali sono progressivamente usati nello sviluppo di sistemi SW e HW industriali come potenti strumenti per la specifica, la verifica e la ricerca di errori. Le metodologie principali e di maggior successo cadono nella famiglia del "Formal Verification", che utilizzano tecniche di automated reasoning come motori. Il Modulo/corso "Formal Verification" presenta un'introduzione alle principali metodologie e agli strumenti per la specifica e soprattutto la verifica formale di sistemi SW e HW. Il corso si concentrera' sulle tecniche di verifica formale, ed in particolare sulla tecnica "Formal Verification". Gli studenti sperimenteranno in laboratorio l'uso di tecniche di model checking basate sui model checker NuXmv. Al termine del modulo/corso, lo studente: - conoscera` le principali tecniche di specifica e verifica formale, in particolare del Formal Verification - sara` in grado di formalizzare semplici sistemi SW o HW e verificarne proprieta`, tramite il model checker NuXmv. --------------------------------------------------------------------------- IMPORTANT NOTE: Starting from academic year 2024/25, the course "Formal Methods" has been renamed into "Automated Reasoning and Formal Verification". The course "Automated Reasoning and Formal Verification" (previously Formal Methods") is split into two consecutive modules: Module I: "Automated Reasoning" [6CFU, of which 4.5CFU theory + 1.5CFU lab] Module II: "Formal Verification" [6CFU, of which 4.5CFU theory + 1.5CFU lab] which are borrowed respectively as single courses * Automated Reasoning [6CFU, of which 4.5CFU theory + 1.5CFU lab] * Formal Verification [6CFU, of which 4.5CFU theory + 1.5CFU lab] from the degree course in Artificial Intelligence Systems. The first module/course is a prerequisite for the second. Part of both modules/courses consists on lab sessions, for 3CFU overall (1.5 CFU Automated Reasoning + 1.5 CFU Formal Verification) As such, the first module/course "Automated Reasoning" will start at the beginning of the semester and end in the middle of the semester, whereas the second module/course "Formal Verification" will start in the middle of the semester and terminate at the end of the semester. Module/course "Automated Reasoning" [6CFU, of which 4.5CFU theory + 1.5CFU lab] Automated (logical) reasoning techniques are widely used in many fields, mainly in Artificial Intelligence --as backend "engines" in several automated reasoning, inference and planning tools-- and in the field of formal specification and validation of complex systems --as backend "engines" on top of which automated-verification tools are build. Module/course "Automated Reasoning" introduces the main methodologies and instruments for automated (logical) reasoning. Students will experience in laboratory the usage of automated reasoning tools, in particular, e.g., of SAT and SMT solvers. At the end of the course, the student: - will know the main automated reasoning techniques - will be able to model simple problems and solved them via automated reasoning tools, like e.g. SAT or SMT solvers. Module/course "Formal Verification" [6CFU, of which 4.5CFU theory + 1.5CFU lab] Formal methods are increasingly used as powerful specification, verification and early debugging methods in the development of industrial SW and HW systems. This course provides an introduction to Formal Techniques and Tools for the specification and verification of Hardware and Software platforms. The main and most-successful fall in the "Formal Verification" family, which use automated-reasoning techniques as backend engines. Module/course "Formal Verification" introduces the main specification and formal verification techniques of SW and HW devices. The course will concentrate mainly on formal verification and techniques and, in particular, on Formal Verification (FV). A laboratory will be given in which the students will experience MC techniques by means of the MC NuXmv. At the end of the course, the student: - will know the main formal specification and verification techniques, in particular Formal Verification - will be able to formalize simple HW and SW systems and verify their properties by means of the model checker NuXmv. > ========================================================================================================= > PREREQUISITI > Indicare le specifiche conoscenze e/o abilità di base che lo studente > deve possedere prima di iniziare il corso > Dettaglio PREREQUISITI Indicare le specifiche conoscenze e/o abilità > di base che lo studente deve possedere prima di iniziare il corso Per entrambi i Moduli/Corsi "Automated Reasoning" e "Formal Verification": Si assume un minimo background nelle seguenti tematiche: - logica Booleana - algoritmi e strutture dati Un minimo background nelle seguenti tematiche potrà rivelarsi utile: - automi e linguaggi formali - logica del primo ordine --------------------------------------------------------------------------- For both modules/courses "Automated Reasoning" and "Formal Verification": It is assumed some basic background in the following topics: - Boolean logic - basic algorithms and data structures Some background in the following topics could be useful: - automata and formal languages - first-order logic > ========================================================================================================= > CONTENUTI/PROGRAMMA DEL CORSO > Indicare i principali contenuti del corso, nell’ordine temporale con > cui saranno trattati > Dettaglio CONTENUTI/PROGRAMMA DEL CORSO Indicare i principali > contenuti del corso, nell’ordine temporale con cui saranno trattati Per il Modulo/corso "Automated Reasoning" gli argomenti principali saranno (non necessariamente in ordine): Teoria: * Ragionamento Booleano E Soddisfacibilità Proposizionale (SAT) * Ordered Binary Decision Diagrams * Tecniche moderne di SAT Solving (CDCL) * Funzionalità Estese per SAT * Satisfacibilità Modulo Teorie (SMT) * Funzionalità Estese per SMT * Logiche temporali: LTL, CTL e CTL* * Modelli di Kripke e Model Checking (MC): Generalità * Ragionamento e Model Checking in logica temporale LTL Laboratorio: * Modellazione e risoluzione di problemi tramite SAT * Modellazione e risoluzione di problemi tramite SMT Per il Modulo/corso "Formal Verification" gli argomenti principali saranno (non necessariamente in ordine): Teoria: * Specifica formale e verifica formale * Rappresentazione Formale di Sistemi * CTL Model Checking * Symbolic MC vs. Explicit-State MC * Fair CTL MC e LTL MC * Astrazione in MC * MC per sistemi real-time e ibridi Laboratorio: * Modellazione e verifica di sistemi e proprietà con il model checker NuXmv NOTA: Dipendendo da varie circostanze, gli argomenti svolti possono subire variazioni. --------------------------------------------------------------------------- For Module/course "Automated Reasoning" the main topics presented in the course are (not necessarily in order): * Boolean Reasoning & Propositional Satisfiability (SAT) * Ordered Binary Decision Diagrams * Modern SAT Solving (CDCL) * Extended SAT Functionalities * Satisfiability Modulo Theories (SMT) * Extended SMT Functionalities * Temporal logics: LTL, CTL and CTL* * Kripke Models and Model Checking (MC): generalities * Reasoning and Model Checking in Linear Temporal Logic (LTL) Lab: * Modeling and problem solving via SAT * Modeling and problem solving via SMT For Module/course "Formal Verification" the main topics presented are (not necessarily in order): Theory: * Formal specification & formal validation * Formal Representation of Systems * CTL MC * Symbolic MC vs. Explicit-State MC * Fair CTL MC and LTL MC * SAT-based MC, * Abstraction in MC * MC with Timed and Hybrid Systems Lab: * Modeling and verification of systems & properties with the NuXmv model checker NOTE: Depending on various circumstances, the covered topics might be subject to variations. > ========================================================================================================= > METODI DIDATTICI UTILIZZATI E ATTIVITÀ DI APPRENDIMENTO RICHIESTE ALLO > STUDENTE > Indicare: > i metodi didattici e gli strumenti a supporto della didattica che > il docente adotterà per il raggiungimento dei risultati di > apprendimento attesi > le attività di apprendimento che saranno richieste allo studente > > Dettaglio METODI DIDATTICI UTILIZZATI E ATTIVITÀ DI APPRENDIMENTO > RICHIESTE ALLO STUDENTE Indicare: i metodi didattici e gli strumenti a > supporto della didattica che il docente adotterà per il raggiungimento > dei risultati di apprendimento attesile attività di apprendimento che > saranno richieste allo studente Per entrambi i Moduli/corsi "Automated Reasoning" e "Formal Verification": Teoria: Le lezioni saranno supportate da slide proiettate via computer, ed integrate da spiegazioni alla lavagna. Agli studenti verrà richiesta padronanza dei concetti teorici, logici ed algoritmici presentati nel corso, e la capacità di rispovere a mano semplici problemi. Laboratorio: Le esercitazioni saranno supportate da slide proiettate via computer, ed integrate da spiegazioni alla lavagna, ed avverranno in aula computer. Agli studenti verrà richiesto di saper modellare sistemi e proprietà nei linguaggi dimacs (SAT), SMT-LIB (SMT), NuXMV (MC), e saperne verificare la correttezza tramite rispettivamente un SAT solver, l'SMT solver MathSAT e il model checker NuXmv. --------------------------------------------------------------------------- For both modules/courses "Automated Reasoning" and "Formal Verification": Theory: The lectures will be supported by computer-projected slides, and integrated by explanations at the board. Students must acquire a deep understanding of the theoretical and algorithmic concepts presented in the course, and the capacity of solving by hand simple formal specification and verification problems. Lab: The lab sessions will be supported by computer-projected slides, and integrated by explanations at the board, and will be held in a computer lab. Student will be required to be able to model systems and properties in the Dimacs (SAT) SMT-LIB (SMT) and NuXMV (MC) languages, and to be able to verify their correctness via some SAT solver, the SMT solver MathSAT, and the NuXMV model checker respectively. > ========================================================================================================= > METODI DI ACCERTAMENTO E CRITERI DI VALUTAZIONE > Indicare: > i metodi di accertamento delle specifiche conoscenze/competenze > acquisite, cioè in cosa consiste la verifica del profitto (se si > tratta di esame scritto/orale, relazione/progetto, se previste > prove in itinere, …) > i criteri utilizzati per la valutazione e i pesi di ogni prova (se > previste prove multiple) > Dettaglio METODI DI ACCERTAMENTO E CRITERI DI VALUTAZIONE Indicare: i > metodi di accertamento delle specifiche conoscenze/competenze > acquisite, cioè in cosa consiste la verifica del profitto (se si > tratta di esame scritto/orale, relazione/progetto, se previste prove > in itinere, …)i criteri utilizzati per la valutazione e i pesi di ogni > prova (se previste prove multiple) Per chi sosterrà l'esame completo di "Automated Reasoning and Formal verification" (studenti c.d.s. "computer science" o studenti c.d.s "Artificial Intelligence Systems" che intendono sostenere entrambi i corsi in un unico esame) l'esame consistera' in tre prove: 1) un'esercitazione pratica al calcolatore in laboratorio, diretta ad indagare la capacita` dello studente di modellare e risolvere semplici problemi tramite un SAT/SMT solver e formalizzare semplici sistemi SW o HW e verificarne proprieta` tramite il model checkers NuXmv. 2) un test scritto, con un misto di domande a risposta multipla e brevi domande aperte, allo scopo di valutare la conoscenza delle principali tecniche del loro utilizzo. 3) una prova orale sulle tematiche del corso, allo scopo di valutare in dettaglio la conoscenza e padronanza delle tecniche di automated reasoning e specifica e verifica formale, nonche' delle loro motivazioni. Sara` valutata anche la capacita` di esprimere i concetti in modo logico-formale. Le tre parti sono indipendenti, e possono essere superate in appelli diversi, con il vincolo che la prova 3) non puo' essere svolta finche' le prove 1) e 2) non siano entrambe superate. E' necessario conseguire una votazione sufficiente (>= 18/30) in tutte e tre le prove. La votazione finale risultera' da una media pesata delle tre prove, con i seguenti pesi: 1) 20% 2) 30% 3) 50% Per chi vuol sostenere uno o entrambi i corsi singolarmente, per ciascun corso l'esame consistera' in due prove: 1) Un'esercitazione pratica al calcolatore in laboratorio, diretta ad indagare la capacita` dello studente di modellare e risolvere semplici problemi tramite un SAT/SMT solver [corso "Automated Reasoning"] e formalizzare semplici sistemi SW o HW e verificarne proprieta` tramite il model checkers NuXmv [corso "Formal Verification"]. 2) Un test scritto, con un misto di domande a risposta multipla e brevi domande aperte, allo scopo di valutare la conoscenza delle principali tecniche del loro utilizzo. Le due parti sono indipendenti, e possono essere superate in appelli diversi. E' necessario conseguire una votazione sufficiente (>= 18/30) in entrambe le prove. La votazione finale risultera' da una media pesata delle due prove, con i seguenti pesi: 1) 40% 2) 60% Non sono previste prove in itinere. Tutte le prove d'esame si terranno esclusivamente IN PRESENZA, non sono previsti prove d'esame in forma remota. L'unico modo di ottenere crediti da questo corsi è passare i rispettivi esami. Non e' prevista alcuna forma alternativa (ad esempio homework, progetti, ecc.) per ottenere crediti. NOTA: Dipendendo da varie circostanze, le modalità di esame possono subire variazioni, che eventualmente verranno comunicate agli studenti per tempo. --------------------------------------------------------------------------- For those who want to take the complete course exam "Automated Reasoning and Formal Verification" (students c.d.s. "Computer Science" and Students c.d.s "Artificial Intelligence Systems" willing to take both courses in one exam) the exam will consist in three parts: 1) a practical exercise session in computer laboratory, aimed at investigating the capability of the student to model and solve simple problems by means of SAT or SMT solvers, and to formalize simple HW and SW systems and to verify their properties by means of the model checker NuXmv. 2) a script test, with a mix of multiple-answer questions and brief open questions, aimed at evaluating the student knowledge on the main techniques and on their usage. 3) an oral interview on the topics of the course, aimed at evaluating in detail the student knowledge on the main automated reasoning and formal specification and verification techniques and their motivations. The capability of the student of expressing concepts in a formal-logical way will also be evaluated. The three parts are independent and can be passed in different sessions, with the constraint that one cannot try part 3) before passing parts 1) and 2). In order to pass the exam it is necessary to obtain a sufficient grade (>= 18/30) in every part. The final grade will be the weighted average of the grades of the three parts, with the following weights: 1) 20% 2) 30% 3) 50% For those who want to take one of both courses singularly, for each course the exam will consist in two parts: 1) a practical exercise session in computer laboratory, aimed at investigating the capability of the student to model and solve simple problems by means of SAT or SMT solvers ["Automated Reasoning" course], and to formalize simple HW and SW systems and to verify their properties by means of the model checker NuXmv ["Formal Verification" course]. 2) a script test, with a mix of multiple-answer questions and brief open questions, aimed at evaluating the student knowledge on the main techniques and on their usage. In order to pass the exam it is necessary to obtain a sufficient grade (>= 18/30) in every part. The final grade will be the weighted average of the grades of the two parts, with the following weights: 1) 40% 2) 60% Intermediate tests ("prove in itinere") are not envisaged. All exam parts will be taken solely IN PRESENCE, remote exam parts are not envisaged. The only way to obtain credit from this course(s) is passing the exam. No extra activities (e.g. projects, homeworks, ...) are envisaged. NOTE: Depending on various circumstances, the exam modalities might be subject to variations, which in case will be communicated to student in due time. > ========================================================================================================= > TESTI DI RIFERIMENTO/BIBLIOGRAFIA > Indicare i testi adottati per lo studio individuale e i materiali > bibliografici adottati > Dettaglio TESTI DI RIFERIMENTO/BIBLIOGRAFIA Indicare i testi adottati > per lo studio individuale e i materiali bibliografici adottati 1) appunti personali dello studente dalle lezioni 2) slides 3) manuali NuXmv e SAT/SMT solvers 4) per il modulo/corso "Automated Reasoning", verranno forniti link ad articoli e tutorials online per il modulo/corso "Formal Verification", uno dei seguenti libri: * Clarke, Grunberg, Long, "Model checking", MIT Press * Baier and Katoen "Principles of Model Checking", MIT Press --------------------------------------------------------------------------- 1) student's personal notes from the classes 2) slides 3) NuXmv e SAT/SMT solvers manuals 4) for the "Automated reasoning" module/course, links to publicly-available articles and tutorials will be provided For the "Formal Verification" module/course, one of the following books: * Clarke, Grunberg, Long, "Model checking", MIT Press * Baier and Katoen "Principles of Model Checking", MIT Press > ========================================================================================================= > ALTRE INFORMAZIONI Nessuna altra informazione. --------------------------------------------------------------------------- No other information.