- -

Abstract Contract Synthesis and Verification in the Symbolic K Framework

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Abstract Contract Synthesis and Verification in the Symbolic K Framework

Show full item record

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/100304

Files in this item

Item Metadata

Title: Abstract Contract Synthesis and Verification in the Symbolic K Framework
Author:
UPV Unit: Universitat Politècnica de València. Grupo de Extensiones de la Programación Lógica (ELP)
Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Issued date:
Abstract:
[EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based ...[+]
Subjects: Contract , Inference , Symbolic execution , Abstract , Subsumption , Deductive , Verification , Contrato , Inferencia , Ejecución simbólica , Subsunción , Abstracta , Deductiva , Verificación , Contracte , Inferència , Execució simbòlica , Subsumpció , Verificació
Copyrigths: Reconocimiento - No comercial - Compartir igual (by-nc-sa)
Thanks:
This work has been partially supported by the EU (FEDER) and Spanish MINECO under grant TIN2015-69175-C4-1-R, and and TIN2013-45732-C4-1-P, and by Generalitat Valenciana PROMETEOII/2015/013. Daniel Pardo was supported ...[+]
Type: Informe

This item appears in the following Collection(s)

Show full item record