We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Get Started with Open Source Formal Verification

Formal Metadata

Title
Get Started with Open Source Formal Verification
Title of Series
Number of Parts
542
Author
License
CC Attribution 2.0 Belgium:
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
Formal verification is the act of proving the correctness of software using mathematics. That means proving that your code is free of bugs and/or follows its specifications. SPARK is both a language (subset of Ada) and a set of tools that bring automatic formal verification in the hands of any developer. This technology is getting more interest from the industry (e.g. NVIDIA recently) for its extremely powerful properties in terms of safety and security. However, it is not widely known that SPARK is both open source and very easy to start using. In this talk I will provide quick and easy instructions to start your first formally verified library in SPARK. Using only free and open-source tools and resources (compiler, package manager, IDE, verification tools).