Shelekhov V. Deductive verification and optimization of the predicate program for string concatenation // # 12, 2018
