Abstract: The paper is devoted to the methods of programs proving in the Insertion Modeling System IMS. Architecture and functional possibilities of IMS, the main notions of insertion modeling were presented in this work. Floyd’s insertion machine and the methods of the satisfiability checking, and the usage of those methods for programs proving were described in the paper.

Keywords: multi-agent systems, insertion modeling, program proving.

ACM Classification Keywords: D.2 SOFTWARE ENGINEERING D.2.4 Software/Program Verification.

Link:

SYSTEM OF PROGRAMS PROVING

Alexander Letichevsky, Olexander Letichevskiy, Marina Morokhovets, Vladimir Peschanenko

http://foibg.com/ibs_isc/ibs-28/ibs-28-p15.pdf