Update index.md refined in form

Author: luigiapetre

content/post/tutorials/index.md

@@ -66,9 +66,13 @@ Here are the details of the scheduled Zoom meeting:
 
 - {{< spoiler text="Read more" >}} 
 
-In his tutorial, Dr. Carvalho presents his perspective on teaching Formal Methods as a rigorous reinterpretation of Software Engineering, moving stepwise from abstract specifications all the way to actual implementations. This approach - based on his more-than-a-decade-long experience with the topic - is backed by a recent [paper](https://dl.acm.org/doi/10.1145/3702231) surveying the role of Formal Methods in Computer Science (CS) education and claiming that "... every computer scientist needs to know Formal Methods..., since the skills and knowledge acquired ... provide the indispensable solid foundation that forms the backbone of CS practice.". To that end, Gustavo takes the students from specifications to automatic code generation, with intermediate correctness proofs, animation techniques and visualisation methods. 
+In his tutorial, Dr. Carvalho presents his perspective on teaching Formal Methods as a rigorous reinterpretation of Software Engineering, moving stepwise from abstract specifications all the way to actual implementations. This approach - based on his more-than-a-decade-long experience with the topic - is backed by a recent [paper](https://dl.acm.org/doi/10.1145/3702231) surveying the role of Formal Methods in Computer Science (CS) education and claiming that 
 
-Initially, he taught a combination of Z and CSP# due to the local curriculum requirement on concurrency. Despite engaging the students with several software platforms (PAT for CSP# concurrent models verification, CZT for typing Z schemas/programs and Z-Eves for proving), the feedback pointed out the weakness of Z-related tools, in addition to the loose connection between the two formalisms. Building on this initial phase, Gustavo continued with teaching a combination of Event-B and CSP~M~, attracting positive feedback on the Event-B related software tools, such as Rodin, ProB and B Motion Studio. The last and current phase consists in teaching only B, due to several developments: the possibility to drop the mandatory concurrency requirement and the recent availability of a B Massive Open Online Course (MOOC). The latter development allowed for changing from a classical teaching format to a flipped classroom, where students are required to follow the MOOC course and then implement in a laboratory the various exercises and projects, with teacher support. The feedback from students changed to an appreciation of the employed software tools (Atelier-B, ProB, B Motion Web and VS Code) together with the integrated nature of the course, since some of the projects involve code generation in C with embedding in various platforms of interest for students.
+>... every computer scientist needs to know Formal Methods..., since the skills and knowledge acquired ... provide the indispensable solid foundation that forms the backbone of CS practice
+
+To that end, Gustavo takes the students from specifications to automatic code generation, with intermediate correctness proofs, animation techniques and visualisation methods. 
+
+Initially, he taught a combination of Z and CSP# due to the local curriculum requirement on concurrency. Despite engaging the students with several software platforms (PAT for CSP# concurrent models verification, CZT for typing Z schemas/programs and Z-Eves for proving), the feedback pointed out the weakness of Z-related tools, in addition to the loose connection between the two formalisms. Building on this initial phase, Gustavo continued with teaching a combination of Event-B and CSP<sub>M</sub>, attracting positive feedback on the Event-B related software tools, such as Rodin, ProB and B Motion Studio. The last and current phase consists in teaching only B, due to several developments: the possibility to drop the mandatory concurrency requirement and the recent availability of a B Massive Open Online Course (MOOC). The latter development allowed for changing from a classical teaching format to a flipped classroom, where students are required to follow the MOOC course and then implement in a laboratory the various exercises and projects, with teacher support. The feedback from students changed to an appreciation of the employed software tools (Atelier-B, ProB, B Motion Web and VS Code) together with the integrated nature of the course, since some of the projects involve code generation in C with embedding in various platforms of interest for students.
 
 The volume of the presented courses ranges to about 25 students, which is rather impressive, considering the volume of the particular student intakes (50 students starting every semester), the advanced nature of the modules hosting the courses, as well as the optional quality of the course in the most recent curriculum.