01Formal reasoning · program synthesis · verificationLogics, 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.
11 papers · 1 open-source tool →02LLM agents · RAG · reliability · securityMaking LLM agents and retrieval pipelines accountable: auditing their traces, defending their memories and retrieval corpora, and deciding which of their outputs have earned the right to be trusted.
14 papers · 2 open-source tools →03RL · robotics · anomaly detection · risk-aware controlAutonomy that respects a specification: reinforcement learning under temporal-logic objectives, and detecting and recovering from anomalies before an autonomous system acts on them.
3 papers →04Quantum programs · quantum logic · post-quantum securityReasoning about quantum software when running it is not enough: separation logic for quantum state, retrieval-grounded repair of quantum programs, and the control-plane decisions that make services quantum-safe.
3 papers · 1 open-source tool →05Data mining · NLP · computer vision · optimizationCollaborative and applied work that carries the lab's methods into data mining, Vietnamese NLP, computer vision, finance, law, and operations research.
14 papers · 3 open-source tools →