- 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.