onr:"swepub:oai:DiVA.org:kth-335068"
Search: onr:"swepub:oai:DiVA.org:kth-335068" > Trace-based Deducti...
- 1 of 1
- Previous record
- Next record
- To hitlist
- Bubel, RichardTechnical University of Darmstadt, Darmstadt, Germany (author)
Trace-based Deductive Verification
- Article/chapterEnglish2023
Publisher, publication year, extent ...
- EasyChair,2023
- printrdacarrier
Numbers
- LIBRIS-ID:oai:DiVA.org:kth-335068
- https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-335068URI
- https://doi.org/10.29007/vdfdDOI
Supplementary language notes
- Language:English
- Summary in:English
Part of subdatabase
- SwePubSwePub
Classification
Notes
- QC 20230831
- Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.
Subject headings and genre
- NATURVETENSKAP Data- och informationsvetenskap Datavetenskap hsv//swe
- NATURAL SCIENCES Computer and Information Sciences Computer Sciences hsv//eng
- contract-based reasoning
- deductive verification
- mu-calculus
- symbolic execution
- trace contracts
Added entries (persons, corporate bodies, meetings, titles ...)
- Gurov, Dilian,1964-KTH,Teoretisk datalogi, TCS(Swepub:kth)u1jmacmb (author)
- Hahnle, ReinerTechnical University of Darmstadt, Darmstadt, Germany (author)
- Scaletta, MarcoTechnical University of Darmstadt, Darmstadt, Germany (author)
- Technical University of Darmstadt, Darmstadt, GermanyTeoretisk datalogi, TCS (creator_code:org_t)
Related titles
- In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning: EasyChair, s. 73-95
Internet link
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Bubel, Richard
- Gurov, Dilian, 1 ...
- Hahnle, Reiner
- Scaletta, Marco
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Computer Science ...
- Articles in the publication
- Proceedings of 2 ...
- 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
