CAP Workshop in Beijing

The CAP Project Workshop


The CAP project is reaching its conclusion; participants from the different partners are going to meet together in Beijing to discuss the outcomes of the project as well as future collaborations.

The CAP Workshop will be held in Beijing at Peking University ISCAS on September 2, 2018, just before CONFESTA, the joint event hosting CONCUR, FORMATS, QEST, and SETTA, as well as several workshop and tutorials and the Summer School on Formal Methods.

Yu-Fang Chen, from Academia Sinica, will give an invited talk on advanced automata-based algorithms for program termination checking while Luca Bortolussi, from University of Trieste, will give an invited talk on parametric verification and synthesis by means of the Bayesian machine learning.


Currently expected participants are:

  • for Saarland University:
  • for RWTH-Aachen:
  • for ISCAS:
  • for Peking University:
    • Meng Sun
    • Bican Xia, giving the talk: Nonlinear Craig Interpolant Generation
    • Yi Li, giving the talk: Generating Arduino C Codes from Mediator
    • Xiyue Zhang, giving the talk: Modeling and Verification of Probabilistic Connectors



  • 08:40-08:45: Opening
  • 08:45-09:45: Invited talk by Luca Bortolussi: Parametric Verification and Synthesis: the Bayesian Machine Learning Way
  • 09:45-10:15: Coffee break
  • 10:15-12:15: Verification
    • Michaela Klauck: Compiling Probabilistic Model Checking into Probabilistic Planning
    • Depeng Liu: Model Checking Differentially Private Properties
    • Xiyue Zhang: Modeling and Verification of Probabilistic Connectors
    • Sebastian Junges: Multi-cost Bounded Reachability in MDP
  • 12:15-13:45: Lunch break
  • 13:45-14:45: Invited talk by Yu-Fang Chen: Advanced Automata-Based Algorithms for Program Termination Checking
  • 14:45-15:45: Embedded software
    • Sebastian Biewer: Doping Tests for Embedded Software
    • Yi Li: Generating Arduino C Codes from Mediator
  • 15:45-16:15: Coffee break
  • 16:15-18:15: Synthesis
    • Naijun Zhan: The opacity of Real-time Automata
    • Mingshuai Chen: What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction
    • Bican Xia: Nonlinear Craig Interpolant Generation
    • Joost-Pieter Katoen: Tweaking the Odds: Advancing Parameter Synthesis
  • 18:15-18:20: Closing



Local organizers: