May 12, 2015
The website for this year’s Sommerfest is now live! You can find it at http://sommerfest-informatik.de. This year it is organized by our group, and will take place June 26th. The three main events, Karriere, Kluge Kopfe and Coole Party, promise to make it a great day. Visit the link if you want to know more.
April 18, 2015
Our paper “PROPhESY: A PRObabilistic ParamEter SYnthesis Tool” by Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, and Erika Ábrahám was accepted for publication at the 27th International Conference on Computer Aided Verification (CAV) 2015. The paper presents the tool PROPhESY, which is dedicated to model checking and parameter synthesis for parametric discrete-time Markov chains. It features novel and efficient model…
Read more about Paper accepted at CAV 2015April 3, 2015
The paper “Model Checking of Open Interval Markov Chains” by Souymodip Chakraborty and Joost-Pieter Katoen has been accepted at the 22nd International Conference on Analytical & Stochastic Modelling Techniques & Applications (ASMTA 2015). The paper shows that interval MCs with open intervals can be verified by re-using techniques for closed interval MCs.
April 3, 2015
The paper “A statistical approach for timed reachability in AADL models” by Harold Bruintjes, Joost-Pieter Katoen, and David Lesens (Airbus Defense & Space) has been accepted at the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2015, acceptance rate 21,8%). The paper presents a statistical model checker for checking timed and stochastic AADL models against timed reachability properties.
March 24, 2015
The paper “Counterexamples for Expected Rewards” by Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker was accepted for publication at the 20th International Symposium on Formal Methods (FM) 2015. The paper presents the first approaches on counterexamples for discrete-time Markov chains and expected reward properties. Methods are proposed to extract a minimal subsystem which already leads to costs beyond the allowed bound. Besides…
Read more about Paper accepted at FM 2015March 20, 2015
Monday March 9, Jonathan Heinen successfully defended his PhD dissertation, entitled “Verification of Java Programs: A Graph Grammar Approach” for a jury consisting of Arend Rensink (Twente, NL), Thomas Seidl, Martin Grohe, and Joost-Pieter Katoen (all Aachen). Jonathan’s dissertation deals with the automated verification of pointer operations in Java Bytecode programs using quantified LTL where graph properties are expressed as MSP formulas.
March 3, 2015
Carsten Kern, formerly a PhD student at Chair i2, recently obtained a Professorship at the Ostbayerische Technische Hochschule in Regensburg (Bavaria). We congratulate him with this success and wish him a lot of success in Regensburg!
January 22, 2015
On January 15, 2015, Arpit Sharma has successfully defended his dissertation on “Reduction Techniques for Nondeterministic and Probabilistic Systems”. His defense committee consisted of Christof Löding, Holger Hermanns (Saarland University), Joost-Pieter Katoen and Bernhard Rumpe (see picture). Arpit’s dissertation treats weighted lumpability as well as layering techniques for various models.
January 21, 2015
Our paper “A Greedy Approach for the Efficient Repair of Stochastic Models” by Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, and Joost-Pieter Katoen was accepted at NFM 2015. The paper addresses the problem of model repair for parametric discrete-time Markov chains which consists of changing a model with minimal costs such that a desired property is satisfied. We present a greedy algorithm iteratively changing probability distributions. We show the correctness in the sense…
Read more about Paper accepted at NFM 2015December 31, 2014
RWTH Aachen hosts the Young Researchers’ Conference “Frontiers in Formal Methods”, February 25-27 2015. Young researchers (up to two years after completing their PhD thesis) are encouraged to submit a 2-5 page abstract by January 12, 2015 (extended firm deadline). More information can be found here.
December 14, 2014
Hongfei Fu has successfully defended his PhD dissertation entitled “Verifying Probabilistic Systems: New Algorithms and Complexity Results”. Hongfei started his PhD research in autumn 2010. His examiners were Antonin Kucera (Masaryk University, Brno), Wolfgang Thomas and Stefan Kowalewski (see picture).
December 4, 2014
Mark Timmer received the award for the best PhD dissertation in 2013 in the region Overijssel, the Netherlands for his thesis Efficient Modelling, Generation and Analysis of Markov Automata. Mark obtained his PhD degree from the University of Twente, and was supervised by Joost-Pieter Katoen, Jaco van de Pol and Marielle Stoelinga. See also http://www.utwente.nl/nieuwsevents/!/2014/11/350971/overijssel-phd-award-voor-mark-timmer.
October 7, 2014
Our paper “High-level Counterexamples for Probabilistic Automata” by Ralf Wimmer, Nils Jansen, Erika Ábrahám and Joost-Pieter Katoen was accepted for publication in the journal Logical Methods in Computer Science (LMCS). In this paper we investigate the computation of several variations of (minimal) counterexamples that are represented in PRISM’s high-level language which defines a subclass of probabilistic programs. These NP-hard problems are solved via mixed-integer linear programming (MILP).…
Read more about Paper accepted for LMCSSeptember 12, 2014
The paper “Compositional Analysis Using Component-Oriented Interpolation” by Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, and Thomas Noll has received the Best Paper Award at the 11th International Symposium on Formal Aspects of Component Software (FACS 2014). It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.
July 4, 2014
The paper “Exponentially timed SADF: Compositional semantics, reduction, and analysis” by Joost-Pieter Katoen and Hao (Stephen) Wu has been accepted for EMSOFT’14 in New Delhi. The paper presents a compositional semantics of SADF using Markov automata, shows that non-determinism cannot occur, and exploits confluence reduction for scaling quantitative evaluation.