CAESAR

caesar - compilation & verification of LOTOS specifications. caesar [Gar89b,GS90] is a compiler that translates a LOTOS specification into executable code that can be used to explore, on-the-fly or exhaustively, the graph (also called labelled transition system, reachability graph, state space, etc.) corresponding to the behaviour of this specification. caesar itself does not embody verification capabilities, but it smootly interfaces with many tools that can perform explicit-state and on-the-fly verification on the generated graph, including model checking, equivalence checking, and visual checking. Taking as input filename.lotos, which contains a LOTOS specification, optionally accompanied by filename.h, which provides C types and functions implementing the LOTOS sorts and operations defined in filename.lotos, caesar performs successive transformation steps and produces a C program that allows to execute, simulate, and/or build the corresponding graph. In the latter case, the result of caesar is the graph itself, rather than the C program, which is removed after its execution.