4 ms·

What are the pros/cons of Alloy over, say, Iris ?

• grayswandyr 5y ago
  I don't know Iris well but the logical setting and aims are completely different. Iris' primary application is proving safety properties of concurrent programs, with the possibility to express fine properties about memory thanks to separation logic. Alloy is a modeling language: there's no notion of program per se, just a logic. Then Iris relies on a very powerful logic so I guess a substantial amount of human intervention (Coq tactics) is needed to prove some property. Alloy is a so-called lightweight formal method (it trades power for efficiency if I may say so): analysis is fully automatic but limited to a bounded state space (the bound is given by the user). So Alloy is good at finding bugs in specifications, far less at proving things once and for all. Still, we found that it was very useful when doing full proofs (e.g. with the Event-B method) as its fast-bug-finding capabilities make it a very good tool to quickly evaluate an idea (before going full proof). Finally, on the language side, Alloy 6 can be used to specify safety and liveness properties.