SPIN has long been used for similar stuff in academia and industry. They have pu... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

nickpsecurity on Jan 18, 2019 | parent | context | favorite | on: Introduction to TLA+ Model Checking in the Command...

SPIN has long been used for similar stuff in academia and industry. They have published a lot of their specs and results.

http://spinroot.com/spin/whatispin.html

http://www.imm.dtu.dk/~albl/promela.html

There were many projects using Pi Calculus, too. One of my project ideas is something that converts TLA+ to SPIN and Pi Calculus to use their tools and works. Or just otherwise integrates them.

Karrot_Kream on Jan 18, 2019 | [–]

Which model checkers use Pi Calculus? I've thought about learning Pi Calculus but an much less interested if there's no checker.

pron on Jan 18, 2019 | [–]

I don't think TLA+ is far too expressive to translate to Promela. There are, however, tools that translate subsets of TLA+ to ProB: https://www3.hhu.de/stups/prob/index.php/TLA

Consider applying for YC's Spring batch! Applications are open till Feb 11.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact