VCC

VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications.


References in zbMATH (referenced in 66 articles )

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

1 2 3 4 next

  1. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  2. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos: System-level non-interference of constant-time cryptography. I: Model (2019)
  3. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  4. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  5. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  6. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Gardner, Philippa: A perspective on specifying and verifying concurrent modules (2018)
  7. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  8. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  9. Roşu, Grigore: Matching logic (2017)
  10. Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei: The spirit of ghost code (2016)
  11. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  12. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  13. Leino, K. Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  14. Nemati, Hamed; Guanciale, Roberto; Dam, Mads: Trustworthy virtualization of the ARMv7 memory subsystem (2015) ioport
  15. O’Hearn, Peter W.; Petersen, Rasmus L.; Villard, Jules; Hussain, Akbar: On the relation between concurrent separation logic and concurrent Kleene algebra (2015)
  16. Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)
  17. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  18. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  19. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  20. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A precise and abstract memory model for C using symbolic values (2014)

1 2 3 4 next