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.

References in zbMATH (referenced in 121 articles )

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

1 2 3 ... 5 6 7 next

  1. Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
  2. Bansal, Kshitij; Koskinen, Eric; Tripp, Omer: Synthesizing precise and useful commutativity conditions (2020)
  3. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  4. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  5. Broy, Manfred: Theory and methodology of assumption/commitment based system interface specification and architectural contracts (2018)
  6. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  7. Swords, Cameron; Sabry, Amr; Tobin-Hochstadt, Sam: An extended account of contract monitoring strategies as patterns of communication (2018)
  8. 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)
  9. Amin, Nada; Rompf, Tiark: LMS-verify: abstraction without regret for verified systems programming (2017)
  10. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  11. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  12. 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)
  13. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  14. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  15. Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015) ioport
  16. 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)
  17. Leino, K. Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  18. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  19. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  20. 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)

1 2 3 ... 5 6 7 next