6
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

LTL is really only useful for concurrency. So you want a problem from that space. I'd consider using spin. Its specification language (Promela) lets you express processes, shared variables, and message passing. You can write simple LTL properties as well. And then the actual spin tool lets you check that your code satisfies the properties. Students don't get bogged down in pen-and-paper proofs in a deduction system for LTL while you have a way to automatically grade submissions.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks for the suggestion! I couldn't find information about spin's CLI though, do you have any pointers? $\endgroup$
    – whoisit
    Mar 8 at 2:50
  • 2
    $\begingroup$ Try spin --help or if you have not installed it yet, check spinroot.com/spin/Man/Spin.html . $\endgroup$
    – Kai
    Mar 8 at 7:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.