The MOSEL team shares members of the EPC VERIDIS, which is a joint project with MPI Saarbrucken. MOSEL contributes methodologies, techniques, and tools for developing trustworthy software based on formal models endowed with a precise semantics. Properties of these models are established using techniques such as state space exploration and formal proof, and models at different levels of abstraction are related by the key notion of refinement, ensuring that properties verified at an abstract level are preserved by an implementation. Event-B and TLAPLUS are the two main formal frameworks to which we contribute. Our objective is to assist designers of algorithms and systems by providing highly automated techniques for finding bugs and proving correctness. We especially target the verification of concurrent and distributed algorithms and systems, with applications ranging from embedded systems on multiple cores to algorithms for the cloud. We contribute to advances in deductive verification, including automatic theorem proving, SMT solving, and their integration in interactive platforms for system development, such as Rodin or \tlaps. This includes identifying decidable fragments of first-order or higher-order logics, and reasoning about theories such as arithmetic that are fundamental for verification. Our conceptual work gives rise to the development of robust software tools and is accompanied by carrying out significant case studies that feed back into fundamental research.
The annual report of the year 2014 is available.