Abstract: The correctness proof for programs with parallelism, and interleaving concurrency with shared memory in particular, is complicated problem because the state of separate execution thread can be changed even in ready-to-run (waiting) time due to possible inference of one execution path over the other via shared data or messaging mechanics. Classical methods like Floyd-Hoare? cannot be applied directly to this case and new non-trivial methods are required to cope with such a complexity. The safety property proof of real-world system using method for software correctness proof in Interleaving Parallel Composition Language (for defined custom class of programs – namely server software for Symmetric Multi-Processing? architecture like DB-server or Web-server) is the subject of this article. Operational semantics of the system is defined in terms of state transitions. Program Invariant as well as Pre- and Post- conditions are formulated in accordance with the methodology. Conclusions about adequacy of the Method usage for such a kind of tasks (thanks to flexibility of compositionnominative platform) and its practicality as well as ease of use for real-world systems have been made based on this and other authors’ works.

Keywords: software correctness, safety proof, concurrent program, interleaving, invariant, IPCL, composition approach, composition-nominative languages, formal verification.

ACM Classification Keywords: F.3.1 Theory of Computation - LOGICS AND MEANINGS OF PROGRAMS - Specifying and Verifying and Reasoning about Programs, D.2.4 Software - SOFTWARE ENGINEERING - Software/Program Verification.

Link:

PROPERTIES PROOF METHOD IN IPCL APPLICATION TO REAL-WORLD SYSTEM CORRECTNESS PROOF

Mykyta Kartavov, Taras Panchenko, Nataliya Polishchuk

http://www.foibg.com/ijima/vol04/ijima04-02-p04.pdf