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

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

1 2 next

  1. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  2. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015)
  3. O’Hearn, Peter W.; Petersen, Rasmus L.; Villard, Jules; Hussain, Akbar: On the relation between concurrent separation logic and concurrent Kleene algebra (2015)
  4. Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)
  5. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  6. Daum, Matthias; Billing, Nelson; Klein, Gerwin: Concerned with the unprivileged: user programs in kernel refinement (2014)
  7. Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)
  8. Moore, J Strother: Proof pearl: proving a simple von Neumann machine Turing complete (2014)
  9. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  10. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  11. Cousot, Patrick; Cousot, Radhia; Fähndrich, Manuel; Logozzo, Francesco: Automatic inference of necessary preconditions (2013)
  12. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  13. Bjørner, Nikolaj: Taking satisfiability to the next level with Z3. (Abstract) (2012)
  14. Greenaway, David; Andronick, June; Klein, Gerwin: Bridging the gap: automatic verified abstraction of C (2012)
  15. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  16. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  17. Siegel, Stephen F.; Zirkel, Timothy K.: Loop invariant symbolic execution for parallel programs (2012)
  18. Backes, Michael; Hriţcu, Cătălin; Tarrach, Thorsten: Automatically verifying typing constraints for a data processing language (2011)
  19. Böhme, Sascha; Moskal, Michał: Heaps and data structures: a challenge for automated provers (2011)
  20. Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: A formal and fast reference implementation of Skein (2011)

1 2 next