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 114 articles )

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

1 2 3 4 5 6 next

  1. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  2. Broy, Manfred: Theory and methodology of assumption/commitment based system interface specification and architectural contracts (2018)
  3. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  4. 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)
  5. Amin, Nada; Rompf, Tiark: LMS-verify: abstraction without regret for verified systems programming (2017)
  6. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  7. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  8. 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)
  9. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  10. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  11. Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015)
  12. 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)
  13. Leino, K. Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  14. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  15. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  16. Din, Crystal Chang; Owe, Olaf: A sound and complete reasoning system for asynchronous communication with shared futures (2014)
  17. Itzhaky, Shachar; Banerjee, Anindya; Immerman, Neil; Lahav, Ori; Nanevski, Aleksandar; Sagiv, Mooly: Modular reasoning about heap paths via effectively propositional formulas (2014)
  18. Almeida, J. Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara: Formal verification of side-channel countermeasures using self-composition (2013)
  19. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  20. Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)

1 2 3 4 5 6 next