Loop Invariants: Learning to Help Teach (Abstract Only)

Loop invariants are a key component in developing code for verification, but many students struggle to grasp how to arrive at one that will remain true at the beginning and end of each iteration as well as be sufficiently strong to prove subsequent assertions reliant on the outcome of the loop. The focus of this research is to provide professors with a clearer idea of the difficulties students face in developing suitable loop invariants by using automated verification tools and collecting data in the background as students develop invariants in a series of isolated studies. This information will help professors to better allocate teaching time in order to best teach students the fundamentals of identifying correct loop invariants and developing verifiable code using tools.