Abstract :
In computer science and software engineering, formal methods are mathematically-based techniques for the specification, development and verification of software and hardware systems. They therefore establish the satisfaction of a specification by a system semantics. Abstract interpretation is a theory of sound approximation of mathematical structures, in particular those involved in the description of the behavior of computer systems. It allows the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model- checking, static analysis, program transformation and optimization, typing, software steganography, etc.). Its main current application is on the safety and security of complex hardware and software computer systems.
Keywords :
approximation theory; formal specification; program verification; security of data; abstract interpretation; computer science; formal methods; hardware systems; mathematical structures approximation; mathematically-based techiques; safety; security; software development; software engineering; software specification; software verification; Algorithm design and analysis; Application software; Computer science; Hardware; Optimization methods; Software algorithms; Software engineering; Software safety; Software systems; Steganography;