Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, which occur in particular interleavings of process actions and are therefore hard to reproduce. It is often nontrivial to precisely state the properties that are expected of an algorithm and the assumptions on the environment under which these properties should hold. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at be- ing similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport's PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. It resembles familiar pseudo-code but is quite expressive and has a formal semantics. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the TLC model checker. As an alternative to partial-order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the TLC model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness.
