Computation and Reasoning with Constraints

CDZ Workshop GZ1115, Beijing, China, November 23–29, 2014

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:30Workshop 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