Lena Becker, Holger Hermanns:
Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic.
QEST+FORMATS 2026: 284-301
DOI
Open Access
Robin Ohs, Gregory F. Stock, Andreas Schmidt, Juan A. Fraire, Jörg Ott, Holger Hermanns:
Dark Clouds Rising in Low-Earth Orbit: On Environmental Limits to Massive Orbital AI.
SIGCOMM 2026: 1960-1965
DOI
Open Access
Research Data
Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang:
Efficient Decomposition Identification of Deterministic Finite Automata from Examples.
SETTA 2025: 177-195
DOI
Open Access
Hanwei Zhang, Luo Cheng, Rui Wen, Yang Zhang, Lijun Zhang, Holger Hermanns:
SL-CBM: Enhancing Concept Bottleneck Models with Semantic Locality for Better Interpretability.
AAAI 2026: 38093-38101
DOI
Open Access
Nick Waddoups, Jonah Boe, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, Zhen Zhang:
Probabilistic Verification for Modular Network-on-Chip Systems.
VMCAI 2026: 383-407
DOI
Open Access
Research Data
Camilo J. Rojas, Fabio Patrone, Juan A. Fraire, Mario Marchese:
From emerging LEO satellite constellations to the space cloud: Emulation platforms and orchestration methods.
Comput. Networks 276: 111970 (2026)
DOI
Open Access
Gregory F. Stock, Alexander Haberl, Juan A. Fraire, Holger Hermanns:
POMDP-Based Routing for DTNs with Partial Knowledge and Dependent Failures.
WiSEE 2025
DOI
Open Access
Valentin Negrelli, Renato Cherini, Juan A. Fraire:
Deep Reinforcement Learning for Routing in Uncertain DTNs with Graph Neural Networks.
WiSEE 2025
DOI
Open Access
Arnd Hartmanns, Robert Modderman:
DTMC Model Checking by Path Abstraction Revisited.
RP 2025: 186-201
DOI
Open Access
Timo P. Gros, Arnd Hartmanns, Ivo Hoese, Joshua Meyer, Nicola J. Müller, Verena Wolf:
PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface.
QEST+FORMATS 2025: 134-156
DOI
Open Access
Research Data
Gabriel Dengler, Carlos E. Budde, Laura Carnevali, Arnd Hartmanns:
Time-Sensitive Importance Splitting.
QEST+FORMATS 2025: 21-41
DOI
Open Access
Research Data
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft:
Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality.
QEST+FORMATS 2025: 83-94
DOI
Open Access
Research Data
Arnd Hartmanns:
An Overview of Sound and Modest Approaches to Quantitative Model Checking from Sea to Space.
FMICS 2025: 21-36
DOI
Open Access
Jan Friso Groote, David N. Jansen:
A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity.
CONCUR 2025: 18:1-18:16
DOI
Open 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)
DOI
Open Access
Research 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
DOI
Open Access
Research Data
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich:
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs.
CAV (2) 2025: 122-146
DOI
Open Access
Research Data
Alexander Bork, Joost-Pieter Katoen, Tim Quatmann, Svenja Stein:
Multi-Cost-Bounded Reachability Analysis of POMDPs.
UAI 2025: 355-387
URL
Open Access
Research Data
Reza Soltani, Pablo Diale, Milan Lopuhaä‑Zwakenberg, Mariëlle Stoelinga:
Safety and Security Risk Mitigation in Satellite Missions via Attack‑Fault‑Defense Trees.
ESREL SRA-E 2025
DOI
Open Access
Mathis Niehage, Carina da Silva, Anne Remke, Arnd Hartmanns:
Rare Event Simulation for Stochastic Hybrid Systems Using Symbolic Importance Functions.
NFM 2025: 254-274
DOI
Open 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
DOI
Open Access
Research 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.
Int. J. Softw. Tools Technol. Transf. 27(3): 361-376 (2025)
DOI
Open Access
Research Data
Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns, Fernando D. Raverta:
Comparing Statistical, Analytical, and Learning-Based Routing Approaches for Delay-Tolerant Networks.
ACM Trans. Model. Comput. Simul. 35(2): 10:1-10:26 (2025)
DOI
Open Access
Research Data
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
DOI
Open Access
Research 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
DOI
Open Access
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler:
J-P: MDP. FP. PP.
LNCS 15260: 255-302
DOI
Open 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
DOI
Open 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
DOI
Open 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)
DOI
Open Access
Arnd Hartmanns, Bram Kohlen, Peter Lammich:
Efficient Formally Verified Maximal End Component Decomposition for MDPs.
FM (1) 2024: 206-225
DOI
Open Access
Research Data
Song Gao, Bohua Zhan, Zhilin Wu, Lijun Zhang:
Verifying Randomized Consensus Protocols with Common Coins.
DSN 2024: 403-415
DOI
Open 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
DOI
Open Access
Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying:
Measurement-Based Verification of Quantum Markov Chains.
CAV (3) 2024: 533-554
DOI
Open Access
Renjue Li, Tianhang Qin, Cas Widdershoven:
ISS-Scenario: Scenario-Based Testing in CARLA.
TASE 2024: 279-286
DOI
Open Access
Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Fuzzy quantitative attack tree analysis.
FASE 2024: 210-231
DOI
Open Access
Milan Lopuhaä-Zwakenberg, Jasper Goseling:
Mechanisms for Robust Local Differential Privacy.
Entropy 26(3): 233 (2024)
DOI
Open Access
Milan Lopuhaä-Zwakenberg:
Fault Tree Reliability Analysis via Squarefree Polynomials.
MODELSWARD 2024: 39-49
DOI
Open Access
Research 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)
DOI
Open Access
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)
DOI
Open 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
DOI
Open Access
Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Attack time analysis in dynamic attack trees via integer linear programming.
SEFM 2023: 165-183
DOI
Open Access
Ying Liu, Andrea Turrini, Ernst Moritz Hahn, Bai Xue, Lijun Zhang:
Scenario Approach for Parametric Markov Models.
ATVA (1) 2023: 158-180
DOI
Open Access
Research Data
Arnd Hartmanns, Bram Kohlen, Peter Lammich:
Fast Verified SCCs for Probabilistic Model Checking.
ATVA (1) 2023: 181-202
DOI
Open Access
Research 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
DOI
Open Access
Research 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
DOI
Open 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
URL
Open Access
Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga:
Cost-damage analysis of attack trees.
DSN 2023: 545-558
DOI
Open Access
Tobias Winkler, Joost-Pieter Katoen:
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata.
LICS 2023
DOI
Open 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
DOI
Open Access
Research Data
Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger:
A Practitioner's Guide to MDP Model Checking Algorithms.
TACAS (1) 2023: 469-488
DOI
Open Access
Research 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
DOI
Open 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)
DOI
Open 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)
DOI
Open Access
Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler:
Stochastic games with lexicographic objectives.
Formal Methods Syst. Des. (2023)
DOI
Open Access
Research 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)
DOI
Open Access
Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, Ernst Moritz Hahn, Mariëlle Stoelinga:
PFL: A Probabilistic Logic for Fault Trees.
FM 2023: 199-221
DOI
Open Access
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen:
Exact Probabilistic Inference Using Generating Functions.
LAFI 2023
URL
Open Access
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
DOI
Open 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)
DOI
Open Access
Research 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
DOI
Open Access
Arnd Hartmanns, Michaela Klauck:
The Modest State of Learning, Sampling, and Verifying Strategies.
ISoLA (3) 2022: 406-432
DOI
Open Access
Research Data
Gregory Stock, Juan A. Fraire, Holger Hermanns:
Distributed On-Demand Routing for LEO Mega-Constellations: A Starlink Case Study.
ASMS/SPSC 2022
DOI
Open Access
Juan A. Fraire, Oana Iova, Fabrice Valois:
Space-Terrestrial Integrated IoT: Challenges and Opportunities.
IEEE Commun. Mag. 60(12): 64-70 (2022)
DOI
Open 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
DOI
Open Access
Research 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
DOI
Open 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
DOI
Open 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
DOI
Open Access
Research 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
DOI
Open 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
DOI
Open Access
Research Data
Stefano M. Nicoletti, Ernst Moritz Hahn, Mariëlle Stoelinga:
BFL: a Logic to Reason about Fault Trees.
DSN 2022: 441-452
DOI
Open 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)
DOI
Open 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
DOI
Open Access
Research 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
DOI
Open Access
Research Data
Arnd Hartmanns:
Correct Probabilistic Model Checking with Floating-Point Arithmetic.
TACAS (2) 2022: 41-59
DOI
Open Access
Research Data
Sebastian Biewer, Holger Hermanns:
On the Detection of Doped Software by Falsification.
FASE 2022: 71-91
DOI
Open Access
Arnd Hartmanns:
An Overview of Modest Models and Tools for Real Stochastic Timed Systems.
MARS@ETAPS 2022
DOI
Open Access
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)
DOI
Open Access