We provide two static analysis approaches(using theorem proving) that check if a given (recursive) procedure behaves as if it were stateless, even when it maintains state in global variables. In other words, we check if ...