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
Verifying Temporal Properties Using Deductive Verifiers
KTH, School of Electrical Engineering and Computer Science (EECS).
KTH, School of Electrical Engineering and Computer Science (EECS).
2019 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesisAlternative title
Verifiering av temporala egenskaper med hjälp av deduktiva verifierare (Swedish)
Abstract [en]

Formal verification is an area of theoretical computer science where mathematical logic is used to prove that a program behaves in a certain way. With the methods in formal verification, you can prove that the program follows some given specification and thereby behaves in the desired way. The area is largely split up into two distinct parts. One deals with how the program transforms data. This uses Hoare logic and deductive verification to prove that the program follows a given specification. The other part deals with temporal properties of the program, this uses temporal logic and model checkers.

The two areas are today largely separated. This report builds on a framework by Alur and Chaudhuri [1] which proves temporal properties in a Hoare logic style reasoning. By using this framework, this report aims to check the viability of using it with deductive verifiers. Thereby bridging the gap between the two areas for formal verification.

In conclusion, the report finds that it is certainly possible to prove temporal properties for C programs using Alur and Chaudhuri’s framework with deductive verifiers. In practical terms, though, it requires too much work to be feasible to use this framework by manually creating annotations for the deductive verifiers. In a small example program of 13 lines, proving a temporal property required around 50 extra lines of annotations. However, some parts of the annotation process could be automated with tooling support but to achieve full automation is probably not possible. This is partly due to ranking functions that the framework requires which, in general, are not easy to generate automatically.

Abstract [sv]

Formell verifikation är ett område inom teoretisk datalogi där man genom matematisk logik vill bevisa att ett program beter sig på ett visst sätt. Genom detta kan man bevisa att programmet följer en given specifikation och beter sig som man tänkt. Detta område kan delas upp i två separata delar. Den ena handlar om att visa hur programmet transformerar data och bygger på Hoare logik och deduktiv verifikation för att bevisa att programmet följer en viss specifikation. Den andra delen handlar om temporala egenskaper och använder sig av model checking och temporal logik. Dessa delar behandlas vanligtvis separat från varandra. Denna rapport bygger på ett logiskt system utvecklat av Alur och Chaudhuri [1] som används för att bevisa temporala egenskaper genom ett angreppssätt som använder Hoare-logik. Genom att använda detta system vill denna rapport undersöka huruvida det är möjligt att bevisa temporala egenskaper med hjälp av deduktiva verifierare och därigenom minska klyftan mellan dessa två områden av formel verifikation.

Rapporten finner att det är möjligt att använda Alur och Chaudhuri’s system för att bevisa temporala egenskaper genom deduktiva verifierare. I praktiska termer krävs det för mycket arbete för att kunna användas genom att manuellt skapa instruktioner till den deduktiva verifieraren. I ett litet exempelprogram på 13 rader kräves 50 extra rader av annotationer för att bevisa en viss temporal egenskap. Stora delar av den processen skulle dock kunna automatiseras med verktygsstöd. Att automatisera hela processen är dock antagligen inte möjligt. Detta är dels pågrund av att de rankning funktioner som systemet använder sig av är svåra att automatisera.

Place, publisher, year, edition, pages
2019.
Series
TRITA-EECS-EX ; 2019:326
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-255157OAI: oai:DiVA.org:kth-255157DiVA, id: diva2:1338659
Subject / course
Computer and Systems Sciences
Supervisors
Examiners
Available from: 2019-07-29 Created: 2019-07-23 Last updated: 2019-07-29Bibliographically approved

Open Access in DiVA

fulltext(561 kB)16 downloads
File information
File name FULLTEXT01.pdfFile size 561 kBChecksum SHA-512
b3429685507d524f230b3dfa8dcb4405366d5b7c56bcb3a30a51ac7ba4e90b13da5da948726a34be290ebeebb9c3f540e002c80e34a47c8a10a00a6b879949f5
Type fulltextMimetype application/pdf

By organisation
School of Electrical Engineering and Computer Science (EECS)
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 16 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 72 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