CV

Education

Work experience

Publications

2022

  1. Spel, J., Heck, L., Junges, S., Katoen, J.-P., & Moerman, J. (2022). Gradient-Descent for Randomized Controllers under Partial Observability. VMCAI. (to appear)

2021

  1. Ceska, M., Hensel, C., Junges, S., & Katoen, J.-P. (2021). Counterexample-guided Inductive Synthesis for Probabilistic Systems. Formal Asp. Comput.
    DOI: 10.1007/s00165-021-00547-2
  2. Quatmann, T., Junges, S., & Katoen, J.-P. (2021). Markov Automata with Multiple Objectives. FMSD.
    DOI: 10.1007/s10703-021-00364-6 supplemental material
  3. Junges, S., Katoen, J.-P., Pérez, G. A., & Winkler, T. (2021). The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci., 119, pp. 183–210.
    DOI: 10.1016/j.jcss.2021.02.006 arXiv: 2009.13128
  4. Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., & Volk, M. (2021). The Probabilistic Model Checker Storm. STTT.
    arXiv: 2002.07080 supplemental material further information
  5. 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., 66(3), pp. 1040–1054.
  6. Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suilen, M., & Topcu, U. (2021). Robust Finite-State Controllers for Uncertain POMDPs. AAAI.
  7. Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.-P., & Stupinsky, S. (2021). PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. CAV, LNCS 12759, pp. 856–869, Springer.
    DOI: 10.1007/978-3-030-81685-8_40 supplemental material
  8. Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Sanjit A. Seshia, & Van den Broeck, G. (2021). Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. CAV, LNCS 12760, pp. 577–601, Springer.
    DOI: 10.1007/978-3-030-81688-9_27 supplemental material
  9. Junges, S., Jansen, N., & Sanjit A. Seshia. (2021). Enforcing Almost-Sure Reachability in POMDPs. CAV, LNCS 12760, Springer.
    DOI: 10.1007/978-3-030-81688-9_28 arXiv: 2007.00085 supplemental material
  10. Junges, S., Torfah, H., & Sanjit A. Seshia. (2021). Runtime Monitors for Markov Decision Processes. CAV, LNCS 12760, Springer.
    DOI: 10.1007/978-3-030-81688-9_26 supplemental material
  11. Vazquez-Chanlatte, M., Junges, S., Fremont, D. J., & Seshia, S. (2021). Entropy-Guided Control Improvisation. RSS.
    DOI: 10.15607/RSS.2021.XVII.051 arXiv: 2103.05672
  12. Torfah, H., Junges, S., Fremont, D., & Sanjit A. Seshia. (2021). Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance. RV, LNCS 12974, Springer. (to appear)
  13. Spel, J., Junges, S., & Katoen, J.-P. (2021). Finding Provably Optimal Markov Chains. TACAS, LNCS 12651, pp. 173–190, Springer.
    DOI: 10.1007/978-3-030-72016-2_10
  14. Andriushchenko, R., Ceska, M., Junges, S., & Katoen, J.-P. (2021). Inductive Synthesis for Probabilistic Programs Reaches New Horizons. TACAS, LNCS 12651, pp. 191–209, Springer.
    DOI: 10.1007/978-3-030-72016-2_11 supplemental material

2020

  1. 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, pp. 104504.
  2. Hartmanns, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Multi-cost Bounded Tradeoff Analysis in MDP. J. Autom. Reason., 64(7), pp. 1483–1522.
    DOI: 10.1007/s10817-020-09574-9 supplemental material
  3. Bork, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Verification of Indefinite-Horizon POMDPs. ATVA, LNCS 12302, pp. 288–304, Springer.
    DOI: 10.1007/978-3-030-59152-6_16 arXiv: 2007.00102 supplemental material
  4. Batz, K., Junges, S., Kaminski, B. L., Katoen, J.-P., Matheja, C., & Schröer, P. (2020). PrIC3: Property Directed Reachability for MDPs. CAV, LNCS 12225, pp. 512–538, Springer.
  5. Jansen, N., Könighofer, B., Junges, S., Serban, A., & Bloem, R. (2020). Safe Reinforcement Learning Using Probabilistic Shields. CONCUR, LIPIcs 171, pp. 3:1–3:16, Schloss Dagstuhl - LZI.
  6. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2020). Scenario-Based Verification of Uncertain MDPs. TACAS, LNCS 12078, pp. 287–305, Springer.

2019

  1. 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, pp. 37–50.
  2. Spel, J., Junges, S., & Katoen, J.-P. (2019). Are Parametric Markov Chains Monotonic? ATVA, LNCS 11781, pp. 479–496, Springer.
    supplemental material
  3. Winkler, T., Junges, S., Pérez, G. A., & Katoen, J.-P. (2019). On the Complexity of Reachability in Parametric Markov Decision Processes. CONCUR, LIPIcs 140, pp. 14:1–14:17, Schloss Dagstuhl - LZI.
  4. Ceska, M., Hensel, C., Junges, S., & Katoen, J.-P. (2019). Counterexample-Driven Synthesis for Probabilistic Program Sketches. FM, LNCS 11800, pp. 101–120, Springer.
  5. Ceska, M., Jansen, N., Junges, S., & Katoen, J.-P. (2019). Shepherding Hordes of Markov Chains. TACAS, LNCS 11428, pp. 172–190, Springer.
  6. 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, LNCS 11500, pp. 107–125, Springer.

2018

  1. Volk, M., Junges, S., & Katoen, J.-P. (2018). Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Trans. Industrial Informatics, 14(1), pp. 370–379.
  2. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., & Topcu, U. (2018). Synthesis in pMDPs: A Tale of 1001 Parameters. ATVA, LNCS 11138, pp. 160–176, Springer.
  3. 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, LNCS 10877, pp. 272–293, Springer.
  4. Junges, S., Jansen, N., Katoen, J.-P., Topcu, U., Zhang, R., & Hayhoe, M. M. (2018). Model Checking for Safe Navigation Among Humans. QEST, LNCS 11024, pp. 207–222, Springer.
  5. Hartmanns, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2018). Multi-cost Bounded Reachability in MDP. TACAS, LNCS 10806, pp. 320–339, Springer.
  6. 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, pp. 519–529, AUAI Press.

2017

  1. 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), pp. 651–703.
  2. Dehnert, C., Junges, S., Katoen, J.-P., & Volk, M. (2017). A storm is Coming: A Modern Probabilistic Model Checker. CAV, LNCS 10427, Springer.
  3. Quatmann, T., Junges, S., & Katoen, J.-P. (2017). Markov Automata with Multiple Objectives. CAV, LNCS 10426, Springer.
  4. 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, pp. 2201–2208, IEEE.
  5. Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., & Volk, M. (2017). Model-Based Safety Analysis for Vehicle Guidance Systems. SAFECOMP, LNCS 10488, pp. 3–19, Springer.
  6. Budde, C. E., Dehnert, C., Hahn, E. M., Hartmanns, A., Junges, S., & Turrini, A. (2017). JANI: Quantitative Model and Tool Interaction. TACAS, LNCS 10206, pp. 151–168.
  7. 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, LNCS 10206, pp. 133–150, Springer.

2016

  1. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., & Katoen, J.-P. (2016). Parameter Synthesis for Markov Models: Faster Than Ever. ATVA, LNCS 9938, pp. 50–67, Springer.
  2. Junges, S., Guck, D., Katoen, J.-P., & Stoelinga, M. (2016). Uncovering Dynamic Fault Trees. DSN, pp. 299–310, IEEE CS.
  3. 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, pp. 72–74, Albert-Ludwigs-Universität Freiburg.
  4. Volk, M., Junges, S., & Katoen, J.-P. (2016). Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates. SAFECOMP, LNCS 9922, pp. 253–265, Springer.
  5. Dombrowski, C., Junges, S., Katoen, J.-P., & Gross, J. (2016). Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks. SRDS, pp. 307–316, IEEE CS.
  6. Junges, S., Jansen, N., Dehnert, C., Topcu, U., & Katoen, J.-P. (2016). Safety-Constrained Reinforcement Learning for MDPs. TACAS, LNCS 9636, pp. 130–146, Springer.
  7. Junges, S., Jansen, N., Katoen, J.-P., & Topcu, U. (2016). Probabilistic Verification for Cognitive Models. FS-16, AAAI Press.

2015

  1. 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, LNCS 9206, pp. 214–231, Springer.
  2. 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, LNCS 9340, pp. 360–368, Springer.
  3. Junges, S., Guck, D., Katoen, J.-P., Rensink, A., & Stoelinga, M. (2015). Fault Trees on a Diet - - Automated Reduction by Graph Rewriting -. SETTA, LNCS 9409, pp. 3–18, Springer.

2014

  1. 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, LNCS 8803, pp. 177–192, Springer.

2013

  1. 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, LNCS 8080, pp. 186–198, Springer.

2012

  1. Corzilius, F., Loup, U., Junges, S., & Ábrahám, E. (2012). SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). SAT, LNCS 7317, pp. 442–448, Springer.

Talks (Since 2020)

(Conference presentations associated with a paper are not listed)

Teaching

Thesis supervision

Lectures (Teaching Assistance)

Guest lectures

Seminar Projects

Academic Service

Organization

PC/AE

2021

AAAI, QAVS, QEST (AE), SYNT, SETTA

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, SPIN, QEST, SafeComp, TACAS

Journals

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