4 ms·
Interesting material. Thanks for sharing! Maybe a dumb thought: is SAT solver good for verifying concurrent system design? (e.g. locks, distributed systems, et
by oldgun 7y ago
Interesting material. Thanks for sharing!
Maybe a dumb thought: is SAT solver good for verifying concurrent system design? (e.g. locks, distributed systems, etc.) Or are systems like TLA+ a must for these cases?
- hwayne 7y agoSadly I don't think it's possible to represent an infinite trace as a SAT problem, so you can't check any liveness properties (will a good thing eventually happen) unless you use something more powerful. Promela/Spin and TLA+/TLC use model checkers, TLA+/TLAPS and B/Rodin use theorem provers, Electrum uses an SMT solver.
- oldgun 7y agoThanks!