Book chapter
The Kind 2 Model Checker
Computer Aided Verification, pp.510-517
Lecture Notes in Computer Science, Springer International Publishing
07/13/2016
DOI: 10.1007/978-3-319-41540-6_29
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.
Details
- Title: Subtitle
- The Kind 2 Model Checker
- Creators
- Adrien Champion - The University of Iowa, Iowa City, USAAlain Mebsout - The University of Iowa, Iowa City, USAChristoph Sticksel - The University of Iowa, Iowa City, USACesare Tinelli - The University of Iowa, Iowa City, USA
- Resource Type
- Book chapter
- Publication Details
- Computer Aided Verification, pp.510-517
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-41540-6_29
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 07/13/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984002413302771
Metrics
22 Record Views