Talk on Conditioning accepted at POPL PPS workshop
November 8, 2015
The talk on “On the Semantic Intricacies of Conditioning” has been accepted for presentation at the Probabilistic Programming Semantics (PPS) workshop at POPL’16.
News
Friedrich Gretz successfully defended his Ph.D. dissertation
September 26, 2015
Friday September 26, Friedrich Gretz successfully defended his PhD dissertation, entitled “Semantics and Loop Invariant Synthesis for Probabilistic Programs” for a jury consisting of Sriram Sankaranarayanan (Boulder, USA), Stefan Kowalewski, Jürgen Giesl, and Joost-Pieter Katoen (all Aachen). Friedrich’s dissertation studies weakest pre-condition semantics, relates this to operational semantics, and extends this to including observations. In addition, he developed the Prinsys tool for…
Read more about Friedrich Gretz successfully defended his Ph.D. dissertationPhD thesis on probabilistic counterexamples
September 22, 2015
The PhD thesis of Nils Jansen titled “Counterexamples in Probabilistic Verification” has recently been published online at the library webpage and can also be found here. The thesis covers multiple approaches and new concepts to the generation and representation of counterexamples for refuted properties on probabilistic systems. All results have been published at several conference proceedings and journals.
Sebastian Junges awarded with Best Master Thesis Prize in Germany
September 10, 2015
Sebastian Junges will receive the price for the best Master Thesis in Computer Science 2014/15 in Germany. His work, entitled Simplifying Fault Trees by Graph Rewriting, has been selected by the Fakultätentag Informatik. Sebastian will be awarded the price during the 45th Annual Meeting of the German Informatics Society (Gesellschaft für Informatik e.V. – GI).
Paper accepted by Formal Methods in System Design
August 28, 2015
The paper entitled Juggrnaut: Using Graph Grammars for Abstracting Unbounded Heap Structures by Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen and Thomas Noll has been accepted for publication by the Formal Methods in System Design journal. This paper presents a novel abstraction framework for heap data structures that employs graph grammars for modelling dynamic data structures, and for defining abstraction mappings to handle infinite state spaces that can arise during the execution of…
Read more about Paper accepted by Formal Methods in System DesignPaper accepted at SETTA 2015
August 23, 2015
The paper “Fault trees on a Diet” by Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink and Mariëlle Stoelinga has been accepted at SETTA’15. The paper presents a novel, fully automated reduction technique for Dynamic Fault Trees (DFTs). The key idea is to interpret DFTs as directed graphs and exploit graph rewriting to simplify them.
Paper accepted at APLAS 2015
August 18, 2015
The paper entitled Tree-Like Grammars and Separation Logic by Christoph Matheja, Christina Jansen and Thomas Noll has been accepted at the 13th Asian Symposium on Programming Languages and Systems (APLAS 2015). This paper investigates the relationship between certain classes of tree grammars and logical formalisms, especially with regard to the corresponding inclusion and entailment problems.
CAV 2015
July 23, 2015
Our new PROPhESY tool for parameter synthesis of Markov chains has been elected (out of 30 artefacts) as runner-up in the Artifact Evaluation at CAV 2015. In addition, Joost-Pieter Katoen gave a three-hour tutorial on probabilistic verification. The tutorial slides can be found here.
Paper accepted at FMCAD 2015
July 8, 2015
The paper entitled IC3 Software Model Checking on Control Flow Automata by Tim Lange, Martin Neuhäußer (Siemens AG) and Thomas Noll has been accepted at the 15th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2015). This paper presents a method to exploit a program’s control flow for efficiently model checking its correctness properties.
Sebastian Junges receives prize for excellent master studies
June 28, 2015
Sebastian Junges received on last Friday (June 26) a price for his excellent achievements in his master studies Computer Science. Sebastian recently completed his master thesis on “Simplifying Dynamic Fault Trees by Graph Rewriting” and was co-supervised by Marielle Stoelinga (Twente). We congratulate Sebastian with this great result!
Paper accepted at FORMATS 2015
June 19, 2015
The paper entitled “Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems” by Martin Fränzle, Sebastian Gerwinn, Paul Kröger (all Oldenburg), Alessandro Abate (Oxford) and Joost-Pieter Katoen has been accepted at the 13th Int. Conf. on Formal Modeling and Analysis of Timed Systems. This paper presents a method to synthesize parameter instances (if such exist) of probabilistic hybrid automata satisfying a multi-objective bounded horizon specification over expected rewards.
Paper accepted at MFCS 40
June 3, 2015
The paper “On the Hardness of Almost-Sure Termination” by Benjamin Kaminski and Joost-Pieter Katoen has been accepted at the 40th MFCS (Mathematical Foundations in Computer Science) conference in Milano. This paper considers the computational hardness of computing expected outcomes and deciding (universal) (positive) almost-sure termination of probabilistic programs with non-determinism.
PROPhESY has been CAV Artifact Evaluated
May 25, 2015
We are happy to announce that our tool PROPhESY: A PRObabilistic ParamEter SYnthesis has successfully passed the CAV 2015 Artifact Evaluation. The purpose of the evaluation is to provide a service by the community to help authors provide more substantial supplements to their papers so future researchers can more effectively build on and compare with previous work.
Falak Sher successfully defended his PhD dissertation
May 17, 2015
Friday April 24, Falak Sher successfully defended his PhD dissertation, entitled “Abstraction and Refinement of Probabilistic Automata using Modal Stochastic Games” for a jury consisting of Lijun Zhang (ISCAS Beijing, China), Stefan Kowalewski, Erich Grädel, and Joost-Pieter Katoen (all Aachen). Falak’s dissertation is concerned with game-based abstraction-refinement in which (instead of existing works) the underlying correctness notion is based on distribution-based (rather than state-based)…
Read more about Falak Sher successfully defended his PhD dissertationPaper accepted at MFPS XXXI
May 17, 2015
The paper “Conditioning in Probabilistic Programming” by Friedrich Gretz, Nils Jansen, Benjamin Kaminski, Joost-Pieter Katoen, Annabelle McIver, and Federico Olmedo has been accepted at the 31st Mathematical Foundations of Programming Semantics Conference. The paper provides an operational and wp-semantics for an imperative probabilistic programming language with conditioning, studies their relation, and shows its usage for program transformations.