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 |