SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). - Florian Corzilius; Ulrich Loup; Sebastian Junges; Erika Ábrahám (SAT, 2012)

On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. - Sebastian Junges; Ulrich Loup; Florian Corzilius; Erika Ábrahám (CAI, 2013)

A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models. - Dimitri Bohlender; Harold Bruintjes; Sebastian Junges; Jens Katelaan; Viet Yen Nguyen; Thomas Noll 001 (ISoLA (2), 2014)

PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. - Christian Dehnert; Sebastian Junges; Nils Jansen 001; Florian Corzilius; Matthias Volk 001; Harold Bruintjes; Joost-Pieter Katoen; Erika Ábrahám (CAV (1), 2015)

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. - Florian Corzilius; Gereon Kremer; Sebastian Junges; Stefan Schupp; Erika Ábrahám (SAT, 2015)

Probabilistic Verification for Cognitive Models. - Sebastian Junges; Nils Jansen 001; Joost-Pieter Katoen; Ufuk Topcu (AAAI Fall Symposia, 2016)

Parameter Synthesis for Markov Models: Faster Than Ever. - Tim Quatmann; Christian Dehnert; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (ATVA, 2016)

Uncovering Dynamic Fault Trees. - Sebastian Junges; Dennis Guck; Joost-Pieter Katoen; Mariëlle Stoelinga (DSN, 2016)

Parameter Synthesis for Probabilistic Systems. - Christian Dehnert; Sebastian Junges; Nils Jansen 001; Florian Corzilius; Matthias Volk 001; Joost-Pieter Katoen; Erika Ábrahám; Harold Bruintjes (MBMV, 2016)

Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates. - Matthias Volk 001; Sebastian Junges; Joost-Pieter Katoen (SAFECOMP, 2016)

Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks. - Christian Dombrowski; Sebastian Junges; Joost-Pieter Katoen; James Gross (SRDS, 2016)

Safety-Constrained Reinforcement Learning for MDPs. - Sebastian Junges; Nils Jansen 001; Christian Dehnert; Ufuk Topcu; Joost-Pieter Katoen (TACAS, 2016)

Advancing Dynamic Fault Tree Analysis. - Matthias Volk 001; Sebastian Junges; Joost-Pieter Katoen (CoRR, 2016)

The Probabilistic Model Checker Storm (Extended Abstract). - Christian Dehnert; Sebastian Junges; Joost-Pieter Katoen; Matthias Volk 001 (CoRR, 2016)

Probabilistic Model Checking for Complex Cognitive Tasks - A case study in human-robot interaction. - Sebastian Junges; Nils Jansen 001; Joost-Pieter Katoen; Ufuk Topcu (CoRR, 2016)

A Storm is Coming: A Modern Probabilistic Model Checker. - Christian Dehnert; Sebastian Junges; Joost-Pieter Katoen; Matthias Volk 001 (CAV (2), 2017)

Motion planning under partial observability using game-based abstraction. - Leonore Winterer; Sebastian Junges; Ralf Wimmer 001; Nils Jansen 001; Ufuk Topcu; Joost-Pieter Katoen; Bernd Becker 001 (CDC, 2017)

Model-Based Safety Analysis for Vehicle Guidance Systems. - Majdi Ghadhab; Sebastian Junges; Joost-Pieter Katoen; Matthias Kuntz; Matthias Volk 001 (SAFECOMP, 2017)

JANI: Quantitative Model and Tool Interaction. - Carlos E. Budde; Christian Dehnert; Ernst Moritz Hahn; Arnd Hartmanns; Sebastian Junges; Andrea Turrini (TACAS (2), 2017)

Sequential Convex Programming for the Efficient Verification of Parametric MDPs. - Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ivan Papusha; Hasan A. Poonawala; Ufuk Topcu (TACAS (2), 2017)

Permissive Finite-State Controllers of POMDPs using Parameter Synthesis. - Sebastian Junges; Nils Jansen 001; Ralf Wimmer 001; Tim Quatmann; Leonore Winterer; Joost-Pieter Katoen; Bernd Becker 001 (CoRR, 2017)

Fault trees on a diet: automated reduction by graph rewriting. - Sebastian Junges; Dennis Guck; Joost-Pieter Katoen; Arend Rensink; Mariëlle Stoelinga (Formal Aspects Comput., 2017)

One Net Fits All - A Unifying Semantics of Dynamic Fault Trees Using GSPNs. - Sebastian Junges; Joost-Pieter Katoen; Mariëlle Stoelinga; Matthias Volk 001 (Petri Nets, 2018)

Synthesis in pMDPs: A Tale of 1001 Parameters. - Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (ATVA, 2018)

Abstraktions-basierte Verifikation von POMDPs im Motion-Planning-Kontext. - Leonore Winterer; Sebastian Junges; Ralf Wimmer 001; Nils Jansen 001; Ufuk Topcu; Joost-Pieter Katoen; Bernd Becker 001 (MBMV, 2018)

Model Checking for Safe Navigation Among Humans. - Sebastian Junges; Nils Jansen 001; Joost-Pieter Katoen; Ufuk Topcu; Ruohan Zhang; Mary M. Hayhoe (QEST, 2018)

Multi-cost Bounded Reachability in MDP. - Arnd Hartmanns; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann (TACAS (2), 2018)

Finite-State Controllers of POMDPs using Parameter Synthesis. - Sebastian Junges; Nils Jansen 001; Ralf Wimmer 001; Tim Quatmann; Leonore Winterer; Joost-Pieter Katoen; Bernd Becker 001 (UAI, 2018)

Shielded Decision-Making in MDPs. - Nils Jansen 001; Bettina Könighofer; Sebastian Junges; Roderick Bloem (CoRR, 2018)

The Partially Observable Games We Play for Cyber Deception. - Mohamadreza Ahmadi; Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (CoRR, 2018)

Fast Dynamic Fault Tree Analysis by Model Checking Techniques. - Matthias Volk 001; Sebastian Junges; Joost-Pieter Katoen (IEEE Trans. Ind. Informatics, 2018)

Are Parametric Markov Chains Monotonic? - Jip Spel; Sebastian Junges; Joost-Pieter Katoen (ATVA, 2019)

Model Repair Revamped - - On the Automated Synthesis of Markov Chains -. - Milan Ceska 002; Christian Dehnert; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (From Reactive Systems to Cyber-Physical Systems, 2019)

Counterexample-Driven Synthesis for Probabilistic Program Sketches. - Milan Ceska 002; Christian Hensel; Sebastian Junges; Joost-Pieter Katoen (FM, 2019)

Correct-by-construction policies for POMDPs. - Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann; Bernd Becker 001; Ralf Wimmer 001; Leonore Winterer (SNR, 2019)

Shepherding Hordes of Markov Chains. - Milan Ceska 002; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (TACAS (2), 2019)

Parameter Synthesis for Markov Models. - Sebastian Junges; Erika Ábrahám; Christian Hensel; Nils Jansen 001; Joost-Pieter Katoen; Tim Quatmann; Matthias Volk 001 (CoRR, 2019)

Safety analysis for vehicle guidance systems with dynamic fault trees. - Majdi Ghadhab; Sebastian Junges; Joost-Pieter Katoen; Matthias Kuntz; Matthias Volk 001 (Reliab. Eng. Syst. Saf., 2019)

Verification of Indefinite-Horizon POMDPs. - Alexander Bork; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann (ATVA, 2020)

PrIC3: Property Directed Reachability for MDPs. - Kevin Batz; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer (CAV (2), 2020)

Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper). - Nils Jansen 001; Bettina Könighofer; Sebastian Junges; Alex Serban; Roderick Bloem (CONCUR, 2020)

Scenario-Based Verification of Uncertain MDPs. - Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (TACAS (1), 2020)

Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. - Christel Baier; Christian Hensel; Lisa Hutschenreiter; Sebastian Junges; Joost-Pieter Katoen; Joachim Klein 001 (Inf. Comput., 2020)

Multi-cost Bounded Tradeoff Analysis in MDP. - Arnd Hartmanns; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann (J. Autom. Reason., 2020)

Parameter synthesis in Markov models. - Sebastian Junges (2020)

Synthese im Kontext Parametrischer Markow-Modelle. - Sebastian Junges (Ausgezeichnete Informatikdissertationen, 2020)

Robust Finite-State Controllers for Uncertain POMDPs. - Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Ahmadreza Marandi; Marnix Suilen; Ufuk Topcu (AAAI, 2021)

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Simon Stupinský (CAV (1), 2021)

Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. - Steven Holtzen; Sebastian Junges; Marcell Vazquez-Chanlatte; Todd D. Millstein; Sanjit A. Seshia; Guy Van den Broeck (CAV (2), 2021)

Enforcing Almost-Sure Reachability in POMDPs. - Sebastian Junges; Nils Jansen 001; Sanjit A. Seshia (CAV (2), 2021)

Runtime Monitors for Markov Decision Processes. - Sebastian Junges; Hazem Torfah; Sanjit A. Seshia (CAV (2), 2021)

Entropy-Guided Control Improvisation. - Marcell Vazquez-Chanlatte; Sebastian Junges; Daniel J. Fremont; Sanjit Seshia (Robotics: Science and Systems, 2021)

Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance. - Hazem Torfah; Sebastian Junges; Daniel J. Fremont; Sanjit A. Seshia (RV, 2021)

Inductive Synthesis for Probabilistic Programs Reaches New Horizons. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen (TACAS (1), 2021)

Finding Provably Optimal Markov Chains. - Jip Spel; Sebastian Junges; Joost-Pieter Katoen (TACAS (1), 2021)

Runtime Monitoring for Markov Decision Processes. - Sebastian Junges; Hazem Torfah; Sanjit A. Seshia (CoRR, 2021)

Counterexample-guided inductive synthesis for probabilistic systems. - Milan Ceska 002; Christian Hensel; Sebastian Junges; Joost-Pieter Katoen (Formal Aspects Comput., 2021)

The complexity of reachability in parametric Markov decision processes. - Sebastian Junges; Joost-Pieter Katoen; Guillermo A. Pérez 001; Tobias Winkler 001 (J. Comput. Syst. Sci., 2021)

Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions. - Leonore Winterer; Sebastian Junges; Ralf Wimmer 001; Nils Jansen 001; Ufuk Topcu; Joost-Pieter Katoen; Bernd Becker 001 (IEEE Trans. Autom. Control., 2021)

Experiments for 'Model Checking Finite-Horizon Markov Chains with Probabilistic Inference'. - Steven Holtzen; Sebastian Junges; Marcell Vazquez-Chanlatte; Todd D. Millstein; Sanjit A. Seshia; Guy Van den Broeck (Zenodo, 2021)

Experiments for 'Enforcing Almost-Sure Reachability in POMDPs'. - Sebastian Junges; Nils Jansen 001; Sanjit A. Seshia (Zenodo, 2021)

Experiments for 'Enforcing Almost-Sure Reachability in POMDPs'. - Sebastian Junges; Nils Jansen 001; Sanjit A. Seshia (Zenodo, 2021)

Experiments for 'Runtime Monitoring for Markov Decision Processes'. - Sebastian Junges; Hazem Torfah; Sanjit A. Seshia (Zenodo, 2021)

Gradient-Descent for Randomized Controllers under Partial Observability (Artifact). - Linus Heck; Jip Spel; Sebastian Junges; Joshua Moerman; Joost-Pieter Katoen (Zenodo, 2021)

Learning Monitorable Operational Design Domains for Assured Autonomy. - Hazem Torfah; Carol Xie; Sebastian Junges; Marcell Vazquez-Chanlatte; Sanjit A. Seshia (ATVA, 2022)

Parameter Synthesis in Markov Models: A Gentle Survey. - Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (Principles of Systems Design, 2022)

Learning Language Intersections. - Sebastian Junges; Jurriaan Rot (A Journey from Process Algebra via Timed Automata to Model Learning, 2022)

Sampling-Based Verification of CTMCs with Uncertain Rates. - Thom S. Badings; Nils Jansen 001; Sebastian Junges; Mariëlle Stoelinga; Matthias Volk 001 (CAV (2), 2022)

Abstraction-Refinement for Hierarchical Probabilistic Models. - Sebastian Junges; Matthijs T. J. Spaan (CAV (1), 2022)

Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. - Edward Kim 005; Jay Shenoy; Sebastian Junges; Daniel J. Fremont; Alberto L. Sangiovanni-Vincentelli; Sanjit A. Seshia (ICCPS, 2022)

Demo: Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. - Edward Kim 005; Jay Shenoy; Sebastian Junges; Daniel J. Fremont; Alberto L. Sangiovanni-Vincentelli; Sanjit A. Seshia (ICCPS, 2022)

COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking. - Dennis Gross; Nils Jansen 001; Sebastian Junges; Guillermo A. Pérez 001 (SETTA, 2022)

Inductive synthesis of finite-state controllers for POMDPs. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen (UAI, 2022)

Gradient-Descent for Randomized Controllers Under Partial Observability. - Linus Heck; Jip Spel; Sebastian Junges; Joshua Moerman; Joost-Pieter Katoen (VMCAI, 2022)

Safe Reinforcement Learning via Shielding for POMDPs. - Steven Carr 002; Nils Jansen 001; Sebastian Junges; Ufuk Topcu (CoRR, 2022)

Scenario-based verification of uncertain parametric MDPs. - Thom S. Badings; Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (Int. J. Softw. Tools Technol. Transf., 2022)

The probabilistic model checker Storm. - Christian Hensel; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann; Matthias Volk 001 (Int. J. Softw. Tools Technol. Transf., 2022)

Convex Optimization for Parameter Synthesis in MDPs. - Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (IEEE Trans. Autom. Control., 2022)

Markov automata with multiple objectives. - Tim Quatmann; Sebastian Junges; Joost-Pieter Katoen (Formal Methods Syst. Des., 2022)

Finding Provably Optimal Markov Chains (Artifact). - Jip Spel; Sebastian Junges; Joost-Pieter Katoen (Zenodo, 2022)

Experiments for 'Sampling-Based Verification of CTMCs with Uncertain Rates'. - Thom S. Badings; Sebastian Junges; Nils Jansen 001; Mariëlle Stoelinga; Matthias Volk 001 (Zenodo, 2022)

Experiments for 'Scenario-Based Verification of Uncertain Parametric MDPs'. - Thom S. Badings; Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (Zenodo, 2022)

Experiments for 'Scenario-Based Verification of Uncertain Parametric MDPs'. - Thom S. Badings; Murat Cubuktepe; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Ufuk Topcu (Zenodo, 2022)

Experiments for 'Sampling-Based Verification of CTMCs with Uncertain Rates'. - Thom S. Badings; Nils Jansen 001; Sebastian Junges; Mariëlle Stoelinga; Matthias Volk 001 (Zenodo, 2022)

Safe Reinforcement Learning via Shielding under Partial Observability. - Steven Carr 002; Nils Jansen 001; Sebastian Junges; Ufuk Topcu (AAAI, 2023)

Search and Explore: Symbiotic Policy Synthesis in POMDPs. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (CAV (3), 2023)

Efficient Sensitivity Analysis for Parametric Robust Markov Chains. - Thom S. Badings; Sebastian Junges; Ahmadreza Marandi; Ufuk Topcu; Nils Jansen 001 (CAV (3), 2023)

Recursive Small-Step Multi-Agent A* for Dec-POMDPs. - Wietze Koops; Nils Jansen 001; Sebastian Junges; Thiago D. Simão (IJCAI, 2023)

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

A Practitioner's Guide to MDP Model Checking Algorithms. - Arnd Hartmanns; Sebastian Junges; Tim Quatmann; Maximilian Weininger (TACAS (1), 2023)

Robust Almost-Sure Reachability in Multi-Environment MDPs. - Marck van der Vegt; Nils Jansen 001; Sebastian Junges (TACAS (1), 2023)

Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (TOOLympics@ETAPS, 2023)

Scalable Analysis of Probabilistic Models and Programs (Dagstuhl Seminar 23241). - Sebastian Junges; Joost-Pieter Katoen; Scott Sanner; Guy Van den Broeck; Bahare Salmani (Dagstuhl Reports, 2023)

Robust Almost-Sure Reachability in Multi-Environment MDPs: Supplemental Material. - Marck van der Vegt; Nils Jansen 001; Sebastian Junges (Zenodo, 2023)

Robust Almost-Sure Reachability in Multi-Environment MDPs: Supplemental Material. - Marck van der Vegt; Nils Jansen 001; Sebastian Junges (Zenodo, 2023)

Artifact supplement for 'Search and Explore: Symbiotic Policy Synthesis in POMDPs'. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2023)

Artifact supplement for 'Search and Explore: Symbiotic Policy Synthesis in POMDPs'. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2023)

Artifact supplement for 'Search and Explore: Symbiotic Policy Synthesis in POMDPs'. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2023)

Experiments for 'Efficient Sensitivity Analysis for Parametric Robust Markov Chains'. - Thom S. Badings; Sebastian Junges; Ahmadreza Marandi; Ufuk Topcu; Nils Jansen 001 (Zenodo, 2023)

Experiments for 'Efficient Sensitivity Analysis for Parametric Robust Markov Chains'. - Thom S. Badings; Sebastian Junges; Ahmadreza Marandi; Ufuk Topcu; Nils Jansen 001 (Zenodo, 2023)

Supplementary Material for "Recursive Small-Step Multi-Agent A* for Dec-POMDPs". - Wietze Koops; Nils Jansen 001; Sebastian Junges; Thiago D. Simão (Zenodo, 2023)

Artifact for "CTMCs with Imprecisely Timed Observations". - Thom S. Badings; Matthias Volk 001; Sebastian Junges; Mariëlle Stoelinga; Nils Jansen 001 (Zenodo, 2023)

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs: Supplemental Material. - Kazuki Watanabe 003; Marck van der Vegt; Ichiro Hasuo; Jurriaan Rot; Sebastian Junges (Zenodo, 2023)

Factored Online Planning in Many-Agent POMDPs. - Maris F. L. Galesloot; Thiago D. Simão; Sebastian Junges; Nils Jansen 001 (AAAI, 2024)

Policies Grow on Trees: Model Checking Families of MDPs. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Filip Macák (ATVA (2), 2024)

Riding the Storm in a Probabilistic Model Checking Landscape. - Christian Hensel; Sebastian Junges; Tim Quatmann; Matthias Volk 001 (Principles of Verification (2), 2024)

Relating Apartness and Branching Bisimulation Games. - Jurriaan Rot; Sebastian Junges; Harsh Beohar (Logics and Type Systems in Theory and Practice, 2024)

Compositional Value Iteration with Pareto Caching. - Kazuki Watanabe 003; Marck van der Vegt; Sebastian Junges; Ichiro Hasuo (CAV (3), 2024)

A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs. - Marnix Suilen; Marck van der Vegt; Sebastian Junges (CONCUR, 2024)

State Matching and Multiple References in Adaptive Active Automata Learning. - Loes Kruger; Sebastian Junges; Jurriaan Rot (FM (1), 2024)

Active Learning of Runtime Monitors Under Uncertainty. - Sebastian Junges; Sanjit A. Seshia; Hazem Torfah (IFM, 2024)

Imprecise Probabilities Meet Partial Observability: Game Semantics for Robust POMDPs. - Eline M. Bovy; Marnix Suilen; Sebastian Junges; Nils Jansen 001 (IJCAI, 2024)

Approximate Dec-POMDP Solving Using Multi-Agent A*. - Wietze Koops; Sebastian Junges; Nils Jansen 001 (IJCAI, 2024)

CTMCs with Imprecisely Timed Observations. - Thom S. Badings; Matthias Volk 001; Sebastian Junges; Mariëlle Stoelinga; Nils Jansen 001 (TACAS (2), 2024)

Small Test Suites for Active Automata Learning. - Loes Kruger; Sebastian Junges; Jurriaan Rot (TACAS (2), 2024)

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs. - Kazuki Watanabe 003; Marck van der Vegt; Ichiro Hasuo; Jurriaan Rot; Sebastian Junges (TACAS (2), 2024)

Approximate Dec-POMDP Solving Using Multi-Agent A. - Wietze Koops; Sebastian Junges; Nils Jansen 001 (CoRR, 2024)

Tools at the Frontiers of Quantitative Verification. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (CoRR, 2024)

Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies. - Thom S. Badings; Wietze Koops; Sebastian Junges; Nils Jansen 001 (CoRR, 2024)

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs: Supplemental Material. - Kazuki Watanabe 003; Marck van der Vegt; Ichiro Hasuo; Jurriaan Rot; Sebastian Junges (Zenodo, 2024)

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs: Supplemental Material. - Kazuki Watanabe 003; Marck van der Vegt; Ichiro Hasuo; Jurriaan Rot; Sebastian Junges (Zenodo, 2024)

Artifact supplement for 'An Oracle-Guided Approach to Constrained Controller Synthesis Under Uncertainty'. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2024)

Compositional Value Iteration with Pareto Caching: Supplemental Material. - Kazuki Watanabe 003; Marck van der Vegt; Sebastian Junges; Ichiro Hasuo (Zenodo, 2024)

Compositional Value Iteration with Pareto Caching: Supplemental Material. - Kazuki Watanabe 003; Marck van der Vegt; Sebastian Junges; Ichiro Hasuo (Zenodo, 2024)

Compositional Value Iteration with Pareto Caching: Supplemental Material. - Kazuki Watanabe 003; Marck van der Vegt; Sebastian Junges; Ichiro Hasuo (Zenodo, 2024)

Artifact supplement for 'An Oracle-Guided Approach to Constrained Controller Synthesis Under Uncertainty'. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2024)

Artifact supplement for 'An Oracle-Guided Approach to Constrained Controller Synthesis Under Uncertainty'. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2024)

Supplementary Material for "Approximate Dec-POMDP Solving Using Multi-Agent A*". - Wietze Koops; Sebastian Junges; Nils Jansen 001 (Zenodo, 2024)

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

Small Decision Trees for MDPs with Deductive Synthesis. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Filip Macák (CAV (2), 2025)

Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates. - Thom S. Badings; Wietze Koops; Sebastian Junges; Nils Jansen 001 (CAV (2), 2025)

Efficient Probabilistic Model Checking for Relational Reachability. - Lina Gerlach; Tobias Winkler 001; Erika Ábrahám; Borzoo Bonakdarpour; Sebastian Junges (CAV (1), 2025)

Tighter Value-Function Approximations for POMDPs. - Merlijn Krale; Wietze Koops; Sebastian Junges; Thiago D. Simão; Nils Jansen 001 (AAMAS, 2025)

Learning Formal Specifications from Membership and Preference Queries. - Ameesh Shah; Marcell Vazquez-Chanlatte; Sebastian Junges; Sanjit A. Seshia (NeuS, 2025)

Symbiotic Local Search for Small Decision Tree Policies in MDPs. - Roman Andriushchenko; Milan Ceska 002; Debraj Chakraborty 002; Sebastian Junges; Jan Kretínský; Filip Macák (UAI, 2025)

An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty. - Roman Andriushchenko; Milan Ceska 002; Filip Macák; Sebastian Junges; Joost-Pieter Katoen (J. Artif. Intell. Res., 2025)

A Unifying Approach to Product Constructions for Quantitative Temporal Inference. - Kazuki Watanabe 003; Sebastian Junges; Jurriaan Rot; Ichiro Hasuo (Proc. ACM Program. Lang., 2025)

Learning Verified Monitors for Hidden Markov Models. - Luko van der Maas; Sebastian Junges (CoRR, 2025)

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains. - Linus Heck; Tim Quatmann; Jip Spel; Joost-Pieter Katoen; Sebastian Junges (CoRR, 2025)

rfPG: Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs. - Maris F. L. Galesloot; Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Nils Jansen 001 (CoRR, 2025)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version). - Lina Gerlach; Tobias Winkler 001; Erika Ábrahám; Borzoo Bonakdarpour; Sebastian Junges (CoRR, 2025)

Compositional Verification of Almost-Sure Büchi Objectives in MDPs. - Marck van der Vegt; Kazuki Watanabe 003; Ichiro Hasuo; Sebastian Junges (CoRR, 2025)