Combining Formal Analyses for the Study of Numerical Invariants
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

Number of scientific articles published: 0

Number of patents filed: 0

Number of product’s innovation: 0

Number of product’s innovation service: 0

Number of projected jobs created: 0

Number of jobs maintained: 0

Number of related companies creation: 0