The NBAC verification/slicing tool

Bertrand Jeannet

October 25, 2006

• Introduction
• NBAC Tutorial
• NBAC Reference Manual
• Verifying LUSTRE programs: lus2nbac
• Error diagnostic: nbac2lucky and lucky
• Analyzing AUTOC/AUTO (hybrid) automata: autoc2auto, auto2nbac, nbac2auto
• Examples
• Download
• References
• Footnotes