CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions.For the pigeon-hole principle I understand that the constraints are:Each Pigeon is in some Hole.Two different Pigeon can't be in same hole.Let's take an example of 4 pigeons and 3 holes. I need to convert this into a CBMC check. I'm trying using two for loops, but I can't find how to do it.
Encoding the pigeonhole principle in CBMC
satisfiability;discrete mathematics;software verification;program verification
If I understand correctly, you're actually looking for a technique to check if an out-of-bounds condition exists (more pigeons than pigeonholes).Here's some example code that fits your analogy. I think you're asking about this technique as an analogy to whatever problem you're actually trying to encode, but next time be direct with what problem you want to solve rather than an analogy :)/* pigeonhole.c */int main() {  _Bool holes_occupied[3];  unsigned int pigeon;  for (pigeon = 0; pigeon < 4; ++pigeon) {    holes_occupied[pigeon] = 1;  }  return 0;}Run with:cbmc --bounds-check pigeonhole.cVERIFICATION FAILED (with error trace)