- NL2CTL: Automatic Generation of Formal Requirements Specifications via Large Language Models.- Repairing Event-B Models through Quantifier Elimination.- Tuning Trains Speed in Railway Scheduling.- The Bright Side of Timed Opacity.- Clock-Dependent Probabilistic Timed Automata with One Clock and No Memory.- Efficient State Estimation of Discrete-Timed Automata.- LRNN: A Formal Logic Rules-Based Neural Network for Software Defect Prediction.- Quantitative Symbolic Robustness Verification for Quantized Neural Networks.

- Graph Convolutional Network Robustness Verification Algorithm Based on Dual Approximation.- Formal Kinematic Analysis of Epicyclic Bevel Gear Trains.- Deciding the synthesis problem for hybrid games through bisimulation.- Formal Analysis of FreeRTOS Scheduler on ARM Cortex-M4 Cores.- Differential Property Monitoring for Backdoor Detection.- MemSpate: Memory Usage Protocol Guided Fuzzing.- The Continuum Hypothesis Implies the Existence of Non-Principal Arithmetical Ultrafilters - A Coq Formal Verification.- Observability of Boolean Control Networks: New Definition and Verification Algorithm.

- Formalizing Potential Flows using the HOL Light Theorem Prover.- On-the-Fly Proof-Based Verification of Reachability in Autonomous Vehicle Controllers Relying on Goal-Aware RSS.- Efficient SMT-Based Model Checking for HyperTWTL.- A Tableau-based Approach to Model Checking Linear Temporal Properties.- Simple LTL Model Checking on Finite and Infinite Traces over Concrete Domains.- Model Checking Concurrency in Smart Contracts with a Case Study of Safe Remote Purchase.