<p>LTL is really only useful for concurrency. So you want a problem from that space. I'd consider using <a href="https://spinroot.com/spin/whatispin.html" rel="nofollow noreferrer">spin</a>. 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.</p>

CC BY-SA 4.0
2023-03-08T02:50:39.927Z
Thanks for the suggestion! I couldn't find information about spin's CLI though, do you have any pointers?
whoisit
CC BY-SA 4.0
2023-03-08T07:21:30.097Z
Try `spin --help` or if you have not installed it yet, check https://spinroot.com/spin/Man/Spin.html .
Kai
CC BY-SA 4.0
2023-03-07T21:58:56.610Z
2023-03-07T21:58:56.610Z
Kai
<p>I'm teaching a course on Intro to Theoretical CS, which is a compulsory course for CS majors. <br />
A pre-requisite is Math for CS and a co-requisite is Design of Algorithms.</p>
<p>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.</p>
<p>This is a large class, so I'd prefer if the assignment can be automatically graded.</p>
<p>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?</p>
<p>Any other ideas on how best to give students a hands-on experience with formal verification?</p>

<programming><lesson-ideas><assessment>
How to design an assignment on applications of Formal Verification?
# How to design an assignment on applications of Formal Verification?

(Asked by: username_0 on 2023-03-07)

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?

**Tags:** programming, lesson-ideas, assessment


---

## 1 answers

### Answer by username_1 on 2023-03-07. Score: 4

LTL is really only useful for concurrency. So you want a problem from that space. I'd consider using [spin](https://spinroot.com/spin/whatispin.html). 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.

> **Comments:**
> **username_0**: Thanks for the suggestion! I couldn't find information about spin's CLI though, do you have any pointers?  
> **username_1**: Try `spin --help` or if you have not installed it yet, check https://spinroot.com/spin/Man/Spin.html .  

---

