ConCEGAR

An old SMT-based Model Checking project that handles shared-memory concurrency through CEGAR. Rather than directly encoding the concurrency semantics, it filters out spurious counterexamples.

The expected inputs are (limited fragments of) C programs that have been compiled into LLVM-IR.

Requirements

Working haskell environment and LLVM-9.

Build

stack build

Run

stack run input.ll

Example Input

#include <stdbool.h>
int x,y,a,b,fence;

bool assert(bool);
void par(void * (*)(void *), ...);
int faa(int *, int);

void * f(void * _) {
    x = 1;
    faa(&fence, 0);
    a = y;
    return 0;
}

void * g(void * _) {
    y = 1;
    faa(&fence, 0);
    b = x;
    return 0;
}

int main() {
    par(f,g);
    assert(a || b);
    return 0;
}

and clang -S -emit-llvm input.c