News for hackers. Stuff that matters.

A comment on TLA+ model checking made symbolic. Parent comment

Re:TLA+ model checking made symbolic by cmarinas on Friday November 29, 2019 @10:38AM (#21664951)
I used it in the context of Linux kernel development to model/verify various algorithms. I gave a presentation last year at Linux Plumbers:

http://procode.org/FormalMethodsPlumbers2018.pdf

Slides 4 and 28 list actual bugs found by such modelling.

I do find TLA+ (or formal modelling in general) pretty useful for real world cases, only that, unfortunately, I don't always have the time.

[ Parent | on HN ]
Re:TLA+ model checking made symbolic by QuinnWilton on Friday November 29, 2019 @02:46PM (#21666383)
This presentation is exactly the sort of thing I'm interested in, thank you!
[ Parent | on HN ]