I'm teaching a course on Intro to Theoretical CS, which is a compulsory course for CS majors.
A pre-requisite is Math for CS and a co-requisite is Design of Algorithms.
In this course we also cover basics of formal verification - such as Linear Temporal Logic, and Proof systems like natural deduction. I'd like to show students some applications of formal verification, through a hands-on (programming) assignment where they can formally verify a simple software program.
This is a large class, so I'd prefer if the assignment can be automatically graded.
What tools are available which have a nice command line interface, and what programs would be simple enough so that students will easily be able to write specifications in LTL?
Any other ideas on how best to give students a hands-on experience with formal verification?