Mostrar el registro sencillo del ítem
dc.contributor.author
Galeotti, Juan Pablo
dc.contributor.author
Furia, Carlo A.
dc.contributor.author
May, Eva
dc.contributor.author
Fraser, Gordon
dc.contributor.author
Zeller, Andreas
dc.date.available
2019-09-27T20:53:55Z
dc.date.issued
2015-10
dc.identifier.citation
Galeotti, Juan Pablo; Furia, Carlo A.; May, Eva; Fraser, Gordon; Zeller, Andreas; Inferring loop invariants by mutation, dynamic analysis, and static checking; IEEE Computer Society; IEEE Transactions On Software Engineering; 41; 10; 10-2015; 1019-1037
dc.identifier.issn
0098-5589
dc.identifier.uri
http://hdl.handle.net/11336/84726
dc.description.abstract
Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants - properties that hold for every iteration of a loop. We show that significant loop invariant candidates can be generated by systematically mutating postconditions; then, dynamic checking (based on automatically generated tests) weeds out invalid candidates, and static checking selects provably valid ones. We present a framework that automatically applies these techniques to support a program prover, paving the way for fully automatic verification without manually written loop invariants: Applied to 28 methods (including 39 different loops) from various Java.util classes (occasionally modified to avoid using Java features not fully supported by the static checker), our DYNAMATE prototype automatically discharged 97 percent of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods - outperforming several state-of-the-art tools for fully automatic verification.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
IEEE Computer Society
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
AUTOMATIC VERIFICATION
dc.subject
DYNAMIC ANALYSIS
dc.subject
FUNCTIONAL PROPERTIES
dc.subject
INFERENCE
dc.subject
LOOP INVARIANTS
dc.subject.classification
Otras Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información
dc.subject.classification
Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información
dc.subject.classification
INGENIERÍAS Y TECNOLOGÍAS
dc.title
Inferring loop invariants by mutation, dynamic analysis, and static checking
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2019-09-26T17:09:59Z
dc.journal.volume
41
dc.journal.number
10
dc.journal.pagination
1019-1037
dc.journal.pais
Estados Unidos
dc.journal.ciudad
Los Alamitos, CA, USA
dc.description.fil
Fil: Galeotti, Juan Pablo. Universitat Saarland; Alemania. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.description.fil
Fil: Furia, Carlo A.. Swiss Federal Institute of Technology Zurich; Suiza
dc.description.fil
Fil: May, Eva. Google; Estados Unidos
dc.description.fil
Fil: Fraser, Gordon. University of Sheffield; Reino Unido
dc.description.fil
Fil: Zeller, Andreas. Universitat Saarland; Alemania
dc.journal.title
IEEE Transactions On Software Engineering
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/http://arxiv.org/abs/1407.5286
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://ieeexplore.ieee.org/document/7105412
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1109/TSE.2015.2431688
Archivos asociados