-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtoto.html
80 lines (43 loc) · 3.06 KB
/
toto.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
<html> <head>
<title>Educational resources
</title>
</head>
<body bgcolor="pink">
<font color="darkblue">
<body>
<h1>Educational resources</h1>
<h2>Dominique Méry, professor of
computer science</h2>
<h3>at University of Lorraine (Université de Lorraine)</h3>
<hr>
This site provides teaching resources for students taking courses at
the University of Lorraine, particularly the IT Masters and Telecom
Nancy.
<hr>
<hr>
<h2> Course MOSOS Modelling Software-based Systems using the Event-B modelling language</h2>
<p> The course Modelling Software-based Systems (MOSOS) is taught in
the Master in Computer Science of the University of Lorraine and in
the Master in Computer Engineering of Telecom Nancy.
</p>
<li>The lectures notes and documents for the students of Telecom
Nancy are at the link <a href="https://mery54.github.io/teaching/mosos" >MOSOS</a></li>
<h2> Course MVSI for french students (in french) </h2>
<p> Les élèves apprentis de seconde année
trouveront un ensemble de ressources pédagohiques comme les
textes des cours et des exercices ainsi que les solutions des
exercices en consultant ce lien <a href="https://mery54.github.io/teaching/mvsi" >MVSI</a> </p>
<h2>Using the Event-B modelling language for teaching verification
techniques </h2>
<p>
Verification of program properties such as partial correctness (PC) or absence of errors at runtime (RTE) applies induction principles using algorithmic techniques for checking statements in a logical framework such as classical logic or temporal logic. Alan Turing was undoubtedly the first to annotate programs, namely Turing machines, and to apply an induction principle to transition systems. Our work is placed in this perspective of verifying safety properties of sequential or distributed programs, with the aim of presenting them as simply as possible to student classes in the context of a posteriori verification. We report on an in vivo experiment using the \eb language and associated tools as an assembly and disassembly platform for correcting programs in a programming language. We revisit the properties of partial correctness and the absence of run-time errors in the context of this experiment, which precedes the use of \eb as a method of correct design by construction. We have adopted a contract-based approach to programming, which we are implementing with \eb. A few examples are given to illustrate this pedagogical approach. This step is part of a process of learning both the underlying techniques and other tools such as Frama-c, Dafny and Why3 \ldots, which are based on the same ideas.
</p>
<h2>Course ASPD on modelling, verifying and trying to udnerstand
distributed algorithms usd in main computer systems.
</h2>
You can get more information by visiting the folloxing <a
href="https://mery54.github.io/fmt" >link</a>.
<address>Dominique Méry, [email protected]</address>
<!-- hhmts start -->Last modified: Tue Nov 19 11:11:50 CET 2024 <!-- hhmts end -->
</body> </html>