Shufang-Zhu.github.io

Dr. Shufang Zhu

I am a Senior Research Associate at the Department of Computer Science, University of Oxford, working with Prof. Giuseppe De Giacomo on his Advanced ERC project WhiteMech.

I received my Ph.D. degree in 2020, at East China Normal University (ECNU), Shanghai, China, under the supervision of Prof. Geguang Pu.

During my Ph.D., I got the scholarship from Chinese Scholarship Council (CSC) and studied as a visiting Ph.D. student (August 2016 to Feb 2018) at Rice University, under the supervision of Prof. Moshe Y. Vardi.

Quick links to find me:

• Github
• Google Scholar
• DBLP

You can find my CV here.

My Erdős number is at most 3 (via Moshe Y. Vardi -> Joel H. Spencer -> Paul Erdős).

Email: shufang.zhu(at)cs.ox.ac.uk

News

Apr 6, 2023
Talk on “On the power of LTLf in Assuerd Autonomy” selected for the Oxbridge Conference 2023!

Mar 15, 2023
Journal paper Finite-trace and generalized-reactivity specifications in temporal synthesis is online!

Mar 2, 2023
Course on Game-Theoretic Approach to Planning and Synthesis accepted at ESSAI’23!

Experience

• Senior Postdoctoral Research Associate, 2023 - Present
  University of Oxford, Oxford, UK

• Postdoctoral Research Associate, 2020 - 2022
  Sapienza Università di Roma, Rome, Italy

• Researcher, 2020.5 - 2020.10
  Shanghai Industrial Control Safety Innovation Technology Co. LTD (TICPSH), Shanghai, China

• Researcher Intern, 2018.6 - 2018.8
  OS Kernel Lab, Huawei, Shanghai, China

• Ph.D. Researcher, 2016.8 - 2018.2
  Rice University, Houston, US

Education

• Ph.D. in School of Software Engineering, 2014 - 2020
  East China Normal University, Shanghai, China (ECNU).

• B.Sc. in School of Software Engineering, 2010 - 2014
  East China Normal University, Shanghai, China (ECNU).

Teaching

• 2023: Game-Theoretic Approach to Planning and Synthesis
  Lecturer, European Summer School on Artificial Intelligence

• 2023: Foundations of Self-Programming Agents
  Teaching Assistant, Hilary Term, University of Oxford

• 2022: Game-Theoretic Approach to Planning and Synthesis
  Lecturer, Italian National PhD Program in Artificial Intelligence

Publications

* indicates author list has been sorted alphabetically by last name.

Conference Articles

• Compositional Safety LTL Synthesis*
  Suguman Bansal, Giuseppe De Giacomo, Antonio Di Stasio, Yong Li, Moshe Y Vardi, Shufang Zhu
  To appear at the 14th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2022
  [paper]

• LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work*
  Giuseppe De Giacomo, Marco Favorito, Jianwen Li, Moshe Y Vardi, Shengping Xiao, Shufang Zhu
  In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 2022
  [paper] [slides]

• Synthesis of Maximally Permissive Strategies for LTLf Specifications
  Shufang Zhu, Giuseppe De Giacomo
  In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 2022
  [paper] [slides]

• Act for Your Duties but Maintain Your Rights
  Shufang Zhu, Giuseppe De Giacomo
  In Proc. of International Conference on Principles of Knowledge Representation and Reasoning (KR), 2022
  [paper] [slides]

• Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis*
  Giuseppe De Giacomo, Antonio Di Stasio, Lucas M Tabajara, Moshe Y. Vardi, Shufang Zhu
  In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 2021
  [paper] [slides]

• On-the-fly Synthesis for LTL over Finite Traces
  Shengping Xiao, Jianwen Li, Shufang Zhu, Yingying Shi, Geguang Pu, Moshe Y. Vardi
  In Proc. of the 35th AAAI Conference on Artificial Intelligence (AAAI), 2021
  [paper]

• Synthesis with Mandatory Stop Actions*
  Giuseppe De Giacomo, Antonio Di Stasio, Giuseppe Perelli, Shufang Zhu
  In Proc. of International Conference on Principles of Knowledge Representation and Reasoning (KR), 2021
  [paper] [slides]

• On the Power of Automata Minimization in Temporal Synthesis
  Shufang Zhu, Lucas M Tabajara, Geguang Pu, Moshe Y Vardi
  In Proc. of International Symposium on Games, Automata, Logics, and Formal Verification (GandALF), 2021
  [paper] [slides]

• Two-stage technique for LTLf synthesis under LTL assumptions*
  Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y. Vardi, Shufang Zhu
  In Proc. of International Conference on Principles of Knowledge Representation and Reasoning (KR), 2020
  [paper]

• LTLf Synthesis with Fairness and Stability Assumptions
  Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y Vardi
  In Proc. of AAAI Conference on Artificial Intelligence (AAAI), 2020
  [paper] [slides]

• First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
  Shufang Zhu, Geguang Pu, Moshe Y. Vardi
  In Proc. of Annual Conference of Theory and Applications of Models of Computation (TAMC), 2019
  [paper] [slides]

• Symbolic LTLf Synthesis
  Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
  In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 2017
  [paper] [slides]

• A Symbolic Approach to Safety LTL Synthesis
  Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
  In Proc. of International Haifa Verification Conference (HVC), 2017
  [paper]

• Safety model checking with complementary approximations
  Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, Moshe Y. Vardi
  In Proc. of IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2017
  [paper]

• SAT-Based Explicit LTL Reasoning
  Jianwen Li, Shufang Zhu, Geguang Pu, Moshe Y. Vardi
  In Proc. of International Haifa Verification Conference (HVC), 2015
  [paper]

Journal Articles

• Finite-trace and generalized-reactivity specifications in temporal synthesis*
  Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu
  Formal Methods Syst. Des. (2023). https://doi.org/10.1007/s10703-023-00413-2
  [paper]

• SAT-based explicit LTL reasoning and its application to satisfiability checking
  Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang, Moshe Y. Vardi
  Formal Methods Syst. Des. 54(2):164-190 (2019)
  [paper]

• An explicit transition system construction approach to LTL satisfiability checking.
  Jianwen Li, Shufang Zhu, Geguang Pu, Moshe Y. Vardi, Jifeng He
  Formal Aspects Comput. 30(2): 193-217 (2018)
  [paper]

Workshop Articles

• Symbolic Approaches to LTLf Best-Effort Synthesis*
  Giuseppe De Giacomo, Gianmarco Parretti, Shufang Zhu
  GenPlan 2022: Sixth Workshop on Generalization in Planning
  [paper] [slides]

• Mimicking Behaviors in Separated Domains*
  Giuseppe De Giacomo, Dror Fried, Fabio Patrizi, Shufang Zhu
  GenPlan 2022: Sixth Workshop on Generalization in Planning
  [paper] [slides]