Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2099.1/26062

SMT-Based Methods for Difference Logic Invariant Generation
Candeago, Lorenzo
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Larrosa Bondia, Francisco Javier
We consider the problem of generating program invariants to prove safety, focusing on invariants that belong to difference logic (i.e., of the form x-y <= k). We present two new methods based on satisfiability modulo theories and constraint solving with promising experimental results.
Àrees temàtiques de la UPC::Matemàtiques i estadística::Lògica matemàtica
First-order logic
Invariant
lògica de diferències
satisfactibilitat mòdul teories
Invariant
difference logic
satisfiability modulo theories
Lògica de primer ordre
info:eu-repo/semantics/masterThesis
Universitat Politècnica de Catalunya
         

Mostrar el registro completo del ítem