loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Generate All Minimal Inductive Validity Cores (MIVCs) #54

Closed janetlj closed 2 years ago

janetlj commented 4 years ago

Capability to generate all minimal inductive validity cores. Main developers: Elaheh Ghassabani and Jaroslav Bendík. The theoretic part are based on the references below, for the offline algorithm [1] and the online algorithm [2].

[1] E. Ghassabani, M. W. Whalen, and A. Gacek. Efficient generation of all minimal inductive validity cores. 2017 Formal Methods in Computer Aided Design (FMCAD), pages 31–38, 2017. [2] J. Bendík, E. Ghassabani, M. Whalen, and I. Černá. Online enumeration of all minimal inductive validity cores. In International Conference on Software Engineering and Formal Methods, pages 189–204. Springer, 2018.

lgwagner commented 2 years ago

Closing this. It's dead.