# Encoding the pigeonhole principle in CBMC

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, ex­cep­tions and user-specified as­ser­tions.

For the pigeon-hole principle I understand that the constraints are:

1. Each Pigeon is in some Hole.
2. 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.

• Could you try to state more precisely what you're trying to do and what you've tried? I can't understand your question at all. – David Richerby Nov 16 '14 at 14:47
• I want to encode Pigeon hole's principle in CBMC . How should i encode at least the first constrain . – Pushpa Nov 16 '14 at 14:54
• This seems to be more of an Stack Overflow question than a Computer Science question since it's about using the programming tool CBMC. It's borderline, though: how to encode the property in CBMC's logic is CS. Unfortunately neither SO nor CS.SE has any existing question about CBMC, so the chances of finding experts are slim. You might be better off trying on a CBMC mailing list, if there is one. – Gilles Nov 16 '14 at 22:17

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.c

VERIFICATION FAILED (with error trace)