CV

Education

Work experience

Publications

  1. Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.-P., & Becker, B. (2021). Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions. IEEE Trans. Autom. Control.
  2. Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., & Volk, M. (2021). The Probabilistic Model Checker Storm. STTT.
  3. Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J.-P., & Klein, J. (2020). Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf. Comput., 272, 104504.
  4. Hartmanns, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Multi-cost Bounded Tradeoff Analysis in MDP. J. Autom. Reason., 64(7), 1483–1522.
  5. Bork, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Verification of Indefinite-Horizon POMDPs. ATVA, 12302, 288–304.
  6. Jansen, N., Könighofer, B., Junges, S., Serban, A., & Bloem, R. (2020). Safe Reinforcement Learning Using Probabilistic Shields. CONCUR, 171, 3:1–3:16.
  7. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2020). Scenario-Based Verification of Uncertain MDPs. TACAS, 12078, 287–305.
  8. Batz, K., Junges, S., Kaminski, B. L., Katoen, J.-P., Matheja, C., & Schröer, P. (2020). PrIC3: Property Directed Reachability for MDPs. CAV, 12225, 512–538.
  9. Ceska, M., Dehnert, C., Jansen, N., Junges, S., & Katoen, J.-P. (2019). Model Repair Revamped - - On the Automated Synthesis of Markov Chains -. From Reactive Systems to Cyber-Physical Systems, 11500, 107–125.
  10. Spel, J., Junges, S., & Katoen, J.-P. (2019). Are Parametric Markov Chains Monotonic? ATVA, 11781, 479–496.
  11. Winkler, T., Junges, S., Pérez, G. A., & Katoen, J.-P. (2019). On the Complexity of Reachability in Parametric Markov Decision Processes. CONCUR, 140, 14:1–14:17.
  12. Ceska, M., Hensel, C., Junges, S., & Katoen, J.-P. (2019). Counterexample-Driven Synthesis for Probabilistic Program Sketches. FM, 11800, 101–120.
  13. Ceska, M., Jansen, N., Junges, S., & Katoen, J.-P. (2019). Shepherding Hordes of Markov Chains. TACAS, 11428, 172–190.
  14. Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., & Volk, M. (2019). Safety analysis for vehicle guidance systems with dynamic fault trees. Rel. Eng. and Sys. Safety, 186, 37–50.
  15. Volk, M., Junges, S., & Katoen, J.-P. (2018). Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Trans. Industrial Informatics, 14(1), 370–379.
  16. Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.-P., & Becker, B. (2018). Finite-State Controllers of POMDPs using Parameter Synthesis. UAI, 519–529.
  17. Junges, S., Katoen, J.-P., Stoelinga, M., & Volk, M. (2018). One Net Fits All - A Unifying Semantics of Dynamic Fault Trees Using GSPNs. Petri Nets, 10877, 272–293.
  18. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2018). Synthesis in pMDPs: A Tale of 1001 Parameters. ATVA, 11138, 160–176.
  19. Junges, S., Jansen, N., Katoen, J.-P., Topcu, U., Zhang, R., & Hayhoe, M. M. (2018). Model Checking for Safe Navigation Among Humans. QEST, 11024, 207–222.
  20. Hartmanns, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2018). Multi-cost Bounded Reachability in MDP. TACAS, 10806, 320–339.
  21. Junges, S., Guck, D., Katoen, J.-P., Rensink, A., & Stoelinga, M. (2017). Fault trees on a diet: automated reduction by graph rewriting. Formal Asp. Comput., 29(4), 651–703.
  22. Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., & Volk, M. (2017). Model-Based Safety Analysis for Vehicle Guidance Systems. SAFECOMP, 10488, 3–19.
  23. Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.-P., & Becker, B. (2017). Motion planning under partial observability using game-based abstraction. CDC, 2201–2208.
  24. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Papusha, I., Poonawala, H. A., & Topcu, U. (2017). Sequential Convex Programming for the Efficient Verification of Parametric MDPs. TACAS, 10206, 133–150.
  25. Budde, C. E., Dehnert, C., Hahn, E. M., Hartmanns, A., Junges, S., & Turrini, A. (2017). JANI: Quantitative Model and Tool Interaction. TACAS, 10206, 151–168.
  26. Dehnert, C., Junges, S., Katoen, J.-P., & Volk, M. (2017). A storm is Coming: A Modern Probabilistic Model Checker. CAV, 10427.
  27. Quatmann, T., Junges, S., & Katoen, J.-P. (2017). Markov Automata with Multiple Objectives. CAV, 10426.
  28. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., & Katoen, J.-P. (2016). Parameter Synthesis for Markov Models: Faster Than Ever. ATVA, 9938, 50–67.
  29. Junges, S., Guck, D., Katoen, J.-P., & Stoelinga, M. (2016). Uncovering Dynamic Fault Trees. DSN, 299–310.
  30. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Katoen, J.-P., Ábrahám, E., & Bruintjes, H. (2016). Parameter Synthesis for Probabilistic Systems. MBMV, 72–74.
  31. Volk, M., Junges, S., & Katoen, J.-P. (2016). Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates. SAFECOMP, 9922, 253–265.
  32. Dombrowski, C., Junges, S., Katoen, J.-P., & Gross, J. (2016). Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks. SRDS, 307–316.
  33. Junges, S., Jansen, N., Dehnert, C., Topcu, U., & Katoen, J.-P. (2016). Safety-Constrained Reinforcement Learning for MDPs. TACAS, 9636, 130–146.
  34. Junges, S., Jansen, N., Katoen, J.-P., & Topcu, U. (2016). Probabilistic Verification for Cognitive Models. FS-16.
  35. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., & Ábrahám, E. (2015). PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. CAV, 9206, 214–231.
  36. Corzilius, F., Kremer, G., Junges, S., Schupp, S., & Ábrahám, E. (2015). SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. SAT, 9340, 360–368.
  37. Junges, S., Guck, D., Katoen, J.-P., Rensink, A., & Stoelinga, M. (2015). Fault Trees on a Diet - - Automated Reduction by Graph Rewriting -. SETTA, 9409, 3–18.
  38. Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V. Y., & Noll, T. (2014). A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models. ISoLA, 8803, 177–192.
  39. Junges, S., Loup, U., Corzilius, F., & Ábrahám, E. (2013). On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. CAI, 8080, 186–198.
  40. Corzilius, F., Loup, U., Junges, S., & Ábrahám, E. (2012). SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). SAT, 7317, 442–448.

Teaching

Thesis supervision

Lectures (Teaching Assistance)

Guest lectures

Seminar Projects

Academic Service

Organization

PC/AE

2021

AAAI, QAVS, QEST (AE)

2020

FORMATS, SETTA, SYNT, QAVS

2019

ATVA (AE)

Editorial

External Reviewer

Conferences

ATVA, ADHS, CAV, CDC, Concur, FM, FSEN, FORTE, Gandalf, HVC, ICALP, iFM, L4DC, Memocode, MMB, PSI, QEST, SafeComp, TACAS

Journals

FMSD, J. Intelligent Robot Syst, J.Systems and Software, JCST, Machine Learning, STTT