MBMV’23
Methoden und Beschreibungssprachen zur
Modellierung und Verifikation von Schaltungen und Systemen
23./24. März 2023, Technische Fakultät, Universität Freiburg
https://cca.informatik.uni-freiburg.de/mbmv23
[ cfp.pdf ] [ cfp.txt ] [ dates ] [ invited ] [ program ] [ organisation ] [ venue ] [ pc ]
Der 26. Workshop der GMM, ITG, und GI-Fachgruppen FG3 und FG4 “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” war ein Forum zu neuen Trends, Ergebnissen und aktuellen Fragen auf dem Gebiet der Modellierung.
News
-
Einige Folien sind nun verlinkt im Programm
Eingeladener Vortrag
“Early Co-verification of Firmware and Hardware to Speed up Development of Embedded Systems”
Programm
Hier finden sie das Programm.
1. Tag Donnerstag 23. März 2023
Session 1 09:00 - 10:00 Eingeladener Vortrag
- Joerg Bormann. Early Co-verification of Firmware and Hardware to Speed up Development of Embedded Systems”
Session 2 10:30 - 12:00 Scalability
- Julius Roob, Anoop Bhagyanath and Klaus Schneider. Towards Buffers as a Scalable Alternative to Registers for Processor-Local Memory
- Mark Deutel, Philipp Woller, Christopher Mutschler and Jürgen Teich. Energy-efficient Deployment of Deep Learning Applications on Cortex-M based Microcontrollers using Deep Compression
- Johannes Schreiner, Vasundhara Raje Gontia, Sebastian Prebeck and Wolfgang Ecker. Generator IP-reuse and Automated Infrastructure Generation for Model-based Full-Chip Generation
Session 3 13:30 - 14:30 Verification
- Arighna Deb, Kamalika Datta and Rolf Drechsler. Equivalence Checking of Majority-based Function Mapping on ReRAM Crossbars
- Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große and Rolf Drechsler. Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization (extended abstract)
Session 4 15:00 - 16:30 Tool, Case Study & Hybrid Systems
- Maximilian Heisinger. Boolean Format Multitool for the Next Generation (Tool page)
- Iwan Feras Fattohi, Christian Prehofer and Frank Slomka. Worst-Case Response Time Analysis of Earliest Deadline First in an Industrial Case Study
- Hagen Heermann and Christoph Grimm. Runtime Verification of Hybrid Systems with Affine Arithmetic Decision Diagrams
Session 5 16:30 - 17:30 Fachgruppensitzung
Workshop-Dinner 19:00 Rothaus Freiburg
2. Tag Freitag 24. März 2023
Session 6 09:00 - 10:00 Certification
- Florian Pollitt, Mathias Fleury and Armin Biere. Efficient Proof Checking with LRAT in CaDiCaL (Work in Progress)
- Emily Yu, Nils Froleyks, Armin Biere and Keijo Heljanko. Stratified Certification for k-Induction (Extended Abstract)
Session 7 10:30 - 12:00 RISC-V
- Lucas Klemmer, Sonja Gurtner and Daniel Grosse. How We Learned to Stop Worrying and Build a RISC-V VP with only one Microcode Instruction
- Lars Luchterhandt, Tom Nellius, Robert Beck, Rainer Dömer, Pascal Kneuper, Wolfgang Mueller and Babak Sadiye. Towards a Rocket Chip Based Implementation of the RISC-V GPC Architecture
- Niklas Bruns, Sallar Ahmadi-Pour, Sören Tempel and Rolf Drechsler. Towards Comprehensive Verification of Hardware and Software for RISC-V based Embedded Systems
Session 8 13:30 - 14:30 Testing
- Swantje Plambeck and Goerschwin Fey. Extended Abstract: Data-Driven Test Generation for Black-Box Systems From Learned Decision Tree Models
- Katharina Ruep and Daniel Große. Fuzz-Testing of SpinalHDL Designs
Session 9 15:00 - 16:30 Security
- Ece Nur Demirhan Coskun, Muhammad Hassan and Rolf Drechsler. Security Validation of VP-based Heterogeneous Systems: A Completeness-driven Perspective
- Lucas Deutschmann, Johannes Müller, Mohammad Fadiheh, Dominik Stoffel and Wolfgang Kunz. Formal Verification of Data-Obliviousness in Hardware
- Philipp Schmitz, Johannes Müller, Christian Bartsch, Dominik Stoffel and Wolfgang Kunz. UPEC-PN: Exhaustive constant time verification of low-level software using property checking
Termine
Die Tagung fand am Donnerstag 23. und Freitag 24. März 2023 statt.
Die finale Version der Beiträge für die Proceedings war am 8. März 2023 fällig.
Die verlängerte Einreichungsfrist für Beiträge endete am 3. Februar 2023.
Organisation
Veranstalter des MBMV waren GMM, ITG und GI FG3 und FG4
Armin Biere (Workshop Chair, co-PC Chair)
Daniel Große (co-PC Chair)
Themen
Diskussionsbeiträge zu folgenden Themen waren im Blickpunkt:
- Formale, semi-formale und andere Mittel zur Spezifikation und Modellierung
- Standards und Erweiterungen von Modellierungssprachen für Hardware oder HW/SW-Systeme
- Modelle und Methoden für die domänenübergreifende Entwicklung: analog-digital, cyber-physisch, HW/SW
- Verhaltensmodellierung, KI-basierte Modelle
- Modellbasierte Entwicklung
- Synthese und formale Synthese, Eigenschaftsverfeinerung aus Spezifikationen
- Formale Verifikation (Äquivalenz- und Eigenschaftsbeweise)
- Schaltungen und Systeme in sicherheitsrelevanten Produkten
- Verifikation nichtfunktionaler Eigenschaften
- Simulationsbasierte Verifikation und Validierung
- Digitalisierung der Entwicklung z.B. durch Machine Learning oder Datenanalyse
Die Betrachtung weiterer Aspekte im Bereich Modellierung und Verifikation war im Sinne des Workshops.
Tagungsband
Der Tagungsband soll als E-Book des VDE-Verlages erscheinen und ausgewählte englischsprachige Beiträge darüber hinaus in IEEE-Xplore übernommen werden.
Einreichungskategorien
Als Einreichungskategorien waren einerseits Wissenschaftliche Beiträge vorgesehen, zweitens Übersichtsvorträge, und drittens Kurzvorstellungen von Open-Source Software bzw. Benchmarks.
Wissenschaftliche Beiträge
Wissenschaftliche Beiträge (6-12 Seiten) ermöglichten unter anderem Doktorandinnen und Doktoranden ihre Arbeit vor Fachpublikum zur Diskussion zu stellen und angemessen zu veröffentlichen. Diese Beiträge wurden vom Programmkomitee nach Originalität und Qualität der Darstellung begutachtet. Ausgewählte englischsprachige Beiträge dieser Kategorie wurden in IEEE-Xplore übernommen.
Übersichtsvorträge
Übersichtsvorträge (1-4 Seiten) ermöglichten, die Bekanntheit schon veröffentlichter Arbeiten zu verbessern, Kontakte zu knüpfen oder vorläufige Arbeiten zur Diskussion zu stellen ohne dabei einen Beitrag veröffentlichen zu müssen. Diese Übersichtsvorträge wurden daher nur als Zusammenfassung im Tagungsband, aber nicht in IEEE-Xplore aufgenommen. Sie wurden vom Programmkomitee nach zu erwartender Qualität und inhaltlicher Relevanz und Bedeutung des zu erwartenden Vortrags begutachtet.
Open-Source Software / Benchmarks
Demos von Open-Source Software und die Vorstellung von Benchmarks ermöglichen entsprechende Entwicklungen vorzustellen. Weiterhin bestand die Möglichkeit diese live in einer Demosession vorzuführen und zu diskutieren. Zu diesem Zwecke sollt eine Kurzbeschreibung (maximal 1 Seite) über das Werkzeug oder den Benchmark eingereicht werden. Diese Beiträge wurden vom Programmkomitee nach inhaltlicher Relevanz begutachtet.
Einreichung
Die Einreichung lief über EasyChair unter https://easychair.org/my/conference?conf=mbmv23 im PDF-Format.
Es wurde erwartet Erstellung des Beitrrages die Formatvorlage des VDE-Verlags bzw. als latex_template.zip hier zu benutzen. Die Sprache des Workshops war Deutsch. Beiträge in englischer Sprache waren willkommen.
Programm Komitee
Armin Biere, Universität Freiburg
Jens Brandt, Hochschule Niederrhein
Oliver Bringmann, Universität Tübingen
Rolf Drechsler, Universität Bremen
Wolfgang Ecker, Infineon Technologies AG
Michael Glass, Universität Ulm
Christoph Grimm, TU Kaiserslautern
Daniel Große, JKU Linz
Christian Haubelt, Universität Rostock
Christoph Jäschke, IBM Research
Daniela Kaufmann, TU Wien
Thomas Klotz, Bosch Sensortec
Wolfgang Kunz, TU Kaiserslautern
Wolfgang Müller, Universität Paderborn
Daniel Müller-Gritschneder, TU München
Frank Oppenheimer, OFFIS
Martin Radetzki, Universität Stuttgart
Jürgen Ruf, Bosch Sensortec GmbH
Klaus Schneider, TU Kaiserslautern
Christoph Scholl, Universität Freiburg
Jens Schönherr, HTW Dresden
Frank Slomka, Universität Ulm
Jürgen Teich, Universität Erlangen-Nürnberg
Markus Wedler, Synopsys GmbH
Robert Wille, TU München
Ralf Wimmer, Altair Engineering GmbH
Registrierung
Die Teilnahmegebühr betrug 250 € mit 20 € Rabatt für VDE Mitglieder (also 230 €) und eine auf 50 € reduzierte Teilnahmegebühr für Studierende.
Veranstaltungsort
SR 02-016/18, Geb. 101
Technische Fakultät
Universität Freiburg
Georges-Köhler-Allee, Gebäude 101
79110 Freiburg
Frühere Workshops
MBMV’22, MBMV’21, MBMV’20, MBMV’19, MBMV’18, MBMV’17, MBMV’16, MBMV’15