Update index.md with input from Dragana

Author: luigiapetre

content/post/tutorials/index.md

@@ -80,11 +80,11 @@ In this talk, I will present our work on automated grading of functional program
 
 - {{< spoiler text="Read more" >}} 
 
-The talk focuses on autograding programming assignments in the context of a large (about 400 students) second year undergraduate *Software Construction* course held at EPFL. Given the size of many courses nowadays, some automation for assignement verification needs to be used; unit testing is one candidate for verifying programming assignments. However, this sometimes proves inaccurate when some cases are missed out, in addition to the problem of ignoring the source code provided by the student and only considering the input/output relations. The latter issue leads to impersonal feedback that the student cannot learn much from. The solution discussed in this tutorial proposes to use formal methods (in particular program equivallence) in addition to unit testing, for verifying programming assignments written in a subset of the SCALA functional programming language.
+The talk focuses on autograding programming assignments in the context of a large (about 400 students) second year undergraduate *Software Construction* course held at EPFL. Given the size of many courses nowadays, some automation for assignement verification needs to be used; unit testing is one candidate for verifying programming assignments. However, this sometimes proves inaccurate when some cases are missed out, in addition to the problem of ignoring the source code provided by the student and only considering the input/output relations. The latter issue leads to impersonal feedback that the student cannot learn much from. The solution discussed in this tutorial proposes to use formal methods (in particular program equivalence) in addition to unit testing, for verifying programming assignments written in a subset of the SCALA functional programming language.
 
-Dr. Milovancevic and her colleagues implemented this solution in the context of a local automated grading system called *Stainless*, that is part of several programming courses at EPFL and works in principle based on pre- and post-conditions. However, this requires that some level of specification skills are needed. Instead, the solution discussed in the talk needs no such knowledge, only the source code the student provides: it then works as a push button approach. This is a remarkable usability improvement.
+Dr. Milovancevic and her colleagues implemented this solution in the context of a local automated grading system called *Stainless*, that is used in several courses at EPFL and works in principle based on pre- and post-conditions. However, this requires that some level of specification skills are needed. Instead, the solution discussed in the talk needs no such knowledge, only the source code the student provides: it then works as a push button approach. This is a remarkable usability improvement.
 
-The proposed solution returns a congratulatory message if the student's code is proved equivallent to the reference solution. It can also provide a counterexample when a wrong input is found as proof of the solution being incorrect. The student receives such feedback within minutes and can resubmit their code. Interestingly, when all solutions are in, the autograder generates for the teacher a set of clusters: one for the reference solution and all solutions equivallent to it, and as many other clusters as found for all the other solutions that are submitted. Some other correct solutions can be found, or incorrect solutions can be seen as equivallent to other incorrect solutions.
+The proposed solution returns a congratulatory message if the student's code is proved equivalent to the reference solution. It can also provide a counterexample when a wrong input is found as proof of the solution being incorrect. The student receives such feedback within minutes and can resubmit their code. Interestingly, when all solutions are in, the autograder generates for the teacher a set of clusters: one for the reference solution and all solutions equivalent to it, and as many other clusters as found for all the other solutions that are submitted. Some other correct solutions can be found, or incorrect solutions can be seen as equivalent to other incorrect solutions.
 
 This is the beauty of this proposal: code can be written in many ways that can be deemed acceptable and be verifiable. Even more, if many solutions have the same type of error, the teacher can address them systematically in the following lecture or even warn students against them the following year.