Publications

Can a smartphone app with AI replace the VNG in caloric testing?

Published in Laryngo-Rhino-Otologie, 2024

Dizziness is one of the most common symptoms in medicine, but the diagnosis is very complex and depends on the examiner's expertise. In addition, this experience and expensive, equipment-based, error-prone diagnostics are not available across the country. An Android smartphone app was developed that can be used by oneself or third parties for videonystagmography (VNG). VNG was carried out on 19 healthy volunteers at rest and after caloric testing of each ear in a conventional manner and using the smartphone app.

Sophia Reinhardt, Joshua Schmidt, Jonas Schneider, Elena Schulte, Michael Leuschel, Christiane Schüle and Jörg Schipper. (2023). "Can a smartphone app with AI replace the VNG in caloric testing?" Laryngo-Rhino-Otologie 103, 95th Annual Meeting German Society of Oto-Rhino-Laryngology, Head and Neck Surgery e. V., Bonn. https://www.thieme-connect.de/products/ejournals/abstract/10.1055/s-0044-1784589

New Applications and Techniques for Constraint Programming in B

Published in Universitäts- und Landesbibliothek Düsseldorf, 2023

In the first part, a translation of a popular formal specification language called Alloy to classical B is presented, which is automated by ProB. The second part of this thesis deals with constraint solving, which is one of the most important features of any formal verification tool.

Joshua Schmidt. (2023). "New Applications and Techniques for Constraint Programming in B" Dissertation. Universitäts- und Landesbibliothek Düsseldorf. https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=64042

Smartphone-Based Videonystagmography Using Artificial Intelligence

Published in Current Directions in Biomedical Engineering, 2023

We present a novel location- and time-independent mobile application for videonystagmography (VNG) to support vertigo patients and medical staff. No additional hardware is necessary. The app uses artificial intelligence for eye tracking and to detect a horizontal nystagmus.

Sophia Reinhardt, Joshua Schmidt, Jonas Schneider, Elena Schulte, Christiane Schüle, Michael Leuschel and Jörg Schipper. (2022). "Smartphone-Based Videonystagmography Using Artificial Intelligence" Current Directions in Biomedical Engineering. https://www.degruyter.com/document/doi/10.1515/cdbme-2023-1132/html

Clinical Nystagmus Characteristics - Distribution of Intensity Components in Acute Vertigo Patients

Published in Laryngo-Rhino-Otologie, 2023

For the evaluation of vestibular function, videonystagmography (VNG) is considered the gold standard in addition to subjective examination with Frenzel glasses. The intensity components are frequency and SPV (slow phase velocity) of the nystagmus. Currently, there are no clear values for the normal distribution of these parameters.

Elena Schulte, Sophia Reinhardt, Christian Hartmann, Joshua Schmidt, Jonas Schneider, Michael Leuschel, Christiane Schüle and Jörg Schipper. (2023). "Clinical Nystagmus Characteristics - Distribution of Intensity Components in Acute Vertigo Patients" Laryngo-Rhino-Otologie 102, 94th Annual Meeting German Society of Oto-Rhino-Laryngology, Head and Neck Surgery e. V.. https://www.thieme-connect.de/products/ejournals/abstract/10.1055/s-0043-1766830

SMT solving for the validation of B and Event-B models

Published in International Journal on Software Tools for Technology Transfer, 2022

This is a follow-up work where we additionally present a direct implementation of SMT solving in Prolog using ProB’s constraint solver as a theory solver. We hereby aim to combine the strengths of conflict-driven clause learning for identifying contradictions with ProB’s constraint solver for finding solutions.

Joshua Schmidt and Michael Leuschel. (2022). "SMT solving for the validation of B and Event-B models" International Journal on Software Tools for Technology Transfer. https://link.springer.com/article/10.1007/s10009-022-00682-y

Improving SMT Solver Integrations for the Validation of B and Event-B Models

Published in Proceedings FMICS (International Conference on Formal Methods for Industrial Critical Systems), 2021

In this paper, we substantially improve the translation from B to SMT-LIB by employing a more constructive rather than axiomatised style using Z3’s lambda functions. We further extend ProB’s interface to Z3 to run different solver configurations in parallel, e.g., either using the former or new translation.

Joshua Schmidt and Michael Leuschel. (2021). "Improving SMT Solver Integrations for the Validation of B and Event-B Models" Proceedings FMICS (International Conference on Formal Methods for Industrial Critical Systems). https://link.springer.com/chapter/10.1007/978-3-030-85248-1_7

VertiGo - a pilot project in nystagmus detection via webcam

Published in Current Directions in Biomedical Engineering, 2020

The aim of this study was to detect horizontal vestibular nystagmus utilizing a webcam. In the feasibility study, caloric induced vestibular nystagmus was recorded with conventional video-nystagmography and webcam.

Sophia Reinhardt, Joshua Schmidt, Michael Leuschel, Christiane Schüle and Jörg Schipper. (2020). "VertiGo – a pilot project in nystagmus detection via webcam" Current Directions in Biomedical Engineering. https://www.degruyter.com/document/doi/10.1515/cdbme-2020-0043/html

Analysing ProB's Constraint Solving Backends

Published in Proceedings ABZ (International Conference on Rigorous State Based Methods), 2020

We evaluate the strengths and weaknesses of different backends of the ProB constraint solver. For this, we train a random forest over a database of constraints to classify whether a backend is able to find a solution within a given amount of time or answers unknown.

Jannik Dunkelau, Joshua Schmidt and Michael Leuschel. (2020). "Analysing ProB's Constraint Solving Backends" Proceedings ABZ (International Conference on Rigorous State Based Methods). https://link.springer.com/chapter/10.1007/978-3-030-48077-6_8

Towards Constraint Logic Programming over Strings for Test Data Generation

Published in Proceedings WLP (Workshop on (Constraint) Logic Programming), 2020

In this paper, we evaluate to what extent constraint logic programming can be used to generate test data, focusing on strings in particular.

Sebastian Krings, Joshua Schmidt, Patrick Skowronek, Jannik Dunkelau and Dierk Ehmke. (2020). "Towards Constraint Logic Programming over Strings for Test Data Generation" Proceedings WLP (Workshop on (Constraint) Logic Programming). https://link.springer.com/chapter/10.1007/978-3-030-46714-2_10

Translating Alloy and Extensions to Classical B

Published in International Journal on Science of Computer Programming, 2020

This a follow-up article in which we introduce a denotational translation of the specification language Alloy to classical B including different Alloy extensions.

Sebastian Krings, Michael Leuschel, Joshua Schmidt, David Schneider and Marc Frappier. (2020). "Translating Alloy and Extensions to Classical B" International Journal on Science of Computer Programming. https://link.springer.com/chapter/10.1007/978-3-030-20652-9_9

Automated Backend Selection for ProB Using Deep Learning

Published in Proceedings NFM (International Symposium on NASA Formal Methods), 2019

In this paper, we use machine learning methods to automate the backend selection for the ProB model checker. In particular, we explore different approaches to deep learning and outline how we apply them to find a suitable backend for given input constraints.

Jannik Dunkelau, Sebastian Krings and Joshua Schmidt. (2018). "Automated Backend Selection for ProB Using Deep Learning" Proceedings NFM (International Symposium on NASA Formal Methods). https://link.springer.com/chapter/10.1007/978-3-030-20652-9_9

Experience Report on an Inquiry-Based Course on Model Checking

Published in Proceedings CEUR (Tagungsband des 16. Workshops "Software Engineering im Unterricht der Hochschulen"), 2019

In this paper, we present a recent revision of our course on model checking at the University of Düsseldorf, shifting from a classical lecture-based format to inquiry and research-based teaching.

Sebastian Krings, Philipp Körner and Joshua Schmidt. (2018). "Experience Report on an Inquiry-Based Course on Model Checking" Proceedings CEUR (Tagungsband des 16. Workshops "Software Engineering im Unterricht der Hochschulen"). https://ceur-ws.org/Vol-2358/

Measuring Coverage of Prolog Programs Using Mutation Testing

Published in Proceedings WFLP (International Workshop on Functional and (Constraint) Logic Programming), 2019

In this paper, we introduce a framework for Prolog programs measuring test coverage using mutations.

Alexandros Efremidis, Joshua Schmidt, Sebastian Krings and Philipp Körner. (2019). "Measuring Coverage of Prolog Programs Using Mutation Testing" Proceedings WFLP (International Workshop on Functional and (Constraint) Logic Programming). https://link.springer.com/chapter/10.1007/978-3-030-16202-3_3

Repair and Generation of Formal Models Using Synthesis

Published in Proceedings ABZ (International Conference on Rigorous State Based Methods), 2018

This paper is the follow-up work regarding the use of program synthesis for the interactive repair and generation of formal models using the B-Method.

Joshua Schmidt, Sebastian Krings and Michael Leuschel. (2018). "Repair and Generation of Formal Models Using Synthesis" Proceedings ABZ (International Conference on Rigorous State Based Methods). https://link.springer.com/chapter/10.1007/978-3-319-91271-4_6

A Translation from Alloy to B

Published in Proceedings ABZ (International Conference on Rigorous State Based Methods), 2018

In this paper, we introduce a translation of the specification language Alloy to classical B.

Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier and Michael Leuschel. (2018). "A Translation from Alloy to B" Proceedings ABZ (International Conference on Rigorous State Based Methods). https://link.springer.com/chapter/10.1007/978-3-319-91271-4_6

Interactive Model Repair by Synthesis

Published in Proceedings ABZ (International Conference on Rigorous State Based Methods), 2016

This short paper is the original idea of using program synthesis for interactive model repair of formal models using the B-Method.

Joshua Schmidt, Sebastian Krings and Michael Leuschel. (2016). "Interactive Model Repair by Synthesis" Proceedings ABZ (International Conference on Rigorous State Based Methods). https://link.springer.com/chapter/10.1007/978-3-319-33600-8_25

Dr. Joshua Schmidt

Publications