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

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

1 2 3 next

  1. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  2. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Gardner, Philippa: A perspective on specifying and verifying concurrent modules (2018)
  3. Filli^atre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei: The spirit of ghost code (2016)
  4. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  5. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  6. Leino, K. Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  7. Nemati, Hamed; Guanciale, Roberto; Dam, Mads: Trustworthy virtualization of the ARMv7 memory subsystem (2015)
  8. O’Hearn, Peter W.; Petersen, Rasmus L.; Villard, Jules; Hussain, Akbar: On the relation between concurrent separation logic and concurrent Kleene algebra (2015)
  9. Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)
  10. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  11. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  12. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A precise and abstract memory model for C using symbolic values (2014)
  13. Daum, Matthias; Billing, Nelson; Klein, Gerwin: Concerned with the unprivileged: user programs in kernel refinement (2014)
  14. Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)
  15. Meyer, Bertrand; Kogtenkov, Alexander: Negative variables and the essence of object-oriented programming (2014)
  16. Moore, J Strother: Proof pearl: proving a simple von Neumann machine Turing complete (2014)
  17. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  18. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  19. Cousot, Patrick; Cousot, Radhia; Fähndrich, Manuel; Logozzo, Francesco: Automatic inference of necessary preconditions (2013)
  20. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)

1 2 3 next