PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

Sadat Shahriyar, Shareef Ahmed, Abdullah Al Arafat

Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, an…