Skip to content
This repository has been archived by the owner on Aug 25, 2022. It is now read-only.
/ SLAyer Public archive

SLAyer is an automatic formal verification tool that uses separation logic to verify memory safety of C programs.

License

Notifications You must be signed in to change notification settings

microsoft/SLAyer

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

9 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

About

SLAyer is an automatic formal verification tool that uses separation logic to verify memory safety of C programs.

Licence

SLAyer is licensed under the MIT licence included in the LICENSE file.

Setup

Building and testing SLAyer has some dependencies on the environment. To set this up, start in a VS 201x shell. Then enter a bash shell, cd to here, and execute:

$ source config.sh

To build SLAyer:

$ cd src; make; cd ..

The slayer.exe will be left in the bin directory.

See src/README for additional building instructions.

To run the tests:

Start a new VS2010+bash shell, and cd to here. (The reason to start a new shell is that SLAyer is built using the usual VS compiler, but when slayer runs on tests, it needs to run the WDK compiler.)

$ source ./config.sh $ cd test; source config.sh

$ cd sll $ slayer -vSE 3 -vAbs 2 traverse.c

See test/README for additional testing instructions.

Contributing

To contribute, you will need to complete a Contributor License Agreement (CLA). Briefly, this agreement testifies that you are granting us permission to use the submitted change according to the terms of the project's license, and that the work being submitted is under appropriate copyright.

Please submit a Contributor License Agreement (CLA) before submitting a pull request. You may visit https://cla.microsoft.com to sign digitally. Alternatively, download the agreement Microsoft Contribution License Agreement.docx or Microsoft Contribution License Agreement.pdf), sign, scan, and email it back to [email protected]. Be sure to include your github user name along with the agreement. Once we have received the signed CLA, we'll review the request.

Papers

Josh Berdine, Byron Cook, Samin Ishtiaq. SLAyer: Memory Safety for Systems-level Code. In CAV, January 1, 2011. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/201120CAV20SLAyer_20Memory20Safety20for20Systems-level20Code.pdf

Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger. Diagnosing Abstraction Failure for Separation Logic-based Analyses. In CAV, July 1, 2012. https://www.microsoft.com/en-us/research/publication/diagnosing-abstraction-failure-for-separation-logic-based-analyses/

Josh Berdine, Nikolaj Bjorner, Samin Ishtiaq, Christoph M. Wintersteiger. Resourceful Reachability as HORN-LA. In CAV, December 15, 2013. https://www.microsoft.com/en-us/research/publication/resourceful-reachability-as-horn-la/

Christoph Haase, Samin Ishtiaq, Joel Ouaknine, Matthew Parkinson. SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. In CAV, January 1, 2013. https://www.microsoft.com/en-us/research/publication/seloger-a-tool-for-graph-based-reasoning-in-separation-logic/

About

SLAyer is an automatic formal verification tool that uses separation logic to verify memory safety of C programs.

Resources

License

Code of conduct

Security policy

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published