Sökning: onr:"swepub:oai:DiVA.org:kth-286278" >
mCoq: Mutation Anal...
mCoq: Mutation Analysis for Coq Verification Projects
- Artikel/kapitelEngelska2020
Förlag, utgivningsår, omfång ...
-
2020-10
-
New York, NY, USA :Association for Computing Machinery (ACM),2020
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:kth-286278
-
https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-286278URI
-
https://doi.org/10.1145/3377812.3382156DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
QC 20210607
-
Software developed and verified using proof assistants, such as Coq, can provide trustworthiness beyond that of software developed using traditional programming languages and testing practices. However, guarantees from formal verification are only as good as the underlying definitions and specification properties. If properties are incomplete, flaws in definitions may not be captured during verification, which can lead to unexpected system behavior and failures. Mutation analysis is a general technique for evaluating specifications for adequacy and completeness, based on making small-scale changes to systems and observing the results. We demonstrate mCoq, the first mutation analysis tool for Coq projects. mCoq changes Coq definitions, with each change producing a modified project version, called a mutant, whose proofs are exhaustively checked. If checking succeeds, i.e., the mutant is live, this may indicate specification incompleteness. Since proof checking can take a long time, we optimized mCoq to perform incremental and parallel processing of mutants. By applying mCoq to popular Coq libraries, we found several instances of incomplete and missing specifications manifested as live mutants. We believe mCoq can be useful to proof engineers and researchers for analyzing software verification projects. The demo video for mCoq can be viewed at: https://youtu.be/QhigpfQ7dNo.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Palmskog, KarlKTH,Teoretisk datalogi, TCS(Swepub:kth)u1dxbowv
(författare)
-
Celik, Ahmet
(författare)
-
Gallego Arias, Emilio Jesús
(författare)
-
Gligoric, Milos
(författare)
-
KTHTeoretisk datalogi, TCS
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Proceedings of the ACM/IEEE 42nd International Conference on Software EngineeringNew York, NY, USA : Association for Computing Machinery (ACM), s. 89-92
Internetlänk