MAYA
The formal development of industrial-size software is an error-prone and therefore an evolutionary process. Verifying formal specifications usually reveals hidden errors causing the change of parts of the specification. Also adding new functionality will result in changes of the specification which always endangers the verification work already done. In this paper we describe the system Maya which maintains formal developments. The Maya-system supports an evolutionary formal development since it allows users to specify and verify developments in a structured manner, incorporates a uniform mechanism for verification in-the-large to exploit the structure of the specification, and maintains the verification work already done when changing the specification. Maya relies on development graphs as a uniform representation of structured specifications, which enables the use of various (structured) specification languages to formalize the software development. Moreover, Maya allows the integration of different theorem provers to deal with the actual proof obligations arising from the specification, i.e. to perform verification in-the-small.
Keywords for this software
References in zbMATH (referenced in 25 articles , 1 standard article )
Showing results 1 to 20 of 25.
Sorted by year (- Autexier, Serge; Hutter, Dieter: Structure formation in large theories (2015)
- Stefaneas, Petros; Ouranos, Iakovos; Triantafyllou, Nikolaos; Ksystra, Katerina: Some engineering applications of the OTS/CafeOBJ method (2014)
- Rabe, Florian; Kohlhase, Michael: A scalable module system (2013)
- Iancu, Mihnea; Rabe, Florian: Management of change in declarative languages (2012)
- Bundy, Alan: Automated theorem provers: a practical tool for the working mathematician? (2011)
- Autexier, Serge; Hutter, Dieter; Mossakowski, Till: Change management for heterogeneous development graphs (2010)
- Bortin, Maksym; Lüth, Christoph: Structured formal development with quotient types in Isabelle/HOL (2010)
- Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
- Dietrich, Dominik; Schulz, Ewaryst; Wagner, Marc: Authoring verified documents by interactive proof construction and verification in text-editors (2008)
- Rowinska-Schwarzweller, Agnieszka; Schwarzweller, Christoph: Towards mathematical knowledge management for electrical engineering (2007)
- Wagner, Marc; Autexier, Serge; Benzmüller, Christoph: Plat$\Omega$: a mediator between text-editors and proof assistance systems (2007)
- Ballarin, Clemens: Interpretation of locales in Isabelle: theories and proof contexts (2006)
- Normann, Immanuel: Enhanced theorem reuse by partial theory inclusions (2006)
- Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
- Wassyng, Alan; Lawford, Mark: Software tools for safety-critical software development (2006) ioport
- Hutter, Dieter; Autexier, Serge: Formal software development in MAYA (2005)
- Krieg-Brückner, Bernd: Towards multimedia instruction in safe and secure systems (2005)
- Mantel, Heiko; Schairer, Axel: Exploiting generic aspects of security models in formal developments (2005)
- Johnsen, Einar Broch; Lüth, Christoph: Theorem reuse by proof term transformation (2004)
- Siekmann, Jörg; Benzmüller, Christoph: $\Omega$MEGA: Computer supported mathematics (2004)