Zeitliche Logische Automaten für die durch Llm Erleichterte Formale Verifikations- und Skalierbarkeitssicherung

Details

Veröffentlichungs-Nr.

EP4756665

Anmeldetag

27. November 2025

Veröffentlichung

10. Juni 2026

Rechtsraum

EP

IPC

G06F30/27, G06F30/3323

Abstract

An apparatus for performing formal verification of a system design comprises a first large language model (LLM) system configured to receive a natural language specification of the system design and generate a first description of the system design in a temporal logic language. A second LLM system is configured to receive the natural language specification of the system design and generate a second description of the system design in the temporal logic language. A generator and compiler is configured to generate finite state machines. At least one finite state machine (FSM) generated by the generator and compiler is configured to analyze operation of the system design using each of the at least one FSM including optimization properties. A formal verification (FV) tool is configured to determine whether the system design passes or fails responsive to the first description of the system design in the temporal logic language.

Anmelder

Firma

RTX Corporation

Land

🇺🇸 USA