CV

Education

• Ph.D in Computer Science, RWTH Aachen University, 2020
• M.Sc. in Computer Science, RWTH Aachen University, 2015
• B.Sc. in Computer Science, RWTH Aachen University, 2012

Work experience

• Sep 2021 - now: Assistant Professor
  • Radboud University, Nijmegen
  • Software Sciences Group
• Feb 2020 - Aug 2021: Postdoctoral Researcher
  • University of California at Berkeley
  • Learn and Verify Group, headed by Sanjit Seshia
• Jun 2015 - Feb 2020: Research Assistant
  • RWTH Aachen University
  • Chair for Software Modeling and Verification, headed by Joost-Pieter Katoen

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.
   
2. Quatmann, T., Junges, S., & Katoen, J.-P. (2021). Markov Automata with Multiple Objectives. FMSD.
   
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.
   
4. Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., & Volk, M. (2021). The Probabilistic Model Checker Storm. STTT.
   
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.
   
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.
   
9. Junges, S., Jansen, N., & Sanjit A. Seshia. (2021). Enforcing Almost-Sure Reachability in POMDPs. CAV, LNCS 12760, Springer.
   
10. Junges, S., Torfah, H., & Sanjit A. Seshia. (2021). Runtime Monitors for Markov Decision Processes. CAV, LNCS 12760, Springer.
    
11. Vazquez-Chanlatte, M., Junges, S., Fremont, D. J., & Seshia, S. (2021). Entropy-Guided Control Improvisation. RSS.
    
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.
    
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.
    

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.
   
3. Bork, A., Junges, S., Katoen, J.-P., & Quatmann, T. (2020). Verification of Indefinite-Horizon POMDPs. ATVA, LNCS 12302, pp. 288–304, Springer.
   
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.
   
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)

• OWLS 2020
• DESTION 2021
• GI Kolloquium
• FUNCTION 2021

Teaching

Thesis supervision

• Tom Janson, Accelerated Model Repair using Heuristic Analysis of Subsystems (BSc, RWTH)
• Tim Quatmann, Multi-Objective Model Checking for Markov Automata (MSc, RWTH)
• Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees (BSc, RWTH) – together with Matthias Volk
• Michael Deutschen, GSPN Semantics for Dynamic Fault Trees (MSc, RWTH) – together with Matthias Volk
• Dustin Jungen, Repairs in Dynamic Fault Trees (BSc, RWTH) – together with Matthias Volk
• Sebastian Kruse, Model Checking a Wireless Token-Passing Network (MSc, RWTH)
• Sven Deserno, Model Checking Families of Markov Chains (MSc, RWTH) – together with Benjamin Kaminski
• Jip Spel, Monotonicity in Markov Chains (MSc, University of Twente)
• Dustin Jungen, SAT-Based Methods for Solving POMDP problems (MSc, RWTH)
• Kevin Batz, Probabilistic IC3 (MSc, RWTH) – together with Benjamin Kaminski and Christoph Matheja
• Marnix Suilen, Multi-environment MDPs – with Nils Jansen

Lectures (Teaching Assistance)

• Model Checking (RWTH, Winter 2019)
• Datastructures and Algorithms (RWTH, Summer 2018)
• Concurrency Theory (RWTH, Winter 2017)
• Compiler Construction (RWTH, Summer 2017)
• Introduction to Model Checking (RWTH, Summer 2016)
• Modeling and Verification of Probabilistic Systems (RWTH, Winter 2015)

Guest lectures

• Introduction to probabilistic model checking (UC Berkeley, Formal Methods, 2020)
• On parameter synthesis (RWTH, Modeling and Verification of Probabilistic Systems, 2019)

Seminar Projects

• Introduction to Program Analysis (RWTH, Proseminar, Sumer 2019)
• Trends and Pearls of Model Checking (RWTH, Seminar, Winter 2019)
• Formal Verification Meets Machine Learning (RWTH, Seminar, Summer 2018)
• Programming Language Design and Implementation (RWTH, Seminar, Winter 2017)
• Introduction to Program Analysis (RWTH, Proseminar, Winter 2016)
• Probabilistic Programming (RWTH, Seminar, Summer 2016)
• Algorithms and Data Structures (RWTH, Proseminar, Winter 2015)

Academic Service

Organization

• VeriProp 2021 (co-located with CAV)
• I co-organised the 1st and 2nd UnRAVEL Spring Meetings.
• I co-organised the ‘Aachener Informatik Tage’, a STEM-outreach event for highschool pupils, several times.

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