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

• Feb 2020 - now: 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

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

• 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)

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