The European Summer School in Logic, Language and Information ESSLLI is a yearly event that normally brings together several hundred students and teachers for two weeks of courses. Next year’s ESSLLI 2016 will be held in Bozen, Italy. One of the courses will be Algebraic Specification and Verification – an Introduction to CafeOBJ by Kokichi Futatsugi and Norbert Preining. We will update the lecture page in the first half of 2016 with details on each lecture as well a slides.
Students and researchers are welcome to participate in this course.
Ensuring correctness of complex systems like computer programs or communication protocols is gaining ever increasing importance. For correctness it does not suffice to consider the finished system, but correctness already on the level of specification is necessary, that is, before the actual implementation starts. To this aim, algebraic specification and verification languages have been conceived. They are aiming at a mathematically correct description of the properties and behavior of the systems under discussion, and in addition often allow to prove (verify) correctness within the same system.
This course will give an introduction to algebraic specification, its history, logic roots, and actuality with respect to current developments. Paired with the theoretical background we give an introduction to CafeOBJ, a programming language that allows both specification and verification to be carried out together. The course should enable students to understand the theoretical background of algebraic specification, as well as enable them to read and write basic specifications in CafeOBJ.