coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FME Teaching Tutorial on January 26, 2024, 3pm CEST: Prof Alcino Cunha, University of Minho, Portugal: Teaching Alloy with Alloy4Fun

From: Luigia Petre <Luigia.Petre AT abo.fi>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] FME Teaching Tutorial on January 26, 2024, 3pm CEST: Prof Alcino Cunha, University of Minho, Portugal: Teaching Alloy with Alloy4Fun
Date: Fri, 19 Jan 2024 09:02:08 +0000
Accept-language: en-US, sv-FI
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Luigia.Petre AT abo.fi; spf=Pass smtp.mailfrom=Luigia.Petre AT abo.fi; spf=None smtp.helo=postmaster AT smtp-out.abo.fi
Dkim-filter: OpenDKIM Filter v2.11.0 smtp-out.abo.fi 7891B102114C
Ironport-data: A9a23:WWWMZak6m4caf6uYK9+bRezo5gzmI0RdPkR7XQ2eYbSJt1+Wr1Gzt xJJC2yFbKvYYmH8f48kPoXkoEoCuJ7Vx99qG1Rkrno8H1tH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayaj98B56r8ks14Kyr4WJA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN0+HENnZJIf/90rEDhk6 NokNx4DUTSq0rfeLLKTEoGAh+w4KdXzeYQCpjdpxzafA/dOrZLrGv6So4UDhnFq35oIQK62i 8kxMVKDaDzkfhxAO15RMJ8ihuqAj3P4NTNZwL6QjfNrvDWIlFwsiNABNvL6QNGQRJ0Ehn+U/ GP4+WujJhs6CNO2nG/tHnWEw7WncTnAcIkVDfiz8uNgqEaCw3QaThwQT1qy5/ej4nNSQPpEL lAMvy0zse47/kvtQNiVswCEnUNodyU0A7J4e9DWIinXokYNy1fEWjo3XXRaZcY4tcQ7YzUv2 xXb15nqHDFj+vndA36U6r7e/3v4NDk3PF0yQ3YObTIExN3//6A1rBbEFeh4HICP09baJDDXw hKxlhYYuYk9t8Aw+puewUHmmBOp/5jAcR407F7YX0Wj9QJIW7SmbI2Jt3ndy+pMDK+FRAK/5 FwBtcmU/b0LBKqsjw2Iev0GR5uy1saGMRrdoF9hJIYg/DKT4EyefZhczTV9BUVxOOMWUGXNT G6Kni0J/75VHn+hTZEvUrKLE85wkJTRT4X0ZM7bfv9lQ8ZXdjbe2ApMeETJ/WTmsHZ0oJEFI Z3BLPqdVycLO59GkgizafwWi4Iw5yYEwmjWe5D34jKn3ZeaZ1+XUb01C0SPXM9o8JK7pBjpz PgHO/uo0xl/VMjMUhvT+6MXLnEIKiEfLrLyoMp1aOWCA1RHHEcMNvzv+o4iKrdVx/ltquT1/ 3+GShB5znj7jib5MgmkUC1oR47uepddlkgFGxIQE2ym4FUZWrb33pwjL8M2WZIF6N1cyeVFS qhZWseYXdVKZDf12xUcSpjfrL1nJAmZgAGPGwGHYzEPWYFqaCKU293jfyrprDIvCAjuv+QAg rSQ7CHpartdeBZDVeH4MOmOyXG1tlgjwNNCZVPCeIRvSR+94bpUJDzUpd5pBcM1cDHo5CaQj iSSCjcm/dj9mZc/qoT1tPrVvrWSMrVMG2RBFDPm9pewDy7R+1SjzaJmUOqleTP8Vnv+yJ69Z Nd6nu3ND/kaoGlk64ZMMa5n7aYb1evdo7V3ygdFHnKSS3+JDrhmAGeN3OgRl6lr64JahzCLW RO0yoEHAYmKBcLrK05OBQwHau/Y6+oYtAOP5tsIIWL7xhRNwpy5bWtoMSOx1RNtdIlODNt9w MMKmtIn1Aikux97bveEln918kqPHFwhUoImlJErBd/2uA8oy3VpQ5/VOgnp6r6hNvRONUgLJ GePpazg3r5z+GvLQ0ARJ1Psg9VPpM0plkhR7VkgI1+ppIL0tsUv1kcMzQVtHxVn8BpX9slSZ E5pDhRRDoeT9W5KgMNjYTidKztZDkfExn2rmko7r0yHfUyGTWeXEXYcP9yK90Un825xWDhX0 bWb6WT9WwbRY8DD8XouaHFhtsDcY4R9xi/alOCjOva1LZ0wTD7mo62pPE4jiR/sB+Evj0zm+ 8hu2stNapPACC1BmJ1jVrGm1okRRi7ddSYGCbtk8bgSFG7RRCCq1HLcYwqtc8dKPLrR/VX+F 8VqIdlVWg+j0DqV6AoWHrMIP6Q+ictBCADuoV83DTVuX3qjQjtVXFb47S3inCosXskomMw6b I3QH95H/qp8mlMM81IhbuEdUoZ7XTXATAT226a78Y3l0rod5fp0fxhaPqSc5h2o3cgOw/5Ql ArJYOnYzoSODGiqc5TESs1+Oul/FT8/uClkPux+XxSioO4j6fvzij4=
Ironport-hdrordr: A9a23:k2JVmK201YSfgwNBVZI8BwqjBJwkLtp133Aq2lEZdPUMSL3gqy ncpoVi6faUskdsZJlD8errBEDkex7hHPFOkO4s1NuZPDUO21HYU72Kj7GSpQEIcheWnoUwus kAT0EUMqyTMbEOt7ef3ODOKadE/DDoytHKuQ6U9QYXcegjUdAb0+5WMHfnLnFL
Ironport-phdr: A9a23:8xG3DxZB8/Z7BdSG/RUk+hr/LTHD2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1g+PB9qKoKse16L/iOPJZy8p2dW7jDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgH c5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTajYr5+N gu6oAfVu8UZnIduNKk8wQbVr3VVfOhb2WxnKVWPkhjm4cu+4IBt+DlKtfI78M5AX6T6f6AmQ rFdET8rLWM76tD1uBfaVQeA6WcSXWsQkhpTHgjK9wr6UYvrsiv7reVyxi+XNtDrQL8uWDSi6 6BrSAL0iCoCKjU0/n3bhtB2galGpx2vugF/w5XMYI6LKPV+Yq3TfdQfRWVbX8ZRUTFKDoezY oYLCuYMO/tToYvgqFsUtRawBReiCv7zyjFGhXH23LE13Os6HA7cwAAgHcgDvGjIoNnoMqoZT OC7zLPPzTXGd/5Y3yr96InHchAgu/6HQKh+ftTNyUk1CQzOk1Kdp4r4PzOU2eQNsnKU4/B6W +2xl24nsR9+ryO1ycg3jYnFnIwVylHd+Ch/3Y06KsG2RlRhbt64DJtfqTuaN41uT84tR2xmt yQ3x6AYtZOnfCUH1YkqywDQZvKHcIWF4Q/uWPqRLzplh39rd66zihW8/0S+yuPxUsm53VdWo idGjtTBsG0G2RLU6siCUPR9/0Gh1C6A1wDS9uFEIV00mrHBJ54gxb48jpsSsUPEHi/zgkn2k bSWel0+9eez7OTreLvmpp6aOoRpiQ/+KrwjltGxDOgkKAQCQWaW9fqm2LH94EH1Xq9Gg/0qn qXBrZzXK9gXqrSnDwJbzIov8QuzAjao3dgCk3QKLUpJdA+JgoT1IV3CPv71Aemlj1ixkjpmx erKM7L9DpjLM3POjrPhfatm605A1gUz181R55NVC74fOP//Rkn8v8HCABAjKQy72ePnBc191 owAXWKPBbeUMLjXsV+U/uIjOu6MZJIJuDrnMfcq/PnugWU3mV8cZaWp3J0XZ26kHvl+PkmUb 2bgjs0fHWoEoAYyVvLmhECcXTJJZ3u+Q7ow5jQhB4KnCYfDSJqtgLuE3CqjGJNWe2FGCl+NE XjybYmKQekDaD6IIsB/iTELT6OuS4g72RGgtQ/207xnIfHM9S0CqZ3jzMR15/HUlRwq6DB4F 96d3H2VT2FogmMIQCc707x4oUxk01uMzax4g+FDGtFI/PNIUgI6NYbGwOBgCtDyXBjBftaTR 1q8TNWmG2J5ctVkidQJegN2H8iophHFxSujRbEP3fTfD5stt6nYwnLZJsBnyn+A2rN33Hc8R c4aEXCnia92vzDeG5TE2xG9iqeldK1a5CPR7mqrxGCJ+k9ZBl0jGZ7ZVGwSMxOF5e/y4VnPG uP/YVxGGg5IyMrYb7BPdsWsl1JNAvHqJNXZZWu13Wa2HxeBgL2WP8LxY2tI+iLbBQAflhwLu 26cPF0aGyauomuYNDFyD1/Haknrt+d/+zugVkFh9wiRdAV60qatvBschPiSUfQWi5YZuSggo nNMEUqn0vrfAd3GqQsyNL5Eb4Yb51FKnXncqxQ7PpGkKPV6gUUCdg1so070/w5yFp0FltU26 nogy0x8KMp0yXtncDWVldD1M7zTcCzp+Qy3LrTR0RfY2cqX/aEG7LI5rU/itUenDBhq9XIvy NRT33aGg/eCRAMPTZL8VFo2/BlmtvnbZCc6/YbdyXxrN+G9rDbD39sjAOZtxAynep9TN6aNF Qm6FMN/ZYDmDPErlFmgKCoJIPpf3Kc+OIWodrrO2aKmOvphgCPzlX5Os8h21kOB8TY5S/adh s1dhavDhE3dDm260Q/y16K/0ZpJbjwTAGelnC3tBYoLI7Z3YZ5OE2ClZcu+2tR5gZfpHX9e7 l+qQV0ci6rLMVKfaULw2QpI2AEZu3uizGGc0j17kjhvlqeDxiHmyu7lMhQGcD0uJiEqnRL3L I64gspPFmy1bgconV2d6FrgyoBSrqM5IWiZEg9YOiPxKW9lSK65sLGPNtVO5J0fuiJSSO2gY FqeR9YRujMi2jj4VytbzTE/LXSxv4nh2gZ9gySbJWpyq3zQfYdxww3e7ZrSX6wZ0j0DTSh+w T7ZYzr0d/20/NqVntH7v/ykWkqoXJoVfyijwY6btSS97HFnGlXmxKj1wIa9V1Jji2mmj5FjT m3QoQz5Y5X32qjfU6ovZURuCFLmqoJ7Fox4jooslcQV0HkeiI+S+ClPmmPyPNNHnKPmOSNWH XhRmISTulG/nhA7fRfrj8rjW36Qw9VsfYy/a2ISgGcm6txSTb2T5/pClDd0pVyxqUTQZ+J8l 3ET06hLijZSjucXtQ4q1ijYDKoVGBwSGTHtmBWBqeizsL9aTG+ldv6+1QAt+LLpRKHHuQxaV HvjL90GAC5/78w5CF/QynDb44vjPtfRJ4F21FXcg1LLiO5bL4g0n/wBiH98OG7zinYizvYyk R1k2Zzp9JjCMWhm+7i1RwJJLjCgLd1G4Snj1OwN+6Tel5DqBJhqHS8HGYflXe79WixHruzpb k6PCGFu8yzDX+CER0nFsRwg9iiXW5GzayPOfyFfl444AkPEfgoC2GV2FH0zzJs1H0Wt2dCnf E5l7zsc4EL1sF1Cy6ppMRL7T2vS9jCzcjlyRZ2WLR5b9AAE6UawU4TW7+R4GzxU88+6tALLL 2Wdax5JCWUAQlTCDFfmdri2uYuRrq7BWbf4dqKVJ+ze8KQJXvOMj/pDy6NA+DCBfoWKN3hmV bgg31ZbGGp+EILfkikOTCoek2TMadSarVGy4H8/qMf36/ntVA/1gOnHQ7JPLdVi/Qy3iqafJ qaRgih+MzNRypILwzfB1rEe2FcYjywmeSOqFPwMsivETaSYnaEybVZTcyRoKM5B9L4xxCFWP NLDz9ToyvhxhPlzBVYEHV3tl8e1ZNAbdmGwMFSUYSTDfL+CJDDN34T2efblEuUW1r4O8Ufp4 3DGSxyGXHzLjTTiWhGxPPsZiSiaOEYbo4ShalN3DmOlStv6axq9OdsxjDsswLRyiGmZUAxUe TV6bU5JqaWdqC1ChfAqUUhc73VkJK+8ljqD4sHRIJFQv/ohUUEW36pKpW83zbdY9nQOXPtuh C7btcJjuXm9l/WXjz16TFxHoDENioPB7iAAce3Js5JHX3jD5hcE626dXg8Lq9VSAdrqo6lMy 9LLmcobzR9L+dWS88pOX6A8x+qOOn1nPxu7QVY87SMeSCKzcGbCmwpUmvbU+HzH9vAH
Ironport-sdr: 65aa3a9b_0OvD0USIHj4AftAh607IoQykPIJnh8kCJL1PvOOGIVOQRI9 q68O4CHPlxdmtkWsof0MQ0JNI8DivnyGuO2HOTw==

Dear all,

The Formal Methods Teaching tutorials series starts in 2024 with a lecture on Friday, January 26!

Prof Alcino Cunha, University of Minho, Portugal will lecture on his experiences in teaching Alloy with Alloy4Fun on Friday, January 26, 2024 at 3 pm CEST. Alcino uses Alloy4Fun in teaching since 2019, and was one of the proponents of Alloy6 and Alloy4Fun. Here is a bit of context for Alloy4Fun, from https://haslab.github.io/Alloy4Fun/tutorial.html:

"Due to the simplicity and flexibility of the language and intuitive and automatic feedback provided by its analyzer, Alloy is often taught in introductory formal methods courses. However, the classic standalone Alloy Analyzer suffers from some limitations that hinder its usage in the classroom, namely

the lack of a straightforward mechanism to share simple Alloy models, instances and associated themes, a process that becomes cumbersome in large classes where students require feedback or have to submit exercise resolutions for evaluation; and
the absence of some automated assessment functionality or online judge system for students to autonomously solve exercises and receive automatic feedback regarding the correctness of their resolutions.

The Alloy4Fun platform was developed precisely to address these issues. Alloy4Fun allows users to edit and execute Alloy 6 models online, providing a minimalistic customizable instance visualizer. Both models and instances can be easily shared through permalinks. Moreover, the platform provides support for simple specification challenges in the form of duels where students attempt to discover a secret constraint specified by the instructors. When solving these challenges, students are supported by a hint system to nudge them in the right direction when stuck. Alloy4Fun collects anonymized information about the student submissions and interactions, so that instructors can measure the progress of the students on the shared challenges and identify potential learning bottlenecks."

More information about our lecturer can be found here: https://alcinocunha.github.io/.

The zoom link for Alcino's lecture is https://aboakademi.zoom.us/j/64254430116.

The event will last about an hour.

Warmly welcome!!

Best wishes,
Luigia

PS: for more info, here is the tutorial series webpage:
https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/.

__
Luigia Petre, Docent, PhD
Faculty of Science and Engineering
Åbo Akademi University, Finland
www.users.abo.fi/lpetre

[Coq-Club] FME Teaching Tutorial on January 26, 2024, 3pm CEST: Prof Alcino Cunha, University of Minho, Portugal: Teaching Alloy with Alloy4Fun, Luigia Petre, 01/19/2024