Sökning: WFRF:(Gurov Dilian 1964 ) >
Constraint-Based Co...
-
Alshnakat, AnoudKTH,Teoretisk datalogi, TCS
(författare)
Constraint-Based Contract Inference for Deductive Verification
- Artikel/kapitelEngelska2020
Förlag, utgivningsår, omfång ...
-
2020-12-04
-
Cham :Springer Nature,2020
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:kth-290389
-
https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-290389URI
-
https://doi.org/10.1007/978-3-030-64354-6_6DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kap swepub-publicationtype
Anmärkningar
-
QC 20210301
-
Assertion-based software model checking refers to techniques that take a program annotated with logical assertions and statically verify that the assertions hold whenever program execution is at the corresponding control point. While the associated annotation overhead is relatively low, these techniques are typically monolithic in that they explore the state space of the whole program at once, and may therefore scale poorly to large programs. Deductive software verification, on the other hand, refers to techniques that prove the correctness of a piece of software against a detailed specification of what it is supposed to accomplish or compute. The associated verification techniques are modular and scale well to large code bases, but incur an annotation overhead that is often very high, which is a real obstacle for deductive verification to be adopted in industry on a wider scale. In this paper we explore synergies between the two mentioned paradigms, and in particular, investigate how interpolation-based Horn solvers used for software model checking can be instrumented to infer missing procedure contracts for use in deductive verification, thus aiding the programmer in the code annotation process. We summarise the main developments in the area of automated contract inference, and present our own experiments with contract inference for C programs, based on solving Horn clauses. To drive the inference process, we put program assertions in the main function, and adapt our TriCera tool, a model checker based on the Horn solver Eldarica, to infer candidate contracts for all other functions. The contracts are output in the ANSI C Specification Language (ACSL) format, and are then validated with the Frama-C deductive verification tool for C programs.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
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, P.
(författare)
-
KTHTeoretisk datalogi, TCS
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Deductive Software VerificationCham : Springer Nature, s. 149-176
Internetlänk
Hitta via bibliotek
Till lärosätets databas