Abstract:
Systematic construction and verification of specifications is still one of the most important challenges in system development aka engineering. We present our approach to this problem, an executable algebraic specification language, CafeOBJ. Based on rigorous logical semantics (institutions) and equipped with high level programming concepts (e.g., abstraction, inheritance, parametrization), the language implements equational logic by rewriting. Being executable by rewriting allows to write both specification and verification within the same language.
After a hands-on introduction to CafeOBJ with some programming challenges, we will present some recent work concerning representation of infinite streams and verification of safety and liveness properties.
744 Motooka, Nishi-ku
Fukuoka 819-0395, Japan
TEL (Office): +81-92-802-4402
FAX (Office): +81-92-802-4405
IMI(Institute of Mathematics for Industry)
Seminar
 |
List | |
All(1084) | |
Today and tomorrow's seminars(0) |
Introduction to CafeOBJ with case study
 |
Hold Date | 2015-03-13 16:00～2015-03-13 17:00 |
|
Place | Seminar Room 6, Faculty of Mathematics building, Ito Campus |
|
Object person | |
|
Speaker | Norbert Preining (JAIST) |
－