Spec#

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec# programming system, consisting of the object-oriented Spec# programming language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs for writing specifications that capture programmer intentions about how methods and data are to be used, the compiler emits run-time checks to enforce these specifications, and the verifier can check the consistency between a program and its specifications.

This software is also peer reviewed by journal TOMS.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 120 articles )

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

1 2 3 4 5 6 next

  1. Bansal, Kshitij; Koskinen, Eric; Tripp, Omer: Synthesizing precise and useful commutativity conditions (2020)
  2. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  3. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  4. Broy, Manfred: Theory and methodology of assumption/commitment based system interface specification and architectural contracts (2018)
  5. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  6. Swords, Cameron; Sabry, Amr; Tobin-Hochstadt, Sam: An extended account of contract monitoring strategies as patterns of communication (2018)
  7. Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (2017)
  8. Amin, Nada; Rompf, Tiark: LMS-verify: abstraction without regret for verified systems programming (2017)
  9. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  10. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  11. Galán, Francisco J.; Cañete-Valdeón, José M.: Synthesis of positive logic programs for checking a class of definitions with infinite quantification (2016)
  12. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  13. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  14. Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015) ioport
  15. Dastani, Mehdi (ed.); Sirjani, Marjan (ed.): Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers (2015)
  16. Leino, K. Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  17. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  18. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  19. Böhl, Florian; Greiner, Simon; Scheidecker, Patrik: Proving correctness and security of two-party computation implemented in Java in presence of a semi-honest sender (2014)
  20. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv

1 2 3 4 5 6 next