Proving Python code correct with Nagini
Formal Metadata
| Title | Proving Python code correct with Nagini |
|
| Title of Series | |
| Number of Parts | 8 |
| Author | |
| Contributors | |
| License | You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. |
| Identifiers | |
| Publisher | |
| Release Date | |
| Language | |
Content Metadata
| Subject Area | |
| Genre | |
| Abstract | With the introduction of PEP 484 type annotations, Python has made a big step towards making programs safer by statically ruling out type errors. But what if we go five steps further and prove that our programs don't crash for any reason at all and, moreover, do what we want them to do?
In this talk, I will give an informal overview about formal verification, what it is and what it can (and can't) do. I'll show how to use the automated verifier Nagini to express what a program is supposed to do and prove that it does. |
|
