@inproceedings{Champion2016Kind2,
    abstract = {Kind 2 is an open-source, multi-engine, SMT-based model checker for safety properties of finite- and infinite-state synchronous reactive systems. It takes as input models written in an extension of the Lustre language that allows the specification of assume-guarantee-style contracts for system components. Kind 2 was implemented from scratch based on techniques used by its predecessor, the PKind model checker. This paper discusses a number of improvements over PKind in terms of invariant generation. It also introduces two main features: contract-based compositional reasoning and certificate generation.},
    author = {Adrien Champion and Alain Mebsout and Christoph Sticksel and Cesare Tinelli},
    booktitle = {28th International Conference on Computer Aided Verification, CAV2016},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {The Kind 2 Model Checker},
    year = {2016}
}