Next Craig Interpolant Prover (NCIP)

NCIP is a Bounded Model Checker (BMC) for solving formal problems in various input formats (AIGER / CNF). Using Craig interpolants it is able to prove unreachability for some formal problems that can be validated via generated unreachability certificates.

Visibility
Publicly available!
ISA Compliance
Status
Date of Availability
Contact

Universität Freiburg
Tobias Faller
Georges-Köhler-Allee 051
79106 Freiburg
Deutschland

Contact Email
fallert [at] informatik.uni-freiburg.de
Target TRL at the end of phase 1
TRL4: Versuchsaufbau im Labor --> Plattform mit Parametrisierung
Target TRL at the end of phase 2
TRL6: Prototyp in vereinfachter/simulierter Einsatzumgebung --> Anwendungsfälle
Component is required for safety critical systems
Nein
Category
Software-Based Self-Test (SBST)