AI 中文总结
研究确定性MPI程序验证问题，通过用户提供特定函数将程序转换为参数化顺序程序，利用Frama-C/Wp扩展实现该验证方法。
AI 中文摘要
我们考虑验证一个消息传递程序的问题，其中进程数是参数NP，每个进程知道其唯一ID。进程使用指定单个目的地或源的发送和接收命令进行通信。为了验证程序，用户提供函数来指定从进程i发送到进程j的消息数量、在发生前层次结构中每个通信事件的级别，以及从i发送到j的第k条消息所成立的事实。这些用于将程序转换为可使用适用于此类程序的任何技术进行验证的参数化顺序程序。我们在Frama-C/Wp的扩展中实现此方法以验证C/MPI程序。
英文摘要
We consider the problem of verifying a message passing program in which the number of processes is a parameter NP and each process knows its unique ID. Processes communicate using send and receive commands which specify a single destination or source. To verify the program, the user provides functions specifying the number of messages sent from process i to process j, the level of each communication event in the happens-before hierarchy, and a fact that holds for the k-th message sent from i to j. These are used to transform the program to a parameterized sequential program which can be verified using any techniques appropriate for such programs. We realize this approach in an extension to Frama-C/Wp to verify C/MPI programs.
