Combining Inlining and Contracting for Human Efficient Deductive Verification
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 annotati...
Main Author: | |
---|---|
Format: | Others |
Language: | English |
Published: |
KTH, Skolan för elektroteknik och datavetenskap (EECS)
2019
|
Subjects: | |
Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-254971 |