4 ms·
Ok I would love to know more about how the RTOS code was shrunk by 10x using TLA+ (at 8:28)
by mooneater 10y ago
Ok I would love to know more about how the RTOS code was shrunk by 10x using TLA+ (at 8:28)
- pron 10y agoWell, that book costs $99: http://www.springer.com/us/book/9781441997357 http://www.springer.com/us/book/9781441997357 But there's been more recent work done in TLA+ on another realtime OS, where the mechanical proof system, TLAPS, was used to prove some aspects of the kernel correct, and you can read about it for free here: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html