A lightweight, blazing fast symbolic analyser for concurrent C programs.
- Clone this project.
- Compile using Visual Studio or Mono.
The input to lockpwn is a concurrent C program translated to the Boogie intermediate verification language using the SMACK LLVM-to-Boogie translator.
Given an input ${PROGRAM} in Boogie, do the following:
.\lockpwn.exe ${PROGRAM}.bpl
lockpwn can also easily integrate with Microsoft's Corral bounded bugfinder. This can be achieved as follows:
.\lockpwn.exe ${PROGRAM}.bpl /corral
The output, ${OUTPUT}.bpl, is an instrumented with context-switches (yields) Boogie program. This can be directly fed to Corral using the /cooperative option (so Corral does not automatically instrument yield statements).
Use /v for verbose mode or /v2 for super verbose mode. Use /time for timing information.
- Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers. Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamarić. In the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2015.