Finding inductive invariants using satisfiability modulo theories and convex optimization

L'analyse statique correcte d'un programme consiste à obtenir des propriétés vraies de toute exécution de ce programme. Celles-ci sont utiles pour démontrer des caractéristiques appréciables du logiciel, telles que l'absence de dépassement de capacité ou autre erreur à l'exécutio...

Full description

Bibliographic Details
Main Author: Karpenkov, George Egor
Other Authors: Grenoble Alpes
Language:en
Published: 2017
Subjects:
SMT
Smt
004
Online Access:http://www.theses.fr/2017GREAM015/document