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.


References in zbMATH (referenced in 20 articles , 1 standard article )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Rabe, Florian; Kohlhase, Michael: A scalable module system (2013)
  2. Iancu, Mihnea; Rabe, Florian: Management of change in declarative languages (2012)
  3. Bundy, Alan: Automated theorem provers: a practical tool for the working mathematician? (2011)
  4. Bortin, Maksym; Lüth, Christoph: Structured formal development with quotient types in Isabelle/HOL (2010)
  5. Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
  6. Dietrich, Dominik; Schulz, Ewaryst; Wagner, Marc: Authoring verified documents by interactive proof construction and verification in text-editors (2008)
  7. Rowinska-Schwarzweller, Agnieszka; Schwarzweller, Christoph: Towards mathematical knowledge management for electrical engineering (2007)
  8. Wagner, Marc; Autexier, Serge; Benzmüller, Christoph: Platomega: A mediator between text-editors and proof assistance systems. (2007)
  9. Ballarin, Clemens: Interpretation of locales in Isabelle: theories and proof contexts (2006)
  10. Normann, Immanuel: Enhanced theorem reuse by partial theory inclusions (2006)
  11. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
  12. Wassyng, Alan; Lawford, Mark: Software tools for safety-critical software development (2006)
  13. Hutter, Dieter; Autexier, Serge: Formal software development in MAYA (2005)
  14. Krieg-Brückner, Bernd: Towards multimedia instruction in safe and secure systems (2005)
  15. Mantel, Heiko; Schairer, Axel: Exploiting generic aspects of security models in formal developments (2005)
  16. Johnsen, Einar Broch; Lüth, Christoph: Theorem reuse by proof term transformation (2004)
  17. Moreira, Anamaria Martins; De Oliveira, Anderson Santana: Simulating algebraic specification genericity on languages with initial semantics. (2004)
  18. Hutter, Dieter: Deduction as an engineering science. (2003)
  19. Johnsen, Einar Broch; Lüth, Christoph: Abstracting refinements for transformation (2003)
  20. Kohlhase, Michael; Anghelache, Romeo: Towards collaborative content management and version control for structured mathematical knowledge (2003)