Sunday, November 23 — Arrival | |||
18:00 | Dinner | We meet in the lobby for dinner at the hotel. | |
Monday, November 24 | |||
09:00–09:30 | Z. She, T. Sturm | Opening | |
Session 1: Symbolic Methods I — Chair: Maximilian Jaroschek | |||
09:30–10:10 | Wang / Dongming | Triangular Decomposition for Constraint Solving | |
10:10–10:40 | Coffee break | ||
10:40–11:20 | Luo / Yong | A Characteristic Set Method for Ordinary Difference Polynomial Systems | |
11:20–12:00 | Mou / Chenqi | Sparse FGLM Algorithms for Solving Polynomial Systems | |
Lunch | |||
Session 2: Real Solving and Application I — Chair: Hassan Errami | |||
14:00–14:40 | Sturm / Thomas | From Classical Quantifier Elimination to Tropical Decisions for the Reals | |
14:40–15:20 | Xia / Bican | Proving Inequalities and Solving Global Optimization Problems via Simplified CAD Projection | |
15:20–15:50 | Coffee break | ||
Session 3: Algorithms and Tools — Chair: Martin Fränzle | |||
15:50–16:30 | Becker / Bernd | Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving | |
16:30–17:10 | Hermanns / Holger | Concurrent Programming in the Post-Java Era | |
17:10–17:50 | Wimmer / Ralf | Solving Dependency-Quantified Boolean Formulas | |
18:00 | Dinner | ||
Tuesday, November 25 — Excursion | |||
08:00–09:00 | Bus Transfer from the hotel | ||
09:00–11:00 | Visiting the Forbidden City | ||
11:30–12:30 | Lunch | ||
12:30–14:00 | Bus transfer | ||
14:00–16:30 | Visiting the Great Wall at Mutianyu | ||
16:30–18:00 | Bus transfer back to the hotel | ||
18:30 | Dinner | ||
Wednesday, November 26 | |||
Session 1: Symbolic Methods II — Chair: Wei Niu | |||
09:00–09:40 | Gao / Xiao-shan | Differential Elimination by Sparse Differential Resultants | |
09:40–10:20 | Wang / Dingkang | Automatic Proving and Discovering of Geometric Theorems | |
10:20–11:00 | Li / Yongbin | Computing the Bell Number by Using Groebner Bases | |
11:00–11:20 | Coffee break | ||
Session 2: Probabilistic and Hybrid Verification I — Chair: Zhengfeng Yang | |||
11:20–12:00 | She / Zhikun | Under-Approximating Backward Reachable Sets by Convex Polytopes | |
12:00–12:40 | He / Anping | Hybrid Systems and Symbolic Computation | |
Lunch | |||
Session 3: First-order Theorem Proving — Chair: Bernd Becker | |||
14:00–14:40 | Schulz / Stephan | The Present and Future of E | |
14:40–15:20 | Waldmann / Uwe | Hierarchic Superposition Revisited | |
15:20–15:50 | Coffee break | ||
Session 4: Safety and Abstration I — Chair: Stephan Merz | |||
15:50–16:30 | Yang / Zhengfeng | Safety Verification of Interval Hybrid Systems Based on Reliable SOS Programming | |
16:30–17:10 | Bu / Lei | Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification | |
17:10–17:50 | Lin / Wang | Safety Verification of Nonlinear Systems Based on Rational Invariants | |
18:00 | Dinner | ||
Thursday, November 27 | |||
Session 1: Symbolic Methods III — Chair: Yongbin Li | |||
09:00–09:40 | Zeng / Zhenbing | A New Method for Machine Proofs for Inequalities | |
09:40–10:20 | Huang / Yanli | Rational General Solutions of Higher Order Algebraic ODEs | |
10:20–10:40 | Coffee break | ||
Session 2: Safety and Abstration II — Chair: Pascal Fontaine | |||
10:40–11:20 | Zhan / Naijun | Abstraction of Elementary Hybrid Systems | |
11:20–12:00 | Chen / Liqian | Static Analysis Using Numerical Abstract Domains with Absolute Values | |
12:00–12:40 | Xu / Ming | Some Algebraic Methods for Validation and Verification | |
Lunch | |||
Joint Session CDZ/NoDI Seminar: Probabilistic and Hybrid Verification I — Chair: Dongming Wang | |||
14:00–14:20 | Bus transfer to Beihang University | ||
14:20–15:00 | Tour on Beihang campus | ||
15:00–15:20 | Presentation of the State Key Laboratory of Software Development Environment | ||
15:20–15:40 | Presentation of the Key Laboratory of Mathematics, Informatics and Behavioral Semantics of the Chinese Ministry of Education | ||
15:40–16:00 | Coffee break | ||
16:00–16:40 | Fränzle / Martin | From Reasoning with Constraints to Mining Constraints: Multi-Objective Parameter Fitting in Parametric Probabilistic Hybrid Automata |
|
16:40–17:20 | Merz / Stephan | Formal Verification of Fault-Tolerant Distributed Algorithms | |
18:30 | Workshop Dinner | ||
Friday, November 28 | |||
Session 1: Real Solving and Applications II — Chair: Yong Luo | |||
09:40–10:20 | Errami / Hassan | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks | |
10:20–10:50 | Coffee break | ||
10:50–11:30 | Chen / Changbo | Cylindrical Algebraic Decomposition and Quantifier Elimination Based on Regular Chains | |
11:30–12:10 | Niu / Wei | Qualitative Analysis of Biological Systems Using Algebraic Methods | |
Lunch | |||
Session 2: Probabilistic and Hybrid Verification II — Chair: Zhikun She | |||
14:00–14:40 | Zhang / Lijun | Probabilistic Model Checking for Linear Temporal Logics | |
14:40–15:20 | Song / Lei | Probably Safe or Live | |
15:20–15:50 | Coffee break | ||
Session 3: Satisfiability Modulo Theory Solving — Chair: Uwe Waldmann | |||
15:50–16:30 | Fontaine / Pascal | SMT Solving and Combination of Theories | |
16:30–17:10 | Abraham / Erika | Real and Integer Arithmetic as Theories in SMT-Solving | |
17:10–17:50 | Jaroschek / Maximilian | Adapting Quantifier Elimination Methods for SMT-Solving | |
18:00 | Dinner | ||
Saturday, November 29 — Departure |