kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Trace-based Deductive Verification
Technical University of Darmstadt, Darmstadt, Germany.
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
Technical University of Darmstadt, Darmstadt, Germany.
Technical University of Darmstadt, Darmstadt, Germany.
2023 (English)In: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair , 2023, Vol. 94, p. 73-95Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
EasyChair , 2023. Vol. 94, p. 73-95
Keywords [en]
contract-based reasoning, deductive verification, mu-calculus, symbolic execution, trace contracts
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-335068DOI: 10.29007/vdfdScopus ID: 2-s2.0-85166468981OAI: oai:DiVA.org:kth-335068DiVA, id: diva2:1793146
Conference
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023, Manizales, Colombia, Jun 4 2023 - Jun 9 2023
Note

QC 20230831

Available from: 2023-08-31 Created: 2023-08-31 Last updated: 2023-08-31Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 23 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf