Player FM 앱으로 오프라인으로 전환하세요!
Korrektheit durch formale Methoden - Bianca Lutz, Lars Hupel
Manage episode 450285562 series 3466870
Tipp: Kostenloses Webinar zu Qualitätsverbesserung von Software am 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
챕터
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)
123 에피소드
Manage episode 450285562 series 3466870
Tipp: Kostenloses Webinar zu Qualitätsverbesserung von Software am 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
챕터
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)
123 에피소드
모든 에피소드
×플레이어 FM에 오신것을 환영합니다!
플레이어 FM은 웹에서 고품질 팟캐스트를 검색하여 지금 바로 즐길 수 있도록 합니다. 최고의 팟캐스트 앱이며 Android, iPhone 및 웹에서도 작동합니다. 장치 간 구독 동기화를 위해 가입하세요.