# Formal verification - Robust and efficient code: Introduction to Formal Verification

- Institution: CERN
- Department: inverted CSC
- Speaker: Kim ALBERTSSON
- Year: 2016
- Language: English
- Subjects: Computer science
- Source: [CERN](https://videos.cern.ch/record/3002891)
- 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 1: We will establish two general approaches to FV and where they are applicable: model checking and theorem proving. We will explore the latter in more details and have a brief look at the underlying theory, predicate logic. We will see how this family of logic systems can be used to prove abstract properties of our program and why this is useful. Practical examples will be presented and explained. ---- 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:39 Slide 2

0:02:29 Slide 3

0:03:46 Slide 4

0:05:32 Slide 5

0:06:14 Slide 6

0:06:36 Slide 7

0:09:53 Slide 8

0:09:58 Slide 9

0:10:25 Slide 10

0:11:27 Slide 11

0:12:51 Slide 12

0:13:46 Slide 13

0:14:11 Slide 14

0:15:03 Slide 15

0:16:46 Slide 16

0:18:12 Slide 17

0:18:35 Slide 18

0:18:56 Slide 19

0:19:09 Slide 20

0:19:44 Slide 21

0:21:03 Slide 22

0:22:19 Slide 23

0:23:52 Slide 24

0:25:42 Slide 25

0:25:46 Slide 26

0:25:53 Slide 27

0:26:00 Slide 28

0:26:39 Slide 29

0:26:43 Slide 30

0:26:59 Slide 31

0:28:56 Slide 32

0:29:18 Slide 33

0:29:25 Slide 34

0:30:34 Slide 35

0:32:05 Slide 36

0:33:39 Slide 37

0:36:05 Slide 38

0:37:30 Slide 39

0:38:33 Slide 40

0:40:01 Slide 41

0:41:58 Slide…

## Lectures

1. [Formal verification - Robust and efficient code: Introduction to Formal Verification](https://invisiblenetwork.ai/learn/cern/3002891/e585a492513d), 1 h 1 min (CERN's player)