Method for checking invariants in a parallel program, - wherein an invariant in the form of a function without parameters (invariant) which returns a Boolean value is declared, - wherein functions ( inv_begin, inv end) for specifying the scope of validity of invariants by a user, and functions ( mem_load, mem_store) for automatic calling with load and store commands are present in a library and are available as binary library code, - wherein the source code of a program is first supplemented by the user by the invariants to be checked, wherein this is done with the aid of the functions ( inv_begin, inv_end) for specifying the scope of validity of invariants in the form of an invariant begin function ( inv _ begin) and of an invariant end function ( inv_end), - wherein the source code, along with the program and the invariants, is translated into a corresponding executable file which is then instrumented with the aid of the binary library code and executed, - wherein an internal data structure is generated in which at least one respective invariant (invariant) is stored, wherein the respective invariant comprises at least one memory location (addresses) on which it depends, and a Boolean value ( record) which indicates whether recording is enabled, - wherein, through the execution of the begin invariant function ( inv_begin), the recording of the invariant concerned is activated and is carried out, along with the corresponding entry in the internal data structure being reset by the end invariant function ( inv _ end), - wherein a corresponding load function ( mem_load) of the functions for automatic calling with load and store commands is called by the instrumentation for each load command and records the addresses of memory locations (addresses) concerned for as long as the recording is enabled, and a corresponding store function ( mem_store) of the functions for automatic calling with load and store commands is called for each store command and checks the invariants (invariant) concerned for their validity, and - in which, with dynamically generated data structures, the addresses relevant for the check are not only determined once at the beginning, but at every change of an affected memory location. - wherein an invariant in the form of a function without parameters (invariant) which returns a Boolean value is declared, - wherein functions ( inv_begin, inv end) for specifying the scope of validity of invariants by a user, and functions ( mem_load, mem_store) for automatic calling with load and store commands are present in a library and are available as binary library code, - wherein the source code of a program is first supplemented by the user by the invariants to be checked, wherein this is done with the aid of the functions ( inv_begin, inv_end) for specifying the scope of validity of invariants in the form of an invariant begin function ( inv _ begin) and of an invariant end function ( inv_end), - wherein the source code, along with the program and the invariants, is translated into a corresponding executable file which is then instrumented with the aid of the binary library code and executed, - wherein an internal data structure is generated in which at least one respective invariant (invariant) is stored, wherein the respective invariant comprises at least one memory location (addresses) on which it depends, and a Boolean value ( record) which indicates whether recording is enabled, - wherein, through the execution of the begin invariant function ( inv_begin), the recording of the invariant concerned is activated and is carried out, along with the corresponding entry in the internal data structure being reset by the end invariant function ( inv _ end), - wherein a corresponding load function ( mem_load) of the functions for automatic calling with load and store commands is called by the instrumentation for each load command and records the addresses of memory locations (addresses) concerned for as long as the recording is enabled, and a corresponding store function ( mem_store) of the functions for automatic calling with load and store commands is called for each store command and checks the invariants (invariant) concerned for their validity, and - in which, with dynamically generated data structures, the addresses relevant for the check are not only determined once at the beginning, but at every change of an affected memory location.