התחל במצב לא מקוון עם האפליקציה Player FM !
Korrektheit durch formale Methoden - Bianca Lutz, Lars Hupel
Manage episode 450285562 series 3466870
Deine Tests dauern ewig? 👉🏻 So bekommst Du trotzdem schnelles Feedback
"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
פרקים
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)
145 פרקים
Manage episode 450285562 series 3466870
Deine Tests dauern ewig? 👉🏻 So bekommst Du trotzdem schnelles Feedback
"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
פרקים
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)
145 פרקים
כל הפרקים
×
1 Synthetische Testdaten - Dominic Steinhöfel 30:22

1 Zeitalter der Autonomik - Peter Liggesmeyer 30:38

1 KI Einsatz für die Legacy-Modernisierung - Erik Dörnenburg 37:00

1 Von der Testfactory zum QS-Coaching - Stephan Brehovsky, Christian Ulrich 18:18

1 Mit Nudging zu mehr Security - Dr. Erlijn van Genuchten 25:09

1 Gewaltfreie Kommunikation im Software Testing - Maroš Kutschy 21:39

1 Geschäftsgetriebene Testautomatisierung - Jörg Sievers 27:46

1 Eine Referenzimplementierung als Testorakel - Stefanie Leitner 20:04

1 Lernen mit Simulationen - Andreas Wübbeke, Johanna Maduch 26:00

1 Leichtgewichtige Testkonzepte im Bundesverwaltungsamt - Dr. Oliver Kortendick, Simone Mester 23:25

1 Robot Test Framework - René Rohner 31:58

1 Software Testing Podcasts - Markus Thaler 46:29

1 Enterprise Testing - Ursula Beiersdorf 30:03

1 Microservices testen - Michael Kutz 37:02
ברוכים הבאים אל Player FM!
Player FM סורק את האינטרנט עבור פודקאסטים באיכות גבוהה בשבילכם כדי שתהנו מהם כרגע. זה יישום הפודקאסט הטוב ביותר והוא עובד על אנדרואיד, iPhone ואינטרנט. הירשמו לסנכרון מנויים במכשירים שונים.