# Formal Verification - Robust and Efficient code: Why Formal Verification

- Institution: CERN
- Department: inverted CSC
- Speaker: Kim ALBERTSSON
- Year: 2016
- Language: English
- Subjects: Computer science
- Source: [CERN](https://videos.cern.ch/record/3002919)
- Licence: [CERN](http://copyright.web.cern.ch)
- Who can watch: Tweens profiles and older (sources give no ratings; placed by Invisible Network from the source's own words)

LECTURE 2: In this lecture we will expand on the concepts of the previous lecture and establish formal methods in a broader context, ignoring implementation detail, and investigate how and where these methods are used today, and where they might be used tomorrow. As concrete examples we will be studying how FV can benefit static analysis and comp-cert, and verified C compiler.

This talk aims to introduce the concepts of Formal Verification and how they can be used to the benefit of the programmer to produce robust and efficient code. We will be looking into the subject at two levels, both and overview of what FV can concretely bring programmers and going into the nitty-gritty details of theorem proving one of the methods use for FV.

In general, FV means "proving that certain properties hold for a given system using formal mathematics". This definition can certainly feel daunting, however, as we will learn, we can reap benefits from the paradigm without digging too deep into the subject.

Examples where FV can help include proving that your code cannot raise division by zero exceptions; produce optimised byte code where the optimisations are proven to be safe and help reason about concurrent systems. .

0:00:00 Slide 1

0:01:14 Slide 2

0:02:09 Slide 3

0:04:17 Slide 4

0:07:03 Slide 5

0:07:29 Slide 6

0:08:31 Slide 7

0:11:04 Slide 8

0:12:54 Slide 9

0:13:45 Slide 10

0:16:45 Slide 11

0:18:53 Slide 12

0:19:28 Slide 13

0:20:09 Slide 14

0:21:19 Slide 15

0:23:20 Slide 16

0:25:24 Slide 17

0:25:30 Slide 18

0:26:37 Slide 19

0:27:52 Slide 20

0:30:15 Slide 21

0:30:44 Slide 22

0:30:52 Slide 23

0:30:58 Slide 24

0:31:10 Slide 25

0:31:19 Slide 26

0:31:33 Slide 27

0:31:42 Slide 28

0:32:13 Slide 29

0:33:39 Slide 30

0:35:01 Slide 31

0:35:24 Slide 32

0:35:41 Slide 33

0:38:26 Slide 34

0:39:35 Slide 35

0:40:39 Slide 36

0:41:56 Slide 37

0:43:49 Slide 38

0:46:30 Slide 39

0:46:50 Slide 40

0:49:07 Slide 41

0:50:42 Slide 42

0:52:40 Slide 43

0:53:37…

## Lectures

1. [Formal Verification - Robust and Efficient code: Why Formal Verification](https://invisiblenetwork.ai/learn/cern/3002919/0770ba093865), 1 h 7 min (CERN's player)