.- Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks.
.- Automata-Based Steering of Large Language Models for Diverse Structured Generation.
.- LLM-SYM: Integrating Symbolic Methods and Large Language Models for Automated Theorem Proving.
.- Modeling and Analysis of Cyber-Physical Systems in the Hybrid pi-Calculus Using Extended Sequence Diagrams.
.- Neural-Symbolic System Control Adjustment Based on Runtime Verification.
.- Formalizing Requirements into Dafny Specifications with LLMs.
.- Detecting Vector Container Errors in C++ Programs via Abstract Interpretation.
.- BCCIC3:Batch Clause Construction Enhanced Generalization in IC3.
.- MetaLogic: Robustness Evaluation of Text-to-Image Models Using Logically Equivalent Prompts.
.- Formal Construction of Threat Detections from Attack Trees.
.- A Test-Driven Approach for Refining Use Case Specifications of Software Requirements with LLMs.
.- ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs.
.- Synthesizing Loops from Linear Ranking Functions.
.- Modeling and Verifying Concurrent Reactive Systems Using Separation Logic.
.- Formal Modeling and Verification of Blockchain Consensus Protocols: A Case Study on ChainMaker.
.- A Unified Method to Efficiently Verify Opacity of Discrete-Timed Automata.
.- Quantitative Verification for Temporal Properties of Massive Linear Systems.
.- Avoiding Larger Conflict Regions in CDCL-Style Methods for Solving SMT-NRA.
.- Formal Modeling of Reinforcement Learning Systems with SMT.
.- Formal modelling of fault tolerant robotic missions.
.- Towards High-Level SMT Program Modeling: Bounded Integers, Simplified Structs, and Metaprogramming.