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.

Participants

Currently expected participants are:

• for Saarland University:
  • Gereon Fox
  • Michaela Klauck, giving the talk: Compiling Probabilistic Model Checking into Probabilistic Planning
  • Daniel Stan
  • Holger Hermanns
  • Sebastian Biewer, giving the talk: Doping Tests for Embedded Software
• for RWTH-Aachen:
  • Sebastian Junges, giving the talk: Multi-cost Bounded Reachability in MDP
  • Joost-Pieter Katoen, giving the talk: Tweaking the Odds: Advancing Parameter Synthesis
• for ISCAS:
  • Lijun Zhang
  • Naijun Zhan, giving the talk: The opacity of Real-time Automata
  • Yong Li
  • Chen Fu
  • Pengfei Yang
  • Depeng Liu, giving the talk: Model Checking Differentially Private Properties
  • Jianlin Li
  • Mingshuai Chen, giving the talk: What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction
• 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

 

Program

• 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

 

Organization

Local organizers:

• Meng Sun (Peking University)
• Andrea Turrini (ISCAS)