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, gu…