CAFEIN

This project addresses the formal verification of functional properties at specification level, for safety critical reactive systems. In particular, we focus on command and control systems interacting with a physical environment, specified using the synchronous language Lustre. The goals of the project are threefold. Improve level of automation of formal verification for such system, address properties of the hybrid system controled and focus on the numerical aspect of such programs implemented with floating-point numbers. Credible Autocoding and Verification of Embedded Software - CrAVES Partners: Georgia Tech - CMU