This paper is a very short overview of a few advancements in automated verification of concurrent programs over the years, with a focus on the role of commutativity and symmetry in proofs. The aim of this line of work is to use commutativity and symmetry to lower the burden of logical reasoning for the backend theorem provers used in automated verification. The paper is not written to list formal results but rather to provide a high-level intuition about how certain contributions fit together in unexpected ways to advance program verification techniques. An interested reader is encouraged to dig deeper into the formal results in the cited papers. The presented ideas go beyond concurrent programs, but a little bit of focus is helpful in telling a coherent story. Techniques discussed here in part have been used in many other interesting program verification problems including hypersafety verification [2, 17], verification of probabilistic programs [29], counting proofs for the verification of parameterized programs [10], verification of recursive programs [2, 19], verification of sequential programs [18], termination proofs of sequential [20], concurrent [16], and parameterized programs [20], and general LTL properties [4]. We start with an informal overview of an operational style of reasoning about programs that is uniquely suitable for incorporating and exploiting these ideas. Then, we discuss how symmetry and commutativity reasoning fit within the framework.