Logical and operational methods in the analysis of programs and systems