Algebraic Formal Methods for Generating Invariants
Abstract
It is well-known that the automation and effectiveness of formal verification of software, embedded or hybrid systems depends to the ease with which precise invariants can be automatically generated from source code or specifications. In this thesis, we first reduce the invariant generation problem to linear algebraic problem in order to present new computational methods that can automate the discovery of non linear invariants, thereby circumventing difficulties met by other recent techniques. We provide the first methods which generate bases of non linear invariants, while dealing with complex programs and non linear hybrid embedded systems similar to those present today in many critical systems. These methods give rise to more efficient algorithms, with much lower computational complexities than the mathematical foundations of previous approaches know today. To the best of our knowledge, we present the first verifications methods that automatically generates bases of invariant expressed by transcendental functions. Finally, we extend the domain of applications for invariant generation methods to encompass security problems. More precisely, we provide an extensible invariant-based platform for analysis and detection of malware and the most virulent intrusions attacks.
