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