D for safety critical applications

[lagfra]

On Wednesday, 10 February 2021 at 17:01:19 UTC, welkam wrote:
> A talk about model checker Alloy. Its an introductory talk to 
> people with not prior knowledge
> "Finding bugs without running or even looking at code" by Jay 
> Parlar
> https://www.youtube.com/watch?v=FvNRlE4E9QQ

That's actually an interesting SAT-based mc, though I never had 
the occasion of trying it out. I like the fact that it is 
currenly under development, in my experience model checkers are 
"old" (most theoretical breaktroughs have been published in the 
1980s and still struggle to get a proper implementation). Plus, 
research is mostly supported by universities, which implies that 
development pace is often quite slow.

A model checker that has been widely adopted is NuSMV 
(https://nusmv.fbk.eu/), there's a very nice survey by K. Rozier 
from NASA Ames research center describing an example application 
of it 
https://www.researchgate.net/publication/222531608_Linear_Temporal_Logic_Symbolic_Model_Checking