Datenstrukturabstraktionen zur Modellprüfung

Details

Veröffentlichungs-Nr.

EP3217284

Aktenzeichen

EP17158901

Anmeldetag

2. März 2017

Veröffentlichung

8. Juni 2022

Erteilung

8. Juni 2022

Rechtsraum

EP

IPC

G06F8/51G06F11/36G06F9/445

Abstract

This disclosure relates generally to data structure abstraction, and more particularly to method and system for data structure abstraction for model checking. In one embodiment, the method includes identifying data structure accesses in the source code. Loops are identified in the data structure accesses, and loop-types are identified in the loops. An abstracted code is generated based on the loop types for abstracting the data structure. Abstracting the data structure includes, for each loop, replacing the data structure accesses by one of a corresponding representative element and a non-deterministic value in the loop body of said loop based on elements accessed, and eliminating loop control statement of said loop operating on elements of data structure based on loop type of said loop, and adding a plurality of non-array assignments at a start and after the loop body of the source code. The abstracted code is provided for the model checking.

Anmelder

Firma

Tata Consultancy Services Limited

Land

🇮🇳 Indien

Fachgebiete