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

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

1 2 3 4 5 next

  1. 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)
  2. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  3. Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015)
  4. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  5. Din, Crystal Chang; Owe, Olaf: A sound and complete reasoning system for asynchronous communication with shared futures (2014)
  6. Itzhaky, Shachar; Banerjee, Anindya; Immerman, Neil; Lahav, Ori; Nanevski, Aleksandar; Sagiv, Mooly: Modular reasoning about heap paths via effectively propositional formulas (2014)
  7. Almeida, J.Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara: Formal verification of side-channel countermeasures using self-composition (2013)
  8. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  9. Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
  10. Barros, José Bernardo; da Cruz, Daniela; Henriques, Pedro Rangel; Pinto, Jorge Sousa: Assertion-based slicing and slice graphs (2012)
  11. Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
  12. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  13. Heidegger, Phillip; Bieniusa, Annette; Thiemann, Peter: Access permission contracts for scripting languages (2012)
  14. Hills, Mark; Chen, Feng; Roşu, Grigore: A rewriting logic approach to static checking of units of measurement in C (2012)
  15. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  16. Sonnex, William; Drossopoulou, Sophia; Eisenbach, Susan: Zeno: an automated prover for properties of recursive data structures (2012)
  17. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  18. Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo: On deciding satisfiability by theorem proving with speculative inferences (2011)
  19. Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco: A parametric segmentation functor for fully automatic and scalable array content analysis (2011)
  20. Huisman, Marieke; Gurov, Dilian: CVPP: a tool set for compositional verification of control-flow safety properties (2011)

1 2 3 4 5 next