Формальная семантика и верификация программного обеспечения