Research area 01
Verified AI
Formal reasoning · program synthesis · verification
Logics, decision procedures and proof techniques that certify what a program — or a model — is claimed to do, from separation logic and fractional permissions to LLM-driven program analysis.
Publications (11)
Filter in publications →Source-Obligation-Guided Validation of LLM-Based Code Translation
CSoNet 2026, Ho Chi Minh City, Vietnam · November 2026
To appearFrom Natural-Language Hypotheses to Verified Data-Mining Discoveries
ICDM 2026 (Research Track, CORE Rank A*, Acceptance Rate: 392/1966, 20%), Shenyang, China · November 2026
CORE A*To appearDistributional Program Analysis: Treating Large Language Models as Program Samplers
ASE 2026 (NIER Track, CORE Rank A*, Acceptance Rate: 23/89, 25%), Munich, Germany · November 2026
CORE A*To appearAutomatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications
ICECCS 2020 (CORE Rank A), Singapore · March 2021
CORE AMonadic Decomposability of Regular Relations
ICALP 2019 (CORE Rank A*), Patras, Greece · July 2019
CORE A*Complexity Analysis of Tree Share Structure
APLAS 2018, Wellington, New Zealand · December 2018
Logical Reasoning for Disjoint Permissions
ESOP 2018 (CORE Rank A), Thessaloniki, Greece · April 2018
CORE AA Certified Decision Procedure for Tree Shares
ICFEM 2017, Xi'an, China · November 2017
Disjoint Fractional Permissions in Verification: Applications, Systems and Theory
PhD Thesis, submitted September 2017
Decidability and Complexity of Tree Share Formulas
FSTTCS 2016, Chennai, India · December 2016
Decision Procedures Over Sophisticated Fractional Permissions
APLAS 2012, Kyoto, Japan · December 2012