Abstract Procedure contracts are a well-known approach for specifying programs in a modular way. We investigate a new contract theory for collective procedures in parallel message-passing programs. As in the sequential setting, one can verify that a procedure f conforms to its contract using only the contracts, and not the implementations, of the collective procedures called by f. We apply this approach to C programs that use the Message Passing Interface (MPI), introducing a new contract language that extends the ANSI/ISO C Specification Language. We present contracts for the standard MPI collective functions, as well as many user-defined collective functions. A prototype verification system has been implemented using the CIVL model checker for checking contract satisfaction within small bounds on the number of processes.

The disclosure of critical audit matters (CAMs) plays an important part in audit report reform and financial risk warnings. Current CAMs include matters that need to be focused on from the audit after a comprehensive evaluation of the internal control and other enterprise information, combined with the experience of the project manager, which is closely related to subjective factors, such as auditor professionalism and independence. An increase in subjective judgment becomes a breeding ground for audit failure. First, since long short-term memory (LSTM) is often used to process temporal data, MacBERT is often used as a text encoding, so LSTM is used to encode financial information to overcome the influence of subjective factors, and MacBert is used to encode nonfinancial information. The two modes are then separately encoded to form a dual-stream structure that simulates the process of auditors reviewing documents. Second, a transformer is used to perform multimodal interactions on the dual-stream encoding results to simulate the process of auditors integrating important information. Finally, the multimodal interaction results are fed into the fully connected layers and the SoftMax function to achieve cross-modal fusion, which simulates the process of auditors obtaining CAMs. Simulating single-modal coding, multimodal interaction, and cross-modal fusion helps to realize the automatic generation of CAMs. This ensemble model is called the CAMs automatic generation model and is based on LSTM–MacBert dual-stream transfer learning. The experimental results show that the features of financial statements and public disclosure text extracted by the model can effectively screen CAMs and realize the automatic generation of high-level CAMs.

Abstract Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP.

CIVL is a framework for static analysis and verification of concurrent programs. One of the main challenges to practical application of these techniques is the large number of ways to express concurrency: MPI, OpenMP, CUDA, and Pthreads, for example, are just a few of many "concurrency dialects" in wide use today. These dialects are constantly evolving and it is increasingly common to use several of them in a single "hybrid" program. CIVL addresses these problems by providing a concurrency intermediate verification language, CIVL-C, as well as translators that consume C programs using these dialects and produce CIVL-C. Analysis and verification tools which operate on CIVL-C can then be applied easily to a wide variety of concurrent C programs. We demonstrate CIVL's error detection and verification capabilities on (1) an MPI+OpenMP program that estimates π and contains a subtle race condition, and (2) an MPI-based 1d-wave simulator that fails to conform to a simple sequential implementation.

There are many ways to express parallel programs: message-passing libraries (MPI) and multithreading/GPU language extensions such as OpenMP, Pthreads, and CUDA, are but a few. This multitude creates a serious challenge for developers of software verification tools: it takes enormous effort to develop such tools, but each development effort typically targets one small part of the concurrency landscape, with little sharing of techniques and code among efforts.