Global ETD Search

1	Provably Sound and Secure Automatic Proving and Generation of Verification Conditions / Tillförlitligt sund och säker automatisk generering och bevisning av verifieringsvillkor Lundberg, Didrik January 2018 (has links) Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project. / Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet. HOL4 HOL Higher-order logic SML Poly/ML Formal methods Axiomatic semantics Formal verification Static verification Program verification Hoare logic Floyd-Hoare logic ITP Interactive theorem prover Theorem prover Proof assistant BIR Automated theorem proving ATP Automated deduction Computer-assisted proof Automated reasoning Computer Sciences Datavetenskap (datalogi) Software Engineering Programvaruteknik

Search results

Provably Sound and Secure Automatic Proving and Generation of Verification Conditions / Tillförlitligt sund och säker automatisk generering och bevisning av verifieringsvillkor