Optimale Zeugenkonstruktion für Llm-Erleichterte Formale Verifizierung

Details

Veröffentlichungs-Nr.

EP4760585

Anmeldetag

27. November 2025

Veröffentlichung

17. 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 and a second LLM system 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 first finite state machine (FSM) is configured to generate verification properties for the system design responsive to the first description of the system design in the temporal logic language. A second FSM configured to generate verification drivers for the system design. A formal verification (FV) tool configured to determine whether a model of the system design passes or fails. The FV tool is further configured to generate a property witness template and an optimal witness template.

Anmelder

Firma

RTX Corporation

Land

🇺🇸 USA