Prophecy-Based Automated Verification of Message-Passing Programs

Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi +2

We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) s…