Application of the Method for Concurrent Programs Properties Proof to Real-World Industrial Software Systems
Taras Panchenko · 2016
Software correctness is an actual topic in many industries nowadays. Significant system properties should be checked in order to use these software safely. The properties proof task is applicable to pre- viously developed systems also, if the property is new one or when the system is transferring to another runtime environment – for example, to multi-core processor. The method for software properties proof in inter- leaving concurrent environment with communication via shared memory was developed to solve the problem of simultaneous check the required property over the family of programs being run arbitrary times in par- allel – instead of doing separate proofs for every number of program in- stances being run concurrently. Application of this method to real-world industrial tasks is demonstrated in this work.