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) After Code Reformat #57

Closed janetlj closed 4 years ago

janetlj commented 4 years ago

Capability to generate all minimal inductive validity cores. This is intended to supersede a previous pull request (https://github.com/agacek/jkind/pull/54) as this one includes code reformat.

Main developers: Elaheh Ghassabani, Jaroslav Bendík, Mike Whalen. The theoretic part are based on the references below, for the offline algorithm [1] and the online algorithm [2]. The offline algorithm [1] is the default algorithm chosen in the setting to use.

[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.