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
Combining Inlining and Contracting for Human Efficient Deductive Verification
KTH, School of Electrical Engineering and Computer Science (EECS).
2019 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

A function is functionally correct when it behaves according to a specification that describes its input-output behaviour. With deductive verification, it is possible to prove whether a function conforms to its specification or not. The specification is provided in the form of a source code annotation and describes the function’s input-output behaviour using first-order logic. The function and specification are then used to generate logic formulas that, if proven valid, ensure that the function follows the specification.Creating these source annotations, also called contracts, can be difficult, time-consuming and hence, costly. Therefore, reducing the cost by decreasing the human workload would be a significant step toward large scale deductive verification. One way to do so is to use inlining, which eliminates function definitions by replacing all call sites with the function body instead.This thesis explores if and how inlining can be combined with contracting to reduce the human workload by reducing the number of contracts to be written. For this to be possible, a method to estimate the machine effort required to prove an inlined version is needed. In other words, we need to be able to estimate the verification time for a code module. To this end, two Scania code modules and five categories of artificial programs have been measured.By using function metrics and the verification times of the artificial programs, a heuristic was created using regression. This heuristic was then tested on the Scania modules. The results suggest that the artificial modules were not complex enough to accurately predict the Scania modules. However, it was possible to fit the heuristic to the Scania modules so that no estimate of a Scania module was severely off target. In other words, the Scania modules and their inlined versions were similar enough to be roughly estimated with the same function.If this similarity extends to other industry modules, then creating a general heuristic for estimating verification time would be possible

Abstract [sv]

En funktion är funktionellt korrekt när dess beteende överenstämmer med en specifikation. Med deduktiv verifikation är det möjligt att bevisa om en funktion följer sin specifikation. Specifikationen ges i form av en källkodsannotering och beskriver förhållandet mellan indata och utdata med hjälp av första ordningens logik. Implementationen och specifikationen används sedan för att generera logiska formler som, om bevisade valida, försäkrar att implementationen följer specifikationen.Skapandet av dessa källkodsannoteringar, som även kallas kontrakt, kan vara svårt, tidskrävande och kostsamt. Att reducera kostnaden genom att minska den mänskliga arbetsbördan vore ett stort steg mot storskalig deduktiv verifikation. Ett sätt att uppnå detta är genom inlining, med inlining kan man byta ut alla anrop till en funktion mot dess funktionskropp istället.Den här uppsatsen utforskar om och hur inlining kan kombineras med kontrakt för att minska den mänskliga arbetsinsatsen genom att reducera antalet kontrakt som måste skrivas. För att detta ska vara möjligt krävs en metod för att approximera maskinarbetsbördan som krävs för att genomföra ett bevis av en version med inlining. Med andra ord behöver vi kunna estimera verifikationstiden för en kodmodul. Mot detta ändamål, så har två Scania-moduler och fem kategorier av artificiella program mätts upp.Med funktionsmetriker och verifikationstider för de artificiella programmen, så skapades en heuristik med hjälp av regression. heuristiken testades sedan på Scania-modulerna. Resultaten antyder att de artificiella programmen inte är komplexa nog för att tillräckligt estimera Scania-modulerna. Däremot var det möjligt att anpassa heuristiken till Scania-modulerna så att ingen version hade ett överdrivet estimeringsfel.Med andra ord så är Scania-modulerna och deras olika versioner lika nog för att grovt estimeras av samma funktion. Om denna likhet sträcker sig till andra industrimoduler, borde det vara möjligt att konstruera en mer generell heuristik som kan estimera verifikationstiden.

Place, publisher, year, edition, pages
2019. , p. 62
Series
TRITA-EECS-EX ; 2019:218
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-254971OAI: oai:DiVA.org:kth-254971DiVA, id: diva2:1337066
Educational program
Master of Science - Computer Science
Supervisors
Examiners
Available from: 2019-07-11 Created: 2019-07-11 Last updated: 2019-07-11Bibliographically approved

Open Access in DiVA

fulltext(2964 kB)9 downloads
File information
File name FULLTEXT01.pdfFile size 2964 kBChecksum SHA-512
6337ba99bb1f505cc7ba8ff988404d82b78b477d5fe63bc2956f5e6adeb10cc224c49ff84761bc04d9edf5e3157a9a571c686ab428ec01f85e007f5450aaed59
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: 9 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: 94 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