Abstract Contract Synthesis and Verification in the Symbolic K Framework
Mostrar el registro sencillo del ítem
| dc.contributor.author | Alpuente Frasnedo, María
|
es_ES |
| dc.contributor.author | Pardo Pont, Daniel
|
es_ES |
| dc.contributor.author | Villanueva García, Alicia
|
es_ES |
| dc.date.accessioned | 2018-04-12T11:35:26Z | |
| dc.date.available | 2018-04-12T11:35:26Z | |
| dc.date.issued | 2018-04-12 | |
| dc.identifier.uri | http://hdl.handle.net/10251/100304 | |
| dc.description.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 structures and heap manipulation. Starting from the semantic definition of KernelC in the K semantic framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.1, which generates logical axioms that express pre- and postcondition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by K, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our framework with little effort. | es_ES |
| dc.description.sponsorship | 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 by FPU-ME grant FPU14/01830. | es_ES |
| dc.format.extent | 44 | es_ES |
| dc.language | Inglés | es_ES |
| dc.publisher | Universitat Politècnica de València | es_ES |
| dc.rights | Reconocimiento - No comercial - Compartir igual (by-nc-sa) | es_ES |
| dc.subject | Contract | es_ES |
| dc.subject | Inference | es_ES |
| dc.subject | Symbolic execution | es_ES |
| dc.subject | Abstract | es_ES |
| dc.subject | Subsumption | es_ES |
| dc.subject | Deductive | es_ES |
| dc.subject | Verification | es_ES |
| dc.subject | Contrato | es_ES |
| dc.subject | Inferencia | es_ES |
| dc.subject | Ejecución simbólica | es_ES |
| dc.subject | Subsunción | es_ES |
| dc.subject | Abstracta | es_ES |
| dc.subject | Deductiva | es_ES |
| dc.subject | Verificación | es_ES |
| dc.subject | Contracte | es_ES |
| dc.subject | Inferència | es_ES |
| dc.subject | Execució simbòlica | es_ES |
| dc.subject | Subsumpció | es_ES |
| dc.subject | Verificació | es_ES |
| dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
| dc.title | Abstract Contract Synthesis and Verification in the Symbolic K Framework | es_ES |
| dc.type | Informe | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/MECD//FPU14%2F01830/ES/FPU14%2F01830/ | es_ES |
| dc.rights.accessRights | Abierto | es_ES |
| dc.contributor.affiliation | Universitat Politècnica de València. Grupo de Extensiones de la Programación Lógica (ELP) | es_ES |
| dc.contributor.affiliation | Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació | es_ES |
| dc.description.bibliographicCitation | Alpuente Frasnedo, M.; Pardo Pont, D.; Villanueva García, A. (2018). Abstract Contract Synthesis and Verification in the Symbolic K Framework. Universitat Politècnica de València. http://hdl.handle.net/10251/100304 | es_ES |
| dc.type.version | info:eu-repo/semantics/submittedVersion | es_ES |
| dc.contributor.funder | European Regional Development Fund | es_ES |
| dc.contributor.funder | Ministerio de Economía y Competitividad | es_ES |
| dc.contributor.funder | Ministerio de Educación, Cultura y Deporte | es_ES |
| dc.contributor.funder | Generalitat Valenciana | es_ES |
Ficheros en el ítem
Este ítem aparece en la(s) siguiente(s) colección(ones)
-
Informes técnicos de investigación DSIC-ELP [15]
ELP: Extensiones de la Programación Lógica (Extensions of Logic Programming)