Source code for SATABS

[mkschreder]

Where is the source code for the satabs model checker?

The website points to "svn co http://www.cprover.org/svn/satabs/releases/satabs-3.2" but this link is no longer working.

[martin-cs]

SATABS has not been maintained or updated in a very long time, see:

#6735 (comment)

for my summary of the state of things. I believe @tautschnig has a reasonably modern version (like 2016) and @kroening may have had the contents of that SVN server but I don't know if it was lost on him leaving Oxford.

HTH

[mkschreder]

SATABS has not been maintained or updated in a very long time, see:

#6735 (comment)

for my summary of the state of things. I believe @tautschnig has a reasonably modern version (like 2016) and @kroening may have had the contents of that SVN server but I don't know if it was lost on him leaving Oxford.

HTH

Thanks for clearing it up. I think it would be good to have the source code for satabs for reference so it doesn't get lost. You mentioned you still had a version from early 2010s. Can you post a git repo?

[martin-cs]

https://github.com/martin-cs/SATABS

I have put this together from a local check-out of revision 408. I've set things up so it compiles and runs. By the looks of it, the default configuration needs a copy of boom so it is probably not usable without a bit more code archaeology. Maybe the version of boppo it builds with can be made to work. If you want to go further I would suggest asking @tautschnig if he has a more recent checkout or, ideally, ask @kroening if he has (access to) the original subversion and can do this archiving job properly.

By all means fork, hack, whatever, the repo. If you are thinking of trying to update it to a modern CBMC version, be aware that it is likely a big job as there were quite a lot of changes between 4.7 and now. It may well be that it is less effort to rewrite it. I have a long running plan to add relational abstractions to goto-analyzer so it might be that the trunk version might be able to do something similar to the predicate abstraction step soon.