Inductive validity cores

Merit and Blame Assignment with Kind 2

Daniel Larraz, Mickaƫl Laurent & Cesare Tinelli
We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models.