A Quantitative Metric Temporal Logic for Execution-Time Constrained Verification. - Sascha Lehmann; Sven-Thomas Antoni; Alexander Schlaefer; Sibylle Schupp (CyPhy/WESE, 2018)

Model checking for trigger loss detection during Doppler ultrasound-guided fetal cardiovascular MRI. - Sven-Thomas Antoni; Sascha Lehmann; Maximilian Neidhardt; Kai Fehrs; Christian Ruprecht; Fabian Kording; Gerhard Adam; Sibylle Schupp; Alexander Schlaefer (Int. J. Comput. Assist. Radiol. Surg., 2018)

Synthesizing Strategies for Needle Steering in Gelatin Phantoms. - Antje Rogalla; Sascha Lehmann; Maximilian Neidhardt; Johanna Sprenger; Marcel Bengs; Alexander Schlaefer; Sibylle Schupp (MARS@ETAPS, 2020)

Online Strategy Synthesis for Safe and Optimized Control of Steerable Needles. - Sascha Lehmann; Antje Rogalla; Maximilian Neidhardt; Alexander Schlaefer; Sibylle Schupp (FMAS, 2021)

Modeling R3 Needle Steering in Uppaal. - Sascha Lehmann; Antje Rogalla; Maximilian Neidhardt; Anton Reinecke; Alexander Schlaefer; Sibylle Schupp (MARS@ETAPS, 2022)

Bounded DBM-based clock state construction for timed automata in Uppaal. - Sascha Lehmann; Sibylle Schupp (Int. J. Softw. Tools Technol. Transf., 2023)

Mutation Testing of Java Bytecode: A Model-Driven Approach. - Christoph Bockisch; Deniz Eren; Sascha Lehmann; Daniel Neufeld; Gabriele Taentzer (MODELS, 2024)

Advanced Mutation Testing of Java Bytecode Using Model Transformation. - Christoph Bockisch; Freya Dorn; Deniz Eren; Sascha Lehmann; Daniel Neufeld; Gabriele Taentzer (Software Engineering, 2025)

A provably safe controller for the needle-steering problem using online strategy synthesis. - Sascha Lehmann; Antje Rogalla; Maximilian Neidhardt; Alexander Schlaefer; Sibylle Schupp (Sci. Comput. Program., 2025)

A model template for reachability-based containment checking of imprecise observations in timed automata. - Sascha Lehmann; Sibylle Schupp (Softw. Syst. Model., 2025)