onr:"swepub:oai:DiVA.org:kth-290389"
Search: onr:"swepub:oai:DiVA.org:kth-290389" > Constraint-Based Co...
- 1 of 1
- Previous record
- Next record
- To hitlist
- Alshnakat, AnoudKTH,Teoretisk datalogi, TCS (author)
Constraint-Based Contract Inference for Deductive Verification
- Article/chapterEnglish2020
Publisher, publication year, extent ...
- 2020-12-04
- Cham :Springer Nature,2020
- printrdacarrier
Numbers
- 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
Supplementary language notes
- Language:English
- Summary in:English
Part of subdatabase
- SwePubSwePub
Classification
Notes
- 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.
Subject headings and genre
- NATURVETENSKAP Data- och informationsvetenskap Datavetenskap hsv//swe
- NATURAL SCIENCES Computer and Information Sciences Computer Sciences hsv//eng
- Logic programming
- Specification languages
- Specifications
- Constraint-based
- Corresponding control points
- Deductive verification
- Inference process
- Program execution
- Software model checking
- Software verification
- Verification techniques
- Model checking
Added entries (persons, corporate bodies, meetings, titles ...)
- Gurov, Dilian,1964-KTH,Teoretisk datalogi, TCS(Swepub:kth)u1jmacmb (author)
- Lidström, ChristianKTH,Teoretisk datalogi, TCS(Swepub:kth)u1thmxts (author)
- Rümmer, P. (author)
- KTHTeoretisk datalogi, TCS (creator_code:org_t)
Related titles
- In:Deductive Software VerificationCham : Springer Nature, s. 149-176
Internet link
Find in a library
- Deductive Software Verification (Search for host publication in LIBRIS)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Alshnakat, Anoud
- Gurov, Dilian, 1 ...
- Lidström, Christ ...
- Rümmer, P.
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Computer Science ...
- Articles in the publication
- Deductive Softwa ...
- By the university
- Royal Institute of Technology
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
