https://fosdem.org/2023/schedule/event/open_source_formal_verification/

FOSDEM23

  * Home
  * About
  * News
  * Schedule
  * Stands
  * Volunteer
  * Practical
  * Search: [                    ]

Brussels / 4 & 5 February 2023

schedule

  * News
  * Sponsors
  * Contact

  * FOSDEM 2023
  * /
  * Schedule
  * /
  * Events
  * /
  * Lightning Talks
  * /
  * Get Started with Open Source Formal Verification

Get Started with Open Source Formal Verification

  * Track: Lightning Talks
  * Room: H.2215 (Ferrer)
  * Day: Sunday
  * Start: 15:00
  * End: 15:15
  * Video only: h2215_ferrer
  * Chat: Join the conversation!


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

Speakers

Photo of Fabien Chouteau Fabien Chouteau

Attachments

  * (slides)

Links

  * SPARK repository on GitHub
  * Alire: Package manager for SPARK/Ada
  * Blog post on the adoption of SPARK by NVIDIA
  * Video recording (WebM/VP9, 36M)
  * Video recording (mp4/aac, 104M)
  * Chat room (web)
  * Chat room (app)
  * Submit feedback

FOSDEM

  * Home
  * News
  * About
  * Sponsors
  * Donate
  * T-shirts and hoodies
  * FAQ
  * Archives

This year

  * Schedule
  * Stands
  * Certification exams
  * T-shirts and hoodies
  * Volunteer
  * Fringe

Practical information

  * T-shirts and hoodies
  * Accessibility
  * Code of Conduct
  * During the Event
  * COVID-19 policy

Media and press

  * Social media

FOSDEM23

Brussels / 4 & 5 February 2023

This work is licensed under the Creative Commons Attribution 2.0
Belgium Licence.
To view a copy of this licence, visit http://creativecommons.org/
licenses/by/2.0/be/deed.en
or send a letter to Creative Commons, 444 Castro Street, Suite 900,
Mountain View, California, 94041, USA.
All content such as talks and biographies is the sole responsibility
of the speaker.