Provably Sound and Secure Automatic Proving and Generation of Verification Conditions

Provably Sound and Secure Automatic Proving and Generation of Verification Conditions

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 ca...

Full description

Bibliographic Details
Main Author: Lundberg, Didrik
Format: Others
Language:English
Published: KTH, Teoretisk datalogi, TCS 2018
Subjects:
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
Online Access:http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-239441

Internet

http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-239441

Similar Items