blazing fast symbolic analysis for concurrent C programs
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
BoogieBinaries
Source/Driver
Test
.gitignore
LICENSE
README.md
lockpwn.sln

README.md

lockpwn

A lightweight, blazing fast symbolic analyser for concurrent C programs.

Build instructions

  1. Clone this project.
  2. Compile using Visual Studio or Mono.

How to use

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

Tool options

Use /v for verbose mode or /v2 for super verbose mode. Use /time for timing information.

Publications