Hello; I'm working on a couple of C projects and I'd like to use automated theorem proving to validate the code. Ideally I'd just like to use the ATP to validate the functions contracts. Is there any functionality in C/gcc or external software/packages/etc that would enable design-by-contract style coding?
If not then thats just incentive to get started on my own.
My references for this would be something like Spec# or Sing# from MSR, but I'm an open source guy and I'm looking for open source solutions.