Specware

Specware is a software engineering tool that automatically generates high-assurance software. Specware is a leading-edge automated software development system that allows users to precisely specify the desired functionality of their applications and to generate provably correct code based on these requirements. At the core of the design process in Specware lies stepwise refinement, in which users begin with a simple, abstract model of their problem and iteratively refine this model until it uniquely and concretely describes their application.


References in zbMATH (referenced in 25 articles )

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

1 2 next

  1. Healy, Michael J.; Caudell, Thomas P.: Episodic memory: a hierarchy of spatiotemporal concepts (2019)
  2. Rabe, Florian; Sharoda, Yasmine: Diagram combinators in MMT (2019)
  3. Kovalyov, S. P.: Category-theoretic approach to software systems design (2016)
  4. Macedo, Hugo D.; Haeusler, Edward H.; Garcia, Alex: Defining effectiveness using finite sets. A study on computability (2016)
  5. Kovalev, S. P.: Systems analysis of life cycle of large-scale information-control systems (2013)
  6. Graves, Henson; Bijan, Yvonne: Using formal methods with SysML in aerospace design and engineering (2011)
  7. Klein, Gerwin: Operating system verification---an overview (2009)
  8. Tomasik, Jerzy; Weyman, Jerzy: Category localization semantics for specification refinements (2007)
  9. Smith, Douglas R.: Composition by colimit and formal software development (2006)
  10. Johnsen, Einar Broch; Lüth, Christoph: Theorem reuse by proof term transformation (2004)
  11. Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
  12. Durán, Francisco; Meseguer, José: Structured theories and institutions (2003)
  13. Roşu, Grigore; Venkatesan, Ram Prasad; Whittle, Jon; Leuştean, Laurenţiu: Certifying optimality of state estimation programs. (2003)
  14. Flener, Pierre: Achievements and prospects of program synthesis (2002)
  15. Gibbons, Jeremy: Towards a colimit-based semantics for visual programming (2002)
  16. Hall, Robert J.: Specification, validation, and synthesis of email agent controllers: A case study in function rich reactive system design (2002)
  17. Coglio, Alessandro; Goldberg, Allen: Type safety in the JVM: Some problems in Java 2 SDK 1. 2 and proposed solutions (2001)
  18. Colvin, Robert; Hayes, Ian; Strooper, Paul: A technique for modular logic program refinement (2001)
  19. Williamson, Keith; Healy, Michael; Barker, Richard: Industrial applications of software synthesis via category theory -- case studies using specware (2001)
  20. Allen, Stuart F.; Constable, Robert L.; Eaton, Rich; Kreitz, Christoph; Lorigo, Lori: The Nuprl open logical environment (2000)

1 2 next