Formal Methods and Software Engineering

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