Bounding Component Behavior via Protocols. - Frantisek Plásil; Milos Besta; Stanislav Visnovsky (TOOLS (30), 1999)

Mechanization of a Proof of String-Preprocessing in Boyer-Moore's Pattern Matching Algorithm. - Milos Besta; Frank A. Stomp (ICECCS, 2002)

A Complete Mechanization of Correctness of a String-Preprocessing Algorithm. - Milos Besta; Frank A. Stomp (Formal Methods Syst. Des., 2005)

An Assertional Correctness Proof of a Self-Stabilizing - Exclusion Algorithm. - Milos Besta; Frank A. Stomp (ICECCS, 2006)