Sökning: onr:"swepub:oai:DiVA.org:kth-336732" >
Automatic Program I...
-
Amilon, JesperKTH,Teoretisk datalogi, TCS
(författare)
Automatic Program Instrumentation for Automatic Verification
- Artikel/kapitelEngelska2023
Förlag, utgivningsår, omfång ...
-
Cham :Springer Nature,2023
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:kth-336732
-
https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-336732URI
-
https://doi.org/10.1007/978-3-031-37709-9_14DOI
-
https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-510220URI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
Part of ISBN 9783031377082QC 20231123
-
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Esen, ZaferUppsala University, Uppsala, Sweden
(författare)
-
Gurov, Dilian,1964-KTH,Teoretisk datalogi, TCS(Swepub:kth)u1jmacmb
(författare)
-
Lidström, ChristianKTH,Teoretisk datalogi, TCS(Swepub:kth)u1thmxts
(författare)
-
Rümmer, Philipp,1978-Uppsala universitet,Avdelningen för datorteknik,Datorteknik,Embedded Systems(Swepub:uu)phiru321
(författare)
-
KTHTeoretisk datalogi, TCS
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Computer Aided VerificationCham : Springer Nature, s. 281-304, s. 281-304
-
Ingår i:CAV 2023: Computer Aided VerificationCham : Springer Nature, s. 281-304, s. 281-30497830313770829783031377099
Internetlänk
Hitta via bibliotek
Till lärosätets databas