Mosel: A flexible toolset for monadic second-order logic. Mosel is a new tool-set for the analysis and verification in Monadic Second-order Logic. In this paper we concentrate on the system’s design: Mosel is a tool-set to include a flexible set of decision procedures for several theories of the logic complemented by a variety of support components for input format translations, visualization, and interfaces to other logics and tools. The main distinguishing features of Mosel are its layered approach to the logic, based on a formal semantics for a minimal subset, its modular design, and its integration in a heterogeneous analysis and verification environment.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Abdulla, Parosh Aziz; Sistla, A. Prasad; Talupur, Muralidhar: Model checking parameterized systems (2018)
- Lamprecht, Anna-Lena; Margaria, Tiziana; Steffen, Bernhard: Bio-jeti: a framework for semantics-based service composition (2009) ioport
- Klarlund, Nils: Relativizations for the logic-automata connection (2005)
- Rogers, James: wMSO theories as grammar formalisms (2003)
- Ayari, Abdelwaheb; Basin, David; Podelski, Andreas: LISA: A specification language based on WS2S (1998)