문제가 w bothering
pow Spaß
orange
resto
a
Gdzie zakończyliśmy ostatni tygodnik?
To jest właściwie kilka slajdów wcześniej, więc pozwólcie mi dać 3-4 slajdów przypomnienia.
Najpierw zaczęliśmy z tych małych akcjomów
dla nowych, dynamicznych konstruktów programowania.
Czy wyszłyście do tego slajdu, które włożyłem w internet?
Podsumowałem paszport z jednym z z zespołów z zewnątrz.
Powiedział, że na niektórych slajdach paszport nie działa.
Pytali mnie, czy jest inny paszport.
Czy z was z zespołów ma jakieś problemy?
Czy ktoś próbuje je otworzyć?
Jest jedna slajda, która nie działa.
To był zespoł z ostatniej lektury?
To była ważna lektura.
Był to zespoł, który był zespołowywany przez błędne problemy.
To jest w tej lektury nieco złe.
Zobacz, co się stało w december 14.
Czy ktoś próbuje je otworzyć?
Czy ktoś próbuje je odwiedzić z ostatniej lektury?
To nie powinienem się zniszczyć z wskazówki.
Nie zaznaczam, że pamiętacie dokładnie co było w lekturze z ostatniej lektury.
Właśnie mam nadzieję, że pamiętacie, co to było z zespołami.
Co to było z zespołami magiczną.
I pamiętacie, że to była rucha w ramach.
Przede wszystkim, gdy przybyliśmy do ruchu w ramach,
próbowaliśmy najpierw zrozumieć, jeśli pamiętacie,
te programy i konstrukcje do impd
w temacie asmonaxium, co jest możliwe.
To znaczy, że postkondycje i postkondycje powinni mówić o najmocniejsziej możliwej części hip.
Najmocniejszym możliwym hip.
Tutaj i tutaj, jak pamiętacie, mówiliśmy nawet o mrocznych hipletach.
Tak więc, jedyną z zależnych informacji był o częściach w stanie,
o częściach, które złożyliśmy z normalnego impd.
I w tym samym, jedyną zależną informacją,
było to, co się stało z programem variable X.
Hiplet był zupełnie zależny.
Oczywiście nie musieliśmy się zrozumieć, że nic jest...
Przepraszam, nie powinnam powiedzieć, że jest zależne.
Nie musieliśmy...
Kompletnie nie zrozumieliśmy, co zostało złożone do tej pory.
I zobaczyliśmy...
Zaczęliśmy złożyć, w temacie sytuacji,
w której jeszcze nie ma pośrednich punktów.
A potem, używając ruchu w ramach, w następnym slajku,
przyjechaliśmy do jakiejś globalnej charakteryzacji,
która pozwoliła, żeby rzeczy się stały w częściach złożonych.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:25:17 Min
Aufnahmedatum
2017-01-25
Hochgeladen am
2019-04-11 14:09:02
Sprache
en-US
In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.
The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre- and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.
Students are going to acquire the following competences:
Wissen- Reproduce the definition of syntax and semantics of temporal logics LTL, CTL, and CTL*.
-
Reproduce the definition of semantics of a simple programming languages like IMP, with special focus on axiomatic semantics (Hoare rules).
-
Explain how CTL can be characterised in terms of fixpoints.
-
model checking
-
specification and verification of reactive systems,
-
verification of functional correctness or memory safety of simple programs.
- Choose the optimal tool for a given verification or specification problem.
-
Differentiate between safety and liveness properties.