Artwork

Contenu fourni par Richard Seidl - Experte für Software-Entwicklung und Testautomatisierung and Richard Seidl - Experte für Software-Entwicklung. Tout le contenu du podcast, y compris les épisodes, les graphiques et les descriptions de podcast, est téléchargé et fourni directement par Richard Seidl - Experte für Software-Entwicklung und Testautomatisierung and Richard Seidl - Experte für Software-Entwicklung ou son partenaire de plateforme de podcast. Si vous pensez que quelqu'un utilise votre œuvre protégée sans votre autorisation, vous pouvez suivre le processus décrit ici https://fr.player.fm/legal.
Player FM - Application Podcast
Mettez-vous hors ligne avec l'application Player FM !

Korrektheit durch formale Methoden - Bianca Lutz, Lars Hupel

25:08
 
Partager
 

Manage episode 450285562 series 3466870
Contenu fourni par Richard Seidl - Experte für Software-Entwicklung und Testautomatisierung and Richard Seidl - Experte für Software-Entwicklung. Tout le contenu du podcast, y compris les épisodes, les graphiques et les descriptions de podcast, est téléchargé et fourni directement par Richard Seidl - Experte für Software-Entwicklung und Testautomatisierung and Richard Seidl - Experte für Software-Entwicklung ou son partenaire de plateforme de podcast. Si vous pensez que quelqu'un utilise votre œuvre protégée sans votre autorisation, vous pouvez suivre le processus décrit ici https://fr.player.fm/legal.
Mathematik meets Software-Qualität

Tipp! Kostenloses Webinar: So gelingt Qualitätsverbesserung von Software wirklich! - 11. März 11 Uhr Infos unter https://swt.fm/quality

"Mit Tests kann ich Fehlerfreiheit nicht nachweisen. Es gibt einfach bestimmte Domänen, da brauche ich aber die Fehlerfreiheit und eben auch den Nachweis." - Lars Hupel, Bianca Lutz

In der neuesten Episode des Software Testing Podcasts feiern wir die World Quality Week. Ich spreche mit mit Lars und Bianca darüber, wie man Fehlerfreiheit in Software mathematisch beweisen kann und welche Tools dabei helfen. Bianca erklärt uns anhand von Beispielen aus der Finanz- und Automobilbranche, warum bestimmte Systeme absolute Fehlerfreiheit benötigen. Lars ergänzt das Gespräch mit Einblicken in formale Methoden und wie sie in der Praxis angewendet werden. Ein besonders interessantes Thema war, wie KI uns bei der Beweisführung unterstützen kann.

Lars Hupel ist Chefevangelist für digitale Währungen bei Giesecke+Devrient, einem internationalen Unternehmen für Sicherheitstechnologie. Im Rahmen dieser Tätigkeit hält und schreibt Lars zahlreiche Vorträge, Workshops und Artikel, um die Technik hinter Digitalwährungen einem breiten Publikum zugänglich zu machen. Mit einem Hintergrund als Softwareentwickler trägt Lars aber auch zur Produktentwicklung bei und vertritt das Unternehmen bei verschiedenen Industriegremien. Lars hat im Bereich Logik und Verifikation an der TU München promoviert und bringt diese Erkenntnisse ein, um die Produkte von Giesecke+Devrient noch sicherer zu machen.

Bianca Lutz ist Softwarearchitektin bei der Active Group GmbH und arbeitet von Berlin aus. Schon im Studium interessierte sie sich für formale Methoden und hat mit dem Beweisassistenten Isabelle/HOL gearbeitet. Aber auch technische Themen, wie Betriebssysteme und hier vor allem eingebettete Systeme, begeistern sie bis heute. Sie war an verschiedenen wissenschaftlichen Publikationen beteiligt, ist Linux-Kernel-Contributor und hat im Rahmen ihrer Abschlussarbeit in Isabelles Archive of Formal Proofs veröffentlicht. Nach mehrjähriger Tätigkeit in der Versicherungsbranche, bei der sie es vor allem mit Legacy-Code zu tun hatte, wechselte sie 2022 ins Lager der Funktionalen Programmierung über.

Highlights:

  • In Bereichen wie Finanzen und Medizin ist Fehlerfreiheit entscheidend, und formale Methoden können dabei helfen.
  • Formale Methoden nutzen mathematische Modelle und Beweisassistenten, um Softwarefehler zu vermeiden.
  • Microsoft nutzt automatisierte Tools, um Treiber auf Fehlerfreiheit zu überprüfen.
  • Formale Methoden sind keine Allheilmittel, sondern ergänzen andere Testmethoden.
  • Änderungen in der Software können zu aufwendigen Anpassungen in den Beweisen führen.

Danke an die Community-Partner des Podcasts:Alliance for Qualification | ASQF | Austrian Testing Board | dpunkt.verlag | German Testing Board | German Testing Day | GI Fachgruppe TAV | Heise | HANSER Verlag | ISTQB | iSQI GmbH | oop | QS-TAG | SIGS-DATACOM | skillsclub | Swiss Testing Board | TACON

Credits: Sound | Grafik

  continue reading

Chapitres

1. Einführung und Begrüßung (00:00:00)

2. Formale Methoden in der Qualitätssicherung (00:01:06)

3. Praktische Anwendung formaler Methoden (00:08:04)

4. Einführung in formale Methoden (00:12:02)

5. Verifizierung von CompCert (00:13:01)

6. KI-Unterstützung bei formalen Beweisen (00:22:03)

7. Einführung in klassische KI und formale Methoden (00:23:47)

125 episodes

Artwork
iconPartager
 
Manage episode 450285562 series 3466870
Contenu fourni par Richard Seidl - Experte für Software-Entwicklung und Testautomatisierung and Richard Seidl - Experte für Software-Entwicklung. Tout le contenu du podcast, y compris les épisodes, les graphiques et les descriptions de podcast, est téléchargé et fourni directement par Richard Seidl - Experte für Software-Entwicklung und Testautomatisierung and Richard Seidl - Experte für Software-Entwicklung ou son partenaire de plateforme de podcast. Si vous pensez que quelqu'un utilise votre œuvre protégée sans votre autorisation, vous pouvez suivre le processus décrit ici https://fr.player.fm/legal.
Mathematik meets Software-Qualität

Tipp! Kostenloses Webinar: So gelingt Qualitätsverbesserung von Software wirklich! - 11. März 11 Uhr Infos unter https://swt.fm/quality

"Mit Tests kann ich Fehlerfreiheit nicht nachweisen. Es gibt einfach bestimmte Domänen, da brauche ich aber die Fehlerfreiheit und eben auch den Nachweis." - Lars Hupel, Bianca Lutz

In der neuesten Episode des Software Testing Podcasts feiern wir die World Quality Week. Ich spreche mit mit Lars und Bianca darüber, wie man Fehlerfreiheit in Software mathematisch beweisen kann und welche Tools dabei helfen. Bianca erklärt uns anhand von Beispielen aus der Finanz- und Automobilbranche, warum bestimmte Systeme absolute Fehlerfreiheit benötigen. Lars ergänzt das Gespräch mit Einblicken in formale Methoden und wie sie in der Praxis angewendet werden. Ein besonders interessantes Thema war, wie KI uns bei der Beweisführung unterstützen kann.

Lars Hupel ist Chefevangelist für digitale Währungen bei Giesecke+Devrient, einem internationalen Unternehmen für Sicherheitstechnologie. Im Rahmen dieser Tätigkeit hält und schreibt Lars zahlreiche Vorträge, Workshops und Artikel, um die Technik hinter Digitalwährungen einem breiten Publikum zugänglich zu machen. Mit einem Hintergrund als Softwareentwickler trägt Lars aber auch zur Produktentwicklung bei und vertritt das Unternehmen bei verschiedenen Industriegremien. Lars hat im Bereich Logik und Verifikation an der TU München promoviert und bringt diese Erkenntnisse ein, um die Produkte von Giesecke+Devrient noch sicherer zu machen.

Bianca Lutz ist Softwarearchitektin bei der Active Group GmbH und arbeitet von Berlin aus. Schon im Studium interessierte sie sich für formale Methoden und hat mit dem Beweisassistenten Isabelle/HOL gearbeitet. Aber auch technische Themen, wie Betriebssysteme und hier vor allem eingebettete Systeme, begeistern sie bis heute. Sie war an verschiedenen wissenschaftlichen Publikationen beteiligt, ist Linux-Kernel-Contributor und hat im Rahmen ihrer Abschlussarbeit in Isabelles Archive of Formal Proofs veröffentlicht. Nach mehrjähriger Tätigkeit in der Versicherungsbranche, bei der sie es vor allem mit Legacy-Code zu tun hatte, wechselte sie 2022 ins Lager der Funktionalen Programmierung über.

Highlights:

  • In Bereichen wie Finanzen und Medizin ist Fehlerfreiheit entscheidend, und formale Methoden können dabei helfen.
  • Formale Methoden nutzen mathematische Modelle und Beweisassistenten, um Softwarefehler zu vermeiden.
  • Microsoft nutzt automatisierte Tools, um Treiber auf Fehlerfreiheit zu überprüfen.
  • Formale Methoden sind keine Allheilmittel, sondern ergänzen andere Testmethoden.
  • Änderungen in der Software können zu aufwendigen Anpassungen in den Beweisen führen.

Danke an die Community-Partner des Podcasts:Alliance for Qualification | ASQF | Austrian Testing Board | dpunkt.verlag | German Testing Board | German Testing Day | GI Fachgruppe TAV | Heise | HANSER Verlag | ISTQB | iSQI GmbH | oop | QS-TAG | SIGS-DATACOM | skillsclub | Swiss Testing Board | TACON

Credits: Sound | Grafik

  continue reading

Chapitres

1. Einführung und Begrüßung (00:00:00)

2. Formale Methoden in der Qualitätssicherung (00:01:06)

3. Praktische Anwendung formaler Methoden (00:08:04)

4. Einführung in formale Methoden (00:12:02)

5. Verifizierung von CompCert (00:13:01)

6. KI-Unterstützung bei formalen Beweisen (00:22:03)

7. Einführung in klassische KI und formale Methoden (00:23:47)

125 episodes

Tous les épisodes

×
 
Loading …

Bienvenue sur Lecteur FM!

Lecteur FM recherche sur Internet des podcasts de haute qualité que vous pourrez apprécier dès maintenant. C'est la meilleure application de podcast et fonctionne sur Android, iPhone et le Web. Inscrivez-vous pour synchroniser les abonnements sur tous les appareils.

 

Guide de référence rapide

Écoutez cette émission pendant que vous explorez
Lire