| Entrambe le parti precedenti la revisione
Revisione precedente
|
|
magistraleinformatica:psc:start [20/04/2024 alle 10:14 (4 giorni fa)]
Roberto Bruni [Lectures (2nd part)] |
magistraleinformatica:psc:start [23/04/2024 alle 09:00 (23 ore fa)] (versione attuale)
Roberto Bruni [Lectures (2nd part)] |
| | 20 | Thu | 18/04 | 16:00-18:00 | X3 | Erlang erl:\\ //numbers, atoms, tuples, lists, terms, variables, term comparison, pattern matching, list comprehension, modules, functions, guards, higher order, recursion, pids, spawn, self, send, receive, examples//\\ \\ 17 - CCS:\\ //Syntax, operational semantics// | [[http://www.erlang.org/|Erlang]]\\ {{ :magistraleinformatica:psc:erl_2024.zip |erl session}}\\ {{ :magistraleinformatica:psc:2024-04-18_-_17a_-_ccs.pdf |Lecture 17a}} | | | 20 | Thu | 18/04 | 16:00-18:00 | X3 | Erlang erl:\\ //numbers, atoms, tuples, lists, terms, variables, term comparison, pattern matching, list comprehension, modules, functions, guards, higher order, recursion, pids, spawn, self, send, receive, examples//\\ \\ 17 - CCS:\\ //Syntax, operational semantics// | [[http://www.erlang.org/|Erlang]]\\ {{ :magistraleinformatica:psc:erl_2024.zip |erl session}}\\ {{ :magistraleinformatica:psc:2024-04-18_-_17a_-_ccs.pdf |Lecture 17a}} | |
| | 21 | Fri | 19/04 | 14:00-16:00 | C1 | 17 - CCS (ctd.):\\ //value passing, finitely branching processes, guarded processes//\\ \\ 18 - Bisimulation:\\ //abstract semantics, graph isomorphism, trace equivalence, bisimulation game, strong bisimulation// | {{ :magistraleinformatica:psc:2024-04-18_-_17a_-_ccs.pdf |Lecture 17a}}\\ {{ :magistraleinformatica:psc:2024-04-19_-_17b_-_ccs_guarded.pdf |Lecture 17b}}\\ {{ :magistraleinformatica:psc:2024-04-19_-_18a_-_ccs_abstract.pdf |Lecture 18a}}\\ {{ :magistraleinformatica:psc:2024-04-19_-_18b_-_ccs_bisimulation.pdf |Lecture 18b}} | | | 21 | Fri | 19/04 | 14:00-16:00 | C1 | 17 - CCS (ctd.):\\ //value passing, finitely branching processes, guarded processes//\\ \\ 18 - Bisimulation:\\ //abstract semantics, graph isomorphism, trace equivalence, bisimulation game, strong bisimulation// | {{ :magistraleinformatica:psc:2024-04-18_-_17a_-_ccs.pdf |Lecture 17a}}\\ {{ :magistraleinformatica:psc:2024-04-19_-_17b_-_ccs_guarded.pdf |Lecture 17b}}\\ {{ :magistraleinformatica:psc:2024-04-19_-_18a_-_ccs_abstract.pdf |Lecture 18a}}\\ {{ :magistraleinformatica:psc:2024-04-19_-_18b_-_ccs_bisimulation.pdf |Lecture 18b}} | |
| | 22 | | | | | 18 - Bisimulation (ctd.):\\ //strong bisimilarity, strong bisimilarity is an equivalence, strong bisimilarity is a bisimulation, strong bisimilarity is the coarsest strong bisimulation, strong bisimilarity is a congruence, some laws for strong bisimilarity, strong bisimilarity as a fixpoint, Phi operator, Phi is monotone, Phi is continuous (on finitely branching processes), Knaster-Tarski's fixpoint theorem// | {{ :magistraleinformatica:psc:2024-04-19_-_18b_-_ccs_bisimulation.pdf |Lecture 18b}}\\ Lecture 18c | | | 22 | Tue | 23/04 | 16:00-18:00 | C1 | 18 - Bisimulation (ctd.):\\ //strong bisimilarity, strong bisimilarity is an equivalence, strong bisimilarity is a bisimulation, strong bisimilarity is the coarsest strong bisimulation, strong bisimilarity is a congruence, some laws for strong bisimilarity, strong bisimilarity as a fixpoint, Phi operator, Phi is monotone, Phi is continuous (on finitely branching processes), Knaster-Tarski's fixpoint theorem// | {{ :magistraleinformatica:psc:2024-04-19_-_18b_-_ccs_bisimulation.pdf |Lecture 18b}}\\ Lecture 18c | |
| | 23 | | | | | 19 - Hennessy-Milner logic:\\ //modalities, HML syntax, formula satisfaction, converse of a formula, HML equivalence//\\ \\ 20 - Weak Semantics:\\ //weak transitions, weak bisimulation, weak bisimilarity, weak bisimilarity is not a congruence, weak observational congruence, Milner's tau-laws//\\ \\ 21 - CCS at work:\\ //modelling imperative programs with CCS, playing with CCS (using CAAL)// | Lecture 19\\ Lecture 20 | | | 23 | Fri | 26/04 | 14:00-16:00 | C1 | 19 - Hennessy-Milner logic:\\ //modalities, HML syntax, formula satisfaction, converse of a formula, HML equivalence//\\ \\ 20 - Weak Semantics:\\ //weak transitions, weak bisimulation, weak bisimilarity, weak bisimilarity is not a congruence, weak observational congruence, Milner's tau-laws//\\ \\ 21 - CCS at work:\\ //modelling imperative programs with CCS, playing with CCS (using CAAL)// | Lecture 19\\ Lecture 20 | |
| | 24 | | | | | 21 - CCS at work (ctd.):\\ //modelling imperative programs with CCS, playing with CCS (using CAAL), modelling and verification of mutual exclusion algorithms with CCS and CAAL//\\ \\ CAAL session (copy the text and paste it in the Edit panel) | Lecture 21\\ [[http://caal.cs.aau.dk/|CAAL]]\\ CAAL session | | | 24 | Tue | 30/04 | 16:00-18:00 | C1 | 21 - CCS at work (ctd.):\\ //modelling imperative programs with CCS, playing with CCS (using CAAL), modelling and verification of mutual exclusion algorithms with CCS and CAAL//\\ \\ CAAL session (copy the text and paste it in the Edit panel) | Lecture 21\\ [[http://caal.cs.aau.dk/|CAAL]]\\ CAAL session | |
| | 25 | | | | | Exercises:\\ //Erlang, CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | Exercises 06\\ Lecture 22a | | | 25 | Thu | 02/05 | 16:00-18:00 | X3 | Exercises:\\ //Erlang, CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | Exercises 06\\ Lecture 22a | |
| | 26 | | | | | 22 - Temporal and modal logics (ctd.):\\ //computational tree logic (CTL* and CTL), infinite trees, infinite paths, branching structure, CTL* satisfaction, equivalence of formulas, CTL formulas, expressiveness comparison, mu-calculus, positive normal form, least and greatest fixpoints, invariant properties, possibly properties, mu-calculus with labels// | Lecture 22a\\ Lecture 22b | | | 26 | Fri | 03/05 | 14:00-16:00 | C1 | 22 - Temporal and modal logics (ctd.):\\ //computational tree logic (CTL* and CTL), infinite trees, infinite paths, branching structure, CTL* satisfaction, equivalence of formulas, CTL formulas, expressiveness comparison, mu-calculus, positive normal form, least and greatest fixpoints, invariant properties, possibly properties, mu-calculus with labels// | Lecture 22a\\ Lecture 22b | |
| | 27 | | | | | 23 - GoogleGo:\\ //an overview//\\ \\ GoogleGo playground:\\ Go principles, variable declaration, type conversion, multiple assignments, type inference, imports, packages and public names, named return values, naked return, multiple results, conditionals and loops, pointers, struct, receiver arguments and methods, interfaces, goroutines, bidirectional channels, channel types, send, receive, asynchronous communication with buffering, close, select, communicating communication means, range, handling multiple senders, concurrent prime sieve | Lecture 23\\ [[http://golang.org/|Google Go]]\\ go session | | | 27 | | | | | 23 - GoogleGo:\\ //an overview//\\ \\ GoogleGo playground:\\ Go principles, variable declaration, type conversion, multiple assignments, type inference, imports, packages and public names, named return values, naked return, multiple results, conditionals and loops, pointers, struct, receiver arguments and methods, interfaces, goroutines, bidirectional channels, channel types, send, receive, asynchronous communication with buffering, close, select, communicating communication means, range, handling multiple senders, concurrent prime sieve | Lecture 23\\ [[http://golang.org/|Google Go]]\\ go session | |
| | 28 | | | | | 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | Lecture 24 | | | 28 | | | | | 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | Lecture 24 | |
