Publications

2025

Jan Friso Groote, David N. Jansen:
A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity.
CONCUR 2025: 18:1-18:16
DOIOpen Access

Robin Ohs, Gregory F. Stock, Andreas Schmidt, Juan A. Fraire, Holger Hermanns:
Dirty Bits in Low-Earth Orbit: The Carbon Footprint of Launching Computers.
ACM SIGEnergy Energy Inform. Rev. 5(2): 26-33 (2025)
DOIOpen AccessResearch Data

Robin Ohs, Gregory F. Stock, Juan A. Fraire, Holger Hermanns, Andreas Schmidt:
PhantomLink: Emulating Virtual End-to-End Links on Ground and in Orbit.
ANRW 2025: 39-46
DOIOpen AccessResearch Data

Alexander Bork, Joost-Pieter Katoen, Tim Quatmann, Svenja Stein:
Multi-Cost-Bounded Reachability Analysis of POMDPs.
UAI 2025: 355-387
URLOpen AccessResearch Data

Mathis Niehage, Carina da Silva, Anne Remke, Arnd Hartmanns:
Rare Event Simulation for Stochastic Hybrid Systems Using Symbolic Importance Functions.
NFM 2025: 254-274
DOIOpen Access

Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft:
Sound Statistical Model Checking for Probabilities and Expected Rewards.
TACAS (1) 2025: 167-190
DOIOpen AccessResearch Data

2024

Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns:
Digging for Decision Trees: A Case Study in Strategy Sampling and Learning.
AISoLA 2024: 354-378
DOIOpen AccessResearch Data

Felix Walter, Marius Feldmann, Juan A. Fraire, Scott Burleigh:
The Architectural Refinement of μD3TN: Toward a Software-Defined DTN Protocol Stack.
SMC-IT 2024: 161-170
DOIOpen Access

Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler:
J-P: MDP. FP. PP.
LNCS 15260: 255-302
DOIOpen Access

Carlos E. Budde, Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns, Zhen Zhang:
Modest Models and Tools for Real Stochastic Timed Systems.
LNCS 15261: 115-142
DOIOpen Access

Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Ceska, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Kretínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang:
Tools at the Frontiers of Quantitative Verification – QComp 2023 Competition Report.
TOOLympics@ETAPS 2023: 90-146
DOIOpen Access

Juan A. Fraire, Santiago Henn, Gregory Stock, Robin Ohs, Holger Hermanns, Felix Walter, Lynn Van Broock, Gabriel Ruffini, Federico Machado, Pablo Serratti, Jose Relloso:
Quantitative analysis of segmented satellite network architectures: A maritime surveillance case study.
Comput. Networks 255: 110874 (2024)
DOIOpen Access

Arnd Hartmanns, Bram Kohlen, Peter Lammich:
Efficient Formally Verified Maximal End Component Decomposition for MDPs.
FM (1) 2024: 206-225
DOIOpen AccessResearch Data

Song Gao, Bohua Zhan, Zhilin Wu, Lijun Zhang:
Verifying Randomized Consensus Protocols with Common Coins.
DSN 2024: 403-415
DOIOpen Access

Gregory Stock, Juan A. Fraire, Santiago Henn, Holger Hermanns, Andreas Schmidt:
A Stability-first Approach to Running TCP over Starlink.
ICC Workshops 2024: 1708-1713
DOIOpen Access

Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying:
Measurement-Based Verification of Quantum Markov Chains.
CAV (3) 2024: 533-554
DOIOpen Access

Renjue Li, Tianhang Qin, Cas Widdershoven:
ISS-Scenario: Scenario-Based Testing in CARLA.
TASE 2024: 279-286
DOIOpen Access

Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Fuzzy quantitative attack tree analysis.
FASE 2024: 210-231
DOIOpen Access

Milan Lopuhaä-Zwakenberg, Jasper Goseling:
Mechanisms for Robust Local Differential Privacy.
Entropy 26(3): 233 (2024)
DOIOpen Access

Milan Lopuhaä-Zwakenberg:
Fault Tree Reliability Analysis via Squarefree Polynomials.
MODELSWARD 2024: 39-49
DOIOpen AccessResearch Data

Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk:
Parameter synthesis for Markov models: covering the parameter space.
Formal Methods Syst. Des. 62(1): 181-259 (2024)
DOIOpen Access

2023

Qiongxiu Li, Jaron Skovsted Gundersen, Milan Lopuhaä-Zwakenberg, Richard Heusdens:
Adaptive Differentially Quantized Subspace Perturbation (ADQSP): A Unified Framework for Privacy-Preserving Distributed Average Consensus.
IEEE Trans. Inf. Forensics Secur. 19: 1780-1793 (2024)
DOIOpen Access

Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn, Mariëlle Stoelinga:
ATM: A Logic for Quantitative Security Properties on Attack Trees.
SEFM 2023: 205-225
DOIOpen Access

Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Attack time analysis in dynamic attack trees via integer linear programming.
SEFM 2023: 165-183
DOIOpen Access

Ying Liu, Andrea Turrini, Ernst Moritz Hahn, Bai Xue, Lijun Zhang:
Scenario Approach for Parametric Markov Models.
ATVA (1) 2023: 158-180
DOIOpen AccessResearch Data

Arnd Hartmanns, Bram Kohlen, Peter Lammich:
Fast Verified SCCs for Probabilistic Model Checking.
ATVA (1) 2023: 181-202
DOIOpen AccessResearch Data

Reza Soltani, Matthias Volk, Leonardo Diamonte, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors.
FMICS 2023: 205-223
DOIOpen AccessResearch Data

Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele:
Quantifying Masking Fault-Tolerance via Fair Stochastic Games.
EXPRESS/SOS 2023: 132-148
DOIOpen Access

Stefano M. Nicoletti, Mattia Fumagalli, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn, Giancarlo Guizzardi, Mariëlle Stoelinga:
Property Specification and Models for Risk: Towards Risk Propagation Graphs.
SAFECOMP 2023 Position Papers
URLOpen Access

Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Cost-damage analysis of attack trees.
DSN 2023: 545-558
DOIOpen Access

Tobias Winkler, Joost-Pieter Katoen:
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata.
LICS 2023: 1-13
DOIOpen Access

Vojtech Havlena, Ondrej Lengál, Yong Li, Barbora Smahlíková, Andrea Turrini:
Modular Mix-and-Match Complementation of Büchi Automata.
TACAS (1) 2023: 249-270
DOIOpen AccessResearch Data

Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger:
A Practitioner's Guide to MDP Model Checking Algorithms.
TACAS (1) 2023: 469-488
DOIOpen AccessResearch Data

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja:
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.
TACAS (2) 2023: 410-429
DOIOpen Access

Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan:
Lower Bounds for Possibly Divergent Probabilistic Programs.
Proc. ACM Program. Lang. 7(OOPSLA1): 696-726 (2023)
DOIOpen Access

Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang:
On the Power of Finite Ambiguity in Büchi Complementation.
Inf. Comput. 292: 105032 (2023)
DOIOpen Access

Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler:
Stochastic games with lexicographic objectives.
Formal Methods Syst. Des. (2023)
DOIOpen AccessResearch Data

Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál, Andrea Turrini:
A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions.
J. Syst. Softw. 201: 111673 (2023)
DOIOpen Access

Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, Ernst Moritz Hahn, Mariëlle Stoelinga:
PFL: A Probabilistic Logic for Fault Trees.
FM 2023: 199-221
DOIOpen Access

Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen:
Exact Probabilistic Inference Using Generating Functions.
LAFI 2023
URLOpen Access

2022

Milan Lopuhaä-Zwakenberg, Boris Škorić, Ninghui Li:
Fisher Information as a Utility Metric for Frequency Estimation under Local Differential Privacy.
WPES@CCS 2022: 41-53
DOIOpen Access

Carlos E. Budde, Pedro R. D'Argenio, Raúl E. Monti, Mariëlle Stoelinga:
Analysis of non-Markovian repairable fault trees through rare event simulation.
Int. J. Softw. Tools Technol. Transf. 24(5): 821-841 (2022)
DOIOpen AccessResearch Data

Qiongxiu Li, Milan Lopuhaä-Zwakenberg, Richard Heusdens, Mads Græsbøll Christensen:
Two for the price of one: communication efficient and privacy-preserving distributed average consensus using quantization.
EUSIPCO 2022: 2166-2170
DOIOpen Access

Arnd Hartmanns, Michaela Klauck:
The Modest State of Learning, Sampling, and Verifying Strategies.
ISoLA (3) 2022: 406-432
DOIOpen AccessResearch Data

Gregory Stock, Juan A. Fraire, Holger Hermanns:
Distributed On-Demand Routing for LEO Mega-Constellations: A Starlink Case Study.
ASMS/SPSC 2022: 1-8
DOIOpen Access

Juan A. Fraire, Oana Iova, Fabrice Valois:
Space-Terrestrial Integrated IoT: Challenges and Opportunities.
IEEE Commun. Mag. 60(12): 64-70 (2022)
DOIOpen Access

Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns, Fernando D. Raverta:
Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks.
QEST 2022: 337-355
DOIOpen AccessResearch Data

Juan A. Fraire, Pablo Madoery, Mehdi Ait Mesbah, Oana Iova, Fabrice Valois:
Simulating LoRa-Based Direct-to-Satellite IoT Networks with FLoRaSat.
WoWMoM 2022: 464-470
DOIOpen Access

Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler:
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions.
CAV (1) 2022: 79-101
DOIOpen Access

Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang:
Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition.
CAV (2) 2022: 152-173
DOIOpen AccessResearch Data

Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele:
Playing Against Fair Adversaries in Stochastic Games with Total Rewards.
CAV (2) 2022: 48-69
DOIOpen Access

Thom S. Badings, Nils Jansen, Sebastian Junges, Mariëlle Stoelinga, Matthias Volk:
Sampling-Based Verification of CTMCs with Uncertain Rates.
CAV (2) 2022: 26-47
DOIOpen AccessResearch Data

Stefano M. Nicoletti, Ernst Moritz Hahn, Mariëlle Stoelinga:
BFL: a Logic to Reason about Fault Trees.
DSN 2022: 441-452
DOIOpen Access

Guido Álvarez, Juan A. Fraire, Khaled Abdelfadeel Hassan, Sandra Céspedes, Dirk Pesch:
Uplink Transmission Policies for LoRa-Based Direct-to-Satellite IoT.
IEEE Access 10: 72687-72701 (2022)
DOIOpen Access

Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga:
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees.
NFM 2022:713-732
DOIOpen AccessResearch Data

Luciano Putruele, Ramiro Demasi, Pablo F. Castro, Pedro R. D'Argenio:
MaskD: A Tool for Measuring Masking Fault-Tolerance.
TACAS (1) 2022: 396-403
DOIOpen AccessResearch Data

Arnd Hartmanns:
Correct Probabilistic Model Checking with Floating-Point Arithmetic.
TACAS (2) 2022: 41-59
DOIOpen AccessResearch Data

Sebastian Biewer, Holger Hermanns:
On the Detection of Doped Software by Falsification.
FASE 2022: 71-91
DOIOpen Access

Arnd Hartmanns:
An Overview of Modest Models and Tools for Real Stochastic Timed Systems.
MARS@ETAPS 2022
DOIOpen Access

2021

Raydel Ortigueira, Juan A. Fraire, Alex Becerra, Tomás Ferrer, Sandra Céspedes:
RESS-IoT: A scalable energy-efficient MAC protocol for direct-to-satellite IoT.
IEEE Access 9: 164440-164453 (2021)
DOIOpen Access