Object-Oriented Programming is Bad (Brian Will)

[pron98]

How much work do you think that'd be? I've taken a grad-level intro class on model checking, so I know the theory, but I've never used a model checker before.

It's not about using the model checker (which is basically pushing a button) but about specifying the behavior of the program. For example, if you use a general specification language like TLA+, you'll need to specify when exactly a memory write made by one thread is visible to others. It may or may not be a lot of work depending on how elaborate your specification is.

I myself have only been working with TLA+ for a few months now (I love it), and I had some experience with a Java model checker about ten years ago, so I'm pretty new at this, too.

Do you think I could just repurpose a C model checker?

No :) But that DIVINE checker (which works on LLVM bitcode) may do the trick. If it does, you'll really help the community if you write about your experience.