Much software is written in industry standard programming languages, but these languages often have complex semantics making them hard to formalize. For example, the use of expressions with side effects is common in C programs. We present new inference rules for conditional (if) statements and looping con structs (while) with pre- and postevaluation side effects in their test expressions. These inference rules allow us to formally reason about the security properties of programs.
展开▼
