Sebastian Junges

sjp_8106_01

This website is now outdated. Please visit my new website.

In February 2020, I defended my PhD Thesis titled ‘Parameter Synthesis in Markov Models’ with honours.

I was a PhD student at the Software Modeling and Verification Group between June 2015 and February 2020. From October 2017 until February 2020, I was affiliated with the Research Training Group UnRAVeL.

You can also find me on DBLP and Google Scholar.

Research interests

  • Model checking of quantitative (parameterised) systems
  • Policy synthesis for variants of partially observable MDPs
  • Formal aspects of reliability engineering, in particular fault trees
  • SMT-solving for real arithmetic
  • Formal modelling of real-world systems

Tool support

Over the years, I’ve been involved in the development of the following tools to advance the state-of-the-art in computer aided verification:

  • The SMT-solver SMT-RAT (2011 — 2015)
  • The arithmetic library carl (2012 — 2015) and its python bindings pycarl (since 2016)
  • Compass (2014)
  • The Markov Chain Parameter Synthesis Framework PROPhESY (since 2014)
  • The Probabilistic Model Checker Storm (since 2014) and its python bindings stormpy (since 2016)

B.Sc or M.Sc theses

I’m always looking forward to work with students. If you’re looking for a thesis in one of the areas above, do not hesitate to contact me! Some ideas are given in our list of open topics.

Previously, I supervised the following theses (chronological order):

  • Tom Janson, Accelerated Model Repair using Heuristic Analysis of Subsystems (BSc)
  • Tim QuatmannMulti-Objective Model Checking for Markov Automata (MSc)
  • Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees (BSc) [together with Matthias Volk]
  • Michael Deutschen, GSPN Semantics for Dynamic Fault Trees (MSc) [together with Matthias Volk]
  • Dustin Jungen, Repairs in Dynamic Fault Trees (BSc) [together with Matthias Volk]
  • Sebastian Kruse, Model Checking a Wireless Token-Passing Network (MSc)
  • Sven Deserno,  Model Checking Families of Markov Chains (MSc) [together with Benjamin Kaminski]
  • Jip SpelMonotonicity in Markov Chains (MSc)

Teaching

I was involved in teaching assistance for the following lectures:

Furthermore, I supervised students in the scope of the following seminars:

Reviewer

I have been PC Member for the Artefact Evaluation of ATVA. 

I have been an external reviewer for the following venues:
ATVA, ADHS, CAV, CDC, FM, FORTE, Gandalf, ICALP, iFM, MMB, HVC, PSI, QEST, SafeComp,

and for the following journals:
FMSD, J.Systems and Software.

2020
DOI [bibtex]
@conference{P2020,
title = {PrIC3},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {512-538},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_27},
url = { https://publications.rwth-aachen.de/record/816242},
}×
[issue]
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3, 32rd International Conference on Computer-Aided Verification, Volume 12225 of LNCS, 512-538, Springer, 2020.
DOI fulltext PDF [bibtex]
@phdthesis{PM2020,
title = {Parameter synthesis in Markov models},
author = {Sebastian Junges},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (xv, 371 Seiten) : Illustrationen},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-02348},
url = { https://publications.rwth-aachen.de/record/783179},
}×
[issue]
Sebastian Junges. Parameter synthesis in Markov models, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xv, 371 Seiten) : Illustrationen, 2020.
fulltext PDF [bibtex]
@techreport{URTG2020,
title = {UnRAVeL Research Training Group},
author = {Joost-Pieter Katoen and Martin Ritzert and Richard Wilke and Katrin M. Dannert and Peter Lindner and Dennis Fischer and Janosch Fuchs and Björn Frederik Tauer and Vipin Ravindran Vijayalakshmi and Laura Vargas Koch and Nadine Friesen and Andreas Gabriel Klinger and Marcel Tobias Hark and Benjamin Lucien Kaminski and Sebastian Junges and Jip Josephine Spel and Anton Pirogov and Stefan Schupp and Till Hofmann and Daxin Liu and Martin Comis and Tabea Claudia Krabs and Stephan Zieger and Rebecca Haehn and Matthias Volk and Norman Weik and Helene-Maria Bolke-Hermanns},
pages = {85 Seiten},
type = {Tech Report},
year = {2020},
url = { https://publications.rwth-aachen.de/record/807487},
}×
[issue]
Joost-Pieter Katoen, Martin Ritzert, Richard Wilke, Katrin M. Dannert, Peter Lindner, Dennis Fischer, Janosch Fuchs, Björn Frederik Tauer, Vipin Ravindran Vijayalakshmi, Laura Vargas Koch, Nadine Friesen, Andreas Gabriel Klinger, Marcel Tobias Hark, Benjamin Lucien Kaminski, Sebastian Junges, Jip Josephine Spel, Anton Pirogov, Stefan Schupp, Till Hofmann, Daxin Liu, Martin Comis, Tabea Claudia Krabs, Stephan Zieger, Rebecca Haehn, Matthias Volk, Norman Weik, Helene-Maria Bolke-Hermanns. UnRAVeL Research Training Group, 85 Seiten, 2020.
DOI fulltext PDF [bibtex]
@article{MBTAM2020,
title = {Multi-cost Bounded Tradeoff Analysis in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
journal = {Journal of automated reasoning},
volume = {64(7)},
pages = {pages 1483-1522},
type = {Journal Article},
year = {2020},
doi = {10.1007/s10817-020-09574-9},
url = { https://publications.rwth-aachen.de/record/794977},
}×
[issue]
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Tradeoff Analysis in MDP, Journal of automated reasoning 64 (7), pages 1483-1522, Springer, 2020.
DOI [bibtex]
@conference{SBVUM2020,
title = {Scenario-Based Verification of Uncertain MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12078},
pages = {287-305},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_16},
url = { https://publications.rwth-aachen.de/record/794207},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Scenario-Based Verification of Uncertain MDPs, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 12078 of Theoretical Computer Science and General Issues, 287-305, Springer, 2020.
DOI [bibtex]
@article{PM2020,
title = {Parametric Markov chains},
author = {Christel Baier and Christian Hensel and Lisa Hutschenreiter and Sebastian Junges and Joost-Pieter Katoen and Joachim Klein},
publisher = {Elsevier},
journal = {Information and computation},
volume = {272},
pages = {pages 104504},
type = {Journal Article},
year = {2020},
doi = {10.1016/j.ic.2019.104504},
url = { https://publications.rwth-aachen.de/record/793292},
}×
[issue]
Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein. Parametric Markov chains, Information and computation 272, pages 104504, Elsevier, 2020.
arXiv:2004.14835 [bibtex]
@unpublished{P2020,
title = {PrIC3},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2004.14835},
}×
[issue]
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3, 2020. https://arxiv.org/abs/2004.14835
2019
DOI [bibtex]
@article{S2019,
title = {Safety analysis for vehicle guidance systems with dynamic fault trees},
author = {Majdi Ghadhab and Sebastian Junges and Joost-Pieter Katoen and Matthias Kuntz and Matthias Volk},
publisher = {Elsevier Science},
journal = {Reliability engineering & system safety},
volume = {186},
pages = {pages 37-50},
type = {Journal Article},
year = {2019},
doi = {10.1016/j.ress.2019.02.005},
url = { https://publications.rwth-aachen.de/record/755407},
}×
[issue]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees, Reliability engineering & system safety 186, pages 37-50, Elsevier Science, 2019.
DOI [bibtex]
@conference{CP2019,
title = {Correct-by-construction policies for POMDPs},
author = {Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Bernd Becker and Ralf Wimmer and Leonore Winterer},
publisher = {ACM Press},
pages = {6-8},
type = {Conference Paper},
year = {2019},
doi = {10.1145/3313149.3313366},
url = { https://publications.rwth-aachen.de/record/764541},
}×
[issue]
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer. Correct-by-construction policies for POMDPs, 5th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR) held as part of the 12th Cyber-Physical Systems and Internet-of-Things Week (CPS-IoT Week) (SNR '19), 6-8, ACM Press, 2019.
DOI [bibtex]
@inbook{MRR2019,
title = {Model Repair Revamped},
author = {Milan Češka and Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11500},
pages = {107-125},
type = {Book Chapter},
year = {2019},
doi = {10.1007/978-3-030-31514-6_7},
url = { https://publications.rwth-aachen.de/record/768054},
}×
[issue]
Milan Češka, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{OCRPMDP2019,
title = {On the Complexity of Reachability in Parametric Markov Decision Processes},
author = {Tobias Winkler and Sebastian Junges and Guillermo A. Pérez and Joost-Pieter Katoen},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August},
booktitle = {Leibniz international proceedings in informatics : LIPIcs},
volume = {140},
type = {Conference Paper},
year = {2019},
doi = {10.4230/LIPICS.CONCUR.2019.14},
url = { https://publications.rwth-aachen.de/record/780394},
}×
[issue]
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, CONCUR 2019, Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019.
DOI [bibtex]
@conference{APMCM2019,
title = {Are Parametric Markov Chains Monotonic?},
author = {Jip Josephine Spel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11781},
pages = {479-496},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-31784-3_28},
url = { https://publications.rwth-aachen.de/record/786826},
}×
[issue]
Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen. Are Parametric Markov Chains Monotonic?, 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), Volume 11781 of LNCS, 479-496, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{SHMC2019,
title = {Shepherding Hordes of Markov Chains},
author = {Milan Češka and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11428},
pages = {172-190},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17465-1_10},
url = { https://publications.rwth-aachen.de/record/786829},
}×
[issue]
Milan Češka, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 11428 of LNCS, 172-190, Springer, 2019.
DOI [bibtex]
@conference{CDSPPS2019,
title = {Counterexample-Driven Synthesis for Probabilistic Program Sketches},
author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11800},
pages = {101-120},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-30942-8_8},
url = { https://publications.rwth-aachen.de/record/786831},
}×
[issue]
Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches, 3rd World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019.
2018
DOI fulltext PDF [bibtex]
@conference{MBRM2018,
title = {Multi-cost Bounded Reachability in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {10806},
pages = {320-339},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89963-3_19},
url = { https://publications.rwth-aachen.de/record/745801},
}×
[issue]
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Reachability in MDP, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806 of LNCS, 320-339, Springer, 2018.
DOI [bibtex]
@article{FDFTAMCT2018,
title = {Fast Dynamic Fault Tree Analysis by Model Checking Techniques},
author = {Matthias Volk and Sebastian Junges and Joost-Pieter Katoen},
publisher = {IEEE},
journal = {IEEE transactions on industrial informatics},
volume = {14(1)},
pages = {pages 370-379},
type = {Journal Article},
year = {2018},
doi = {10.1109/TII.2017.2710316},
url = { https://publications.rwth-aachen.de/record/713138},
}×
[issue]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques, IEEE transactions on industrial informatics 14 (1), pages 370-379, IEEE, 2018.
[bibtex]
@conference{FSCPPS2018,
title = {Finite-State Controllers of POMDPs using Parameter Synthesis},
author = {Sebastian Junges and Nils Jansen and Ralf Wimmer and Tim Quatmann and Leonore Winterer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Curran Associates, Inc.},
pages = {519-529},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/794908},
}×
[issue]
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34th Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, Curran Associates, Inc., 2018.
fulltext PDF [bibtex]
@conference{FSCPPS2018,
title = {Finite-State Controllers of POMDPs using Parameter Synthesis},
author = {Sebastian Junges and Nils Jansen and Ralf Wimmer and Tim Quatmann and Leonore Winterer and Joost-Pieter Katoen and Bernd Becker},
publisher = {AUAI Press},
pages = {519-529},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/754534},
}×
[issue]
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34th Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, AUAI Press, 2018.
DOI [bibtex]
@conference{MCSNAH2018,
title = {Model Checking for Safe Navigation Among Humans},
author = {Sebastian Junges and Nils Jansen and Joost-Pieter Katoen and Ufuk Topcu and Ruohan Zhang and Mary Hayhoe},
publisher = {Springer},
booktitle = {LNCS},
volume = {11024},
pages = {207-222},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-99154-2_13},
url = { https://publications.rwth-aachen.de/record/754533},
}×
[issue]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking for Safe Navigation Among Humans, 15th International Conference on Quantitative Evaluation of Systems (QEST), Volume 11024 of LNCS, 207-222, Springer, 2018.
DOI [bibtex]
@conference{S2018,
title = {Synthesis in pMDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Springer},
booktitle = {LNCS},
volume = {11138},
pages = {160-176},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-030-01090-4},
url = { https://publications.rwth-aachen.de/record/753087},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs, 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Volume 11138 of LNCS, 160-176, Springer, 2018.
DOI [bibtex]
@conference{ONFA2018,
title = {One Net Fits All},
author = {Sebastian Junges and Joost-Pieter Katoen and Marielle Stoelinga and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10877},
pages = {272-293},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-91268-4_14},
url = { https://publications.rwth-aachen.de/record/753065},
}×
[issue]
Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All, 39th International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS 2018), Volume 10877 of LNCS, 272-293, Springer, 2018.
2017
DOI [bibtex]
@conference{M2017,
title = {Motion planning under partial observability using game-based abstraction},
author = {Leonore Winterer and Sebastian Junges and Ralf Wimmer and Nils Jansen and Ufuk Topcu and Joost-Pieter Katoen and Bernd Becker},
publisher = {IEEE},
pages = {2201-2208},
type = {Conference Paper},
year = {2017},
doi = {10.1109/CDC.2017.8263971},
url = { https://publications.rwth-aachen.de/record/713579},
}×
[issue]
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion planning under partial observability using game-based abstraction, IEEE 56th Annual Conference on Decision and Control (CDC), 2201-2208, IEEE, 2017.
DOI [bibtex]
@conference{MAMO2017,
title = {Markov Automata with Multiple Objectives},
author = {Tim Quatmann and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10426},
pages = {140-159},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63387-9_7},
url = { https://publications.rwth-aachen.de/record/713574},
}×
[issue]
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10426 of LNCS, 140-159, Springer, 2017.
DOI [bibtex]
@conference{J2017,
title = {JANI},
author = {Carlos E. Budde and Hans Christian Dehnert and E. Moritz Hahn and Arnd Hartmanns and Sebastian Junges and Andrea Turrini},
publisher = {Springer},
booktitle = {LNCS},
volume = {10206},
pages = {151-168},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-662-54580-5_9},
url = { https://publications.rwth-aachen.de/record/713573},
}×
[issue]
Carlos E. Budde, Hans Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. JANI, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 151-168, Springer, 2017.
DOI [bibtex]
@conference{SCPEVPM2017,
title = {Sequential Convex Programming for the Efficient Verification of Parametric MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ivan Papusha and Hasan A. Poonawala and Ufuk Topcu},
publisher = {Springer},
booktitle = {LNCS},
volume = {10206},
pages = {133-150},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-662-54580-5_8},
url = { https://publications.rwth-aachen.de/record/713572},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 133-150, Springer, 2017.
DOI [bibtex]
@conference{ASC2017,
title = {A Storm is Coming},
author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10427},
pages = {592-600},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63390-9_31},
url = { https://publications.rwth-aachen.de/record/713569},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017.
arXiv:1702.04311 [bibtex]
@unpublished{AC2017,
title = {A storm is Coming},
author = {Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk},
pages = {14 Seiten : Tabellen, Diagramme},
type = {Preprint},
year = {2017},
url = { https://arxiv.org/abs/1702.04311},
}×
[issue]
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming, 14 Seiten : Tabellen, Diagramme, 2017. https://arxiv.org/abs/1702.04311
DOI [bibtex]
@article{F2017,
title = {Fault trees on a diet},
author = {Sebastian Junges and Dennis Guck and Joost-Pieter Katoen and Arend Rensink and Mariëlle Stoelinga},
publisher = {Springer},
journal = {Formal aspects of computing},
volume = {29(4)},
pages = {pages 651-703},
type = {Journal Article},
year = {2017},
doi = {10.1007/s00165-016-0412-0},
url = { https://publications.rwth-aachen.de/record/696190},
}×
[issue]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga. Fault trees on a diet, Formal aspects of computing 29 (4), pages 651-703, Springer, 2017.
DOI [bibtex]
@conference{MSAVGS2017,
title = {Model-based Safety Analysis for Vehicle Guidance Systems},
author = {Majdi Ghadhab and Sebastian Junges and Joost-Pieter Katoen and Matthias Kuntz and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10488},
pages = {3-19},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-66266-4_1},
url = { https://publications.rwth-aachen.de/record/713577},
}×
[issue]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems, 36th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Volume 10488 of LNCS, 3-19, Springer, 2017.
2016
DOI [bibtex]
@inbook{UDFT2016,
title = {Uncovering Dynamic Fault Trees},
author = {Sebastian Junges and Dennis Guck and Joost-Pieter Katoen and Marielle Stoelinga},
publisher = {IEEE},
pages = {299-310},
type = {Book Chapter},
year = {2016},
doi = {10.1109/DSN.2016.35},
url = { https://publications.rwth-aachen.de/record/684644},
}×
[issue]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga. Uncovering Dynamic Fault Trees, 299-310, IEEE, 2016.
DOI [bibtex]
@conference{MCAPDULLWN2016,
title = {Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks},
author = {Christian Dombrowski and Sebastian Junges and Joost-Pieter Katoen and James Gross},
publisher = {IEEE},
pages = {307-316},
type = {Conference Paper},
year = {2016},
doi = {10.1109/SRDS.2016.048},
url = { https://publications.rwth-aachen.de/record/683784},
}×
[issue]
Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross. Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks, 2016 IEEE 35th Symposium on Reliable Distributed Systems (SRDS) (SRDS 2016), 307-316, IEEE, 2016.
DOI [bibtex]
@conference{PSMM2016,
title = {Parameter Synthesis for Markov Models},
author = {Tim Quatmann and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9938},
pages = {50-67},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-46520-3_4},
url = { https://publications.rwth-aachen.de/record/681503},
}×
[issue]
Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
DOI fulltext PDF [bibtex]
@conference{P2016,
title = {Parameter synthesis for probabilistic systems},
author = {Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Albert-Ludwigs-Universität},
pages = {72-74},
type = {Conference Paper},
year = {2016},
doi = {10.6094/UNIFR/10639},
url = { https://publications.rwth-aachen.de/record/683021},
}×
[issue]
Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
DOI [bibtex]
@inbook{ADFTAGSSSFSFR2016,
title = {Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates},
author = {Matthias Volk and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9922},
pages = {253-265},
type = {Book Chapter},
year = {2016},
doi = {10.1007/978-3-319-45477-1_20},
url = { https://publications.rwth-aachen.de/record/684646},
}×
[issue]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, Volume 9922 of LNCS, 253-265, Springer, 2016.
DOI [bibtex]
@inbook{SRLM2016,
title = {Safety-constrained Reinforcement Learning for MDPs},
author = {Sebastian Junges and Nils Jansen and Hans Christian Dehnert and Ufuk Topcu and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9636},
pages = {130-146},
type = {Book Chapter},
year = {2016},
doi = {10.1007/978-3-662-49674-9_8},
url = { https://publications.rwth-aachen.de/record/684642},
}×
[issue]
Sebastian Junges, Nils Jansen, Hans Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs, Volume 9636 of LNCS, 130-146, Springer, 2016.
fulltext PDF [bibtex]
@inbook{PVCM2016,
title = {Probabilistic Verification for Cognitive Models},
author = {Sebastian Junges and Nils Jansen and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {AAAI Press},
booktitle = {AAAI Technical Reports},
volume = {FS-16-03},
pages = {185-188},
type = {Book Chapter},
year = {2016},
url = { https://publications.rwth-aachen.de/record/684648},
}×
[issue]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models, Volume FS-16-03 of AAAI Technical Reports, 185-188, AAAI Press, 2016.
2015
DOI [bibtex]
@conference{FTD2015,
title = {Fault Trees on a Diet},
author = {Sebastian Junges and Dennis Guck and Joost-Pieter Katoen and Arend Rensink and Mariëlle Stoelinga},
publisher = {Springer},
booktitle = {LNCS},
volume = {9409},
pages = {3-18},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-25942-0_1},
url = { https://publications.rwth-aachen.de/record/571615},
}×
[issue]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga. Fault Trees on a Diet, First International Symposium on Dependable Software Engineering (SETTA 2015), Volume 9409 of LNCS, 3-18, Springer, 2015.
DOI [bibtex]
@conference{P2015,
title = {PROPhESY},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9206},
pages = {214-231},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-21690-4_13},
url = { https://publications.rwth-aachen.de/record/564236},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
DOI [bibtex]
@conference{SR2015,
title = {SMT-RAT},
author = {Florian Corzilius and Gereon Kremer and Sebastian Junges and Stefan Schupp and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9340},
pages = {360-368},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-24318-4_26},
url = { https://publications.rwth-aachen.de/record/561680},
}×
[issue]
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám. SMT-RAT, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, 360-368, Springer, 2015.
2014
DOI [bibtex]
@inbook{ARSMCPRTSM2014,
title = {A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models},
author = {Dimitri Bohlender and Harold Yorick Bruintjes and Sebastian Junges and Jens Katelaan and Viet Yen Nguyen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {8803},
pages = {177-192},
type = {Book Chapter},
year = {2014},
doi = {10.1007/978-3-662-45231-8_13},
url = { https://publications.rwth-aachen.de/record/465766},
}×
[issue]
Dimitri Bohlender, Harold Yorick Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models, Volume 8803 of LNCS, 177-192, Springer, 2014.
2013
fulltext PDF [bibtex]
@techreport{OGBCSMTSRN2013,
title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers},
author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám},
publisher = {Shaker [u.a.]},
booktitle = {Aachener Informatik-Berichte : AIB},
volume = {2013,08},
pages = {3-21},
type = {Tech Report},
year = {2013},
url = { https://publications.rwth-aachen.de/record/228582},
}×
[issue]
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, 3-21, Shaker [u.a.], 2013.
DOI [bibtex]
@inbook{OGBCSMTSRN2013,
title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers},
author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {8080},
pages = {186-198},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-40663-8_18},
url = { https://publications.rwth-aachen.de/record/226897},
}×
[issue]
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 8080 of LNCS, 186-198, Springer, 2013.