Verfahren zur Automatischen Überprüfung der Richtigkeit eines Zielcomputerprogrammes

Details

Veröffentlichungs-Nr.

EP4797102

Anmeldetag

20. Februar 2025

Veröffentlichung

26. August 2026

Rechtsraum

EP

IPC

G06F11/3604

Abstract

The present invention relates to a method for automatically verifying the correctness of a target computer program, said target computer program being defined by first code instructions in a given programming language, characterized in that it comprises performing, by a data processing unit (21) of a server (2), steps of: (a) Obtaining a collection of mathematical proof obligations, the truth of which implies correctness of the target computer program; (b) Constructing a set of proof strategies, each strategy being defined as a sequence of at least one elementary strategy based on a proof tactic and/or at least one automated prover run, for attempting to discharge at least one of said proof obligations; (c) Selecting a priority proof strategy among said set of proof strategies according to a given criterion; (d) Applying the selected priority proof strategy so as to attempt to discharge at least one of said proof obligations; (e) Determining whether the correctness of said target computer program is verified as a function of the proof obligations that have been successfully discharged.

Anmelder

Firmen

Commissariat à l'Energie Atomique et aux Energies Alternatives
THALES

Land

🇫🇷 Frankreich

Fachgebiete