This lecture introduces a framework for automatically verifying programming exercises, covering topics such as axiomatic processing, model-based representation of programs, implementation issues, and future works. It discusses the use of counterexamples, Hoare triples, and dealing with specific classes of loop-based programs.