TCSE logo 
 Sigsoft logo
Sustainability badge
Wed 30 Apr 2025 12:00 - 12:15 at 103 - Formal Methods 1 Chair(s): Cristian Cadar

Behavior Trees (BTs), originated from the control of Non-Player-Characters (NPCs), have been widely embraced in robotics and software engineering communities due to their modularity, reactivity, and other beneficial characteristics. It is highly desirable to synthesize BTs automatically. The consequent challenges are to ensure the generated BTs semantically correct, well-structured, and efficiently executable. To address these challenges, in this paper, we present a novel reactive synthesis method for BTs, namely EffBT, to generate correct and efficient controllers from formal specifications in GR(1) automatically. The idea is to construct BTs soundly from the intermediate strategies derived during the algorithm of GR(1) realizability check. Additionally, we introduce pruning strategies and use of \textit{Parallel} nodes to improve BT execution, while none of the priors explored before. We prove the soundness of the EffBT method, and experimental results across various scenarios and datasets demonstrate its effectiveness.

Wed 30 Apr

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
Formal Methods 1Research Track / New Ideas and Emerging Results (NIER) at 103
Chair(s): Cristian Cadar Imperial College London
11:00
15m
Talk
SpecGen: Automated Generation of Formal Program Specifications via Large Language ModelsFormal Methods
Research Track
Lezhi Ma Nanjing University, Shangqing Liu Nanyang Technological University, Yi Li Nanyang Technological University, Xiaofei Xie Singapore Management University, Lei Bu Nanjing University
11:15
15m
Talk
Gpass: a Goal-adaptive Neural Theorem Prover based on Coq for Automated Formal VerificationFormal Methods
Research Track
Yizhou Chen Peking University, Zeyu Sun Institute of Software, Chinese Academy of Sciences, Guoqing Wang Peking University, Dan Hao Peking University
11:30
15m
Talk
AI-Assisted Autoformalization of Combinatorics Problems in Proof AssistantsFormal Methods
New Ideas and Emerging Results (NIER)
Long Doan George Mason University, ThanhVu Nguyen George Mason University
11:45
15m
Talk
Formally Verified Binary-level Pointer AnalysisFormal MethodsArtifact-Available
Research Track
Freek Verbeek Open Universiteit & Virginia Tech, Ali Shokri Virginia Tech, Daniel Engel Open University Of The Netherlands, Binoy Ravindran Virginia Tech
12:00
15m
Talk
EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution FrameworkFormal MethodsArtifact-FunctionalArtifact-Available
Research Track
ziji wu National University of Defense Technology, yu huang National University of Defense Technology, peishan huang National University of Defense Technology, shanghua wen National University of Defense Technology, minglong li National University of Defense Technology, Ji Wang National University of Defense Technology
12:15
7m
Talk
SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code GenerationFormal Methods
New Ideas and Emerging Results (NIER)
Junjie Sheng East China Normal University, Yanqiu Lin East China Normal University, Jiehao Wu East China Normal University, Yanhong Huang East China Normal University, Jianqi Shi East China Normal University, Min Zhang East China Normal University, Xiangfeng Wang East China Normal University
12:22
7m
Talk
Listening to the Firehose: Sonifying Z3’s BehaviorArtifact-FunctionalArtifact-ReusableArtifact-AvailableFormal Methods
New Ideas and Emerging Results (NIER)
Finn Hackett University of British Columbia, Ivan Beschastnikh University of British Columbia
:
:
:
: