PlusCal in Alloy

I have used Huth & Ryan in our Logic in Computer Science course at Iowa and I think it is an excellent introductory text.

A more specialized one that I found pretty good and would recommend for an introduction to LTL is

Software Reliability Methods by Doron Peled
https://link.springer.com/book/10.1007/978-1-4757-3540-6

I should note that both books are out of date with respect to the state of the art in automated reasoning/verification. They are perhaps more useful as references on the foundations.

Cesare

1 Like

Hmm. It is a bit scary to realize all these books are long out of print.

Then again, maybe it is time for the formal methods renaissance with Alloy! :slight_smile:

Hmm. It is a bit scary to realize all these books are long out of print.

There are several other books on FMs which are in print but they are more technical.

I suggested Huth&Ryan and Peled because the temporal logic chapters there are pretty accessible, as they are meant to be undergraduate textbooks. And while they may be out of print, they are still available in electronic format :slightly_smiling_face:

Cesare

My concern is more that this area seems to not moving into interesting commercial waters. Ah, well, story of my life :slight_smile:

This sounds like an interesting experiment – did anything come of it?

Well, it did work. But I did not find anybody remotely interested to further it. So I figured it was one of those things my kids told me the world wasn’t like me …