Industrial applicability of advanced model/code-based V&V techniques for verifying program properties in embedded applications

International audienceThe constant and significant increase of computer power at low cost and many recent major technologicaladvances in program properties verification techniques show that designers and developers can now efficientlyand practically use proving techniques either at model or source code level.Those new V&V techniques convey major benefits to industrial sectors where software quality is at stake includingearly detection of errors (at specification, design and coding levels), and proof of absence of errors. Thosetechniques strengthen software application development process and minimize the likelihood of errors foundeither late or released in the field.The paper describes several advanced techniques for statically verifying dynamic properties of programsincluding logical, functional, run-time errors, how those techniques fit within current development processes andhow they may be used for monitoring software quality over time. The paper primarily applies to the developmentof embedded applications and demonstrates how the combined usage of techniques such as model-checking andabstract interpretation effectively handles industrial problems today