
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">

<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>

</head>

<body dir="ltr">

<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Helvetica, sans-serif, Helvetica, EmojiFont, "Apple Color Emoji", "Segoe UI Emoji", NotoColorEmoji, "Segoe UI Symbol", "Android Emoji", EmojiSymbols;">

<p><span id="ms-rterangepaste-start"></span></p>

<p style="font-family:Calibri,Helvetica,sans-serif,serif,EmojiFont; font-size:16px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Dear all,</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">We continue our Formal Methods Teaching tutorials series with a lecture on

</span><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Friday, May 29, at 3 pm CEST!</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Prof Peter Csaba lveczky has worked in Formal Methods especially in the areas

</span><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">of:</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">- formal specification and verification</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">- rewriting logic</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">- distributed and cyber-physical systems</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">- real-time and embedded systems</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">- executable formal semantics.</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">In education, Prof. lveczky is well known for promoting the integration of

</span><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">formal methods into mainstream computer science teaching. His work often

</span><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">combines rigorous theoretical foundations with practically executable models,

</span><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">helping students connect formal reasoning with realistic systems engineering

</span><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">problems.</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">His tutorial argues for the suitability of Maude in teaching: "Introducing Formal Methods for/and Distributed

 Systems Using Maude". The abstract follows below:</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px"><br>

</span></p>

<p style="font-family:Calibri,Helvetica,sans-serif,serif,EmojiFont; font-size:16px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">"<i>I have used rewriting logic and the Maude tool to introduce formal methods</i></span><i><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">for/and distributed systems to undergraduate students in Oslo for 20+ years.</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">In this talk I first argue that Maude should be a very good choice for</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">introducing formal modeling of distributed systems to undergraduate students:</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">The Maude formalism is intuitive, general, and expressive, and students tend</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">to like the functional-programming-style executable modeling in Maude.</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Furthermore, since it is fairly easy to model distributed systems in Maude,</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">students can quickly model and analyze central distributed systems, such as</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">distributed commit protocols, mutual exclusion algorithms, leader election</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">algorithms, and consensus algorithms, as well as transport protocols and</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">cryptographic protocols in such an introductory formal methods course. I then</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">give an overview of the course and its textbook Designing Reliable</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Distributed Systems, before concluding by summarizing student feedback and my</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

</i><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px"><i>own impressions about the course.</i>"</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">The event will last about an hour.</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Warmly welcome!!</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Best wishes,</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">Luigia</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">PS: for more info, here is the tutorial series webpage:</span><br style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">

<a href="https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/" target="_blank" rel="noopener noreferrer" style="font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/</a><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px">.</span></p>

<div><span style="color:rgb(33,33,33); font-family:wf_segoe-ui_normal,"Segoe UI","Segoe WP",Tahoma,Arial,sans-serif,serif,EmojiFont; font-size:13.3333px"><br>

</span></div>

<span id="ms-rterangepaste-end"></span><br>

<p></p>

<p><br>

</p>

<div id="Signature">

<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif,Helvetica,EmojiFont,"Apple Color Emoji","Segoe UI Emoji",NotoColorEmoji,"Segoe UI Symbol","Android Emoji",EmojiSymbols">

<p><span style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">__</span><br style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">

<span style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">Luigia Petre, Docent, PhD</span><br style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">

<span style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">Faculty of Science and Engineering</span><br style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">

<span style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">bo Akademi University, Finland</span><br style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">

<span style="font-family:Helvetica; font-size:12px; orphans:2; widows:2">www.users.abo.fi/lpetre</span><br>

</p>

</div>

</div>

</div>

</body>

</html>