Underspecified behaviour in C with software verification

My research and development project that I worked on during my honours year of 2022 was on the topic of “Explicit sequencing of C programs” whereby I looked at ways to improve the current state of Software Verification in Lazy-CSeq with regards to the underspecified evaluation ordering of function arguments and binary operators in the C programming language. The transformation module was written in Python2 (as is standard with CSeq).