SLAyer
SLAyer

The SLAyer research project is focused on developing methods for automatic formal verification of code that manipulates heap-allocated linked data structures.

SLAyer is an automatic formal verification tool in development within Microsoft Research which is aimed at proving properties of programs that may involve reasoning inductively about data-structures. This is in response to the shortfalls of first-generation software model checking tools, like SLAM or BLAST, which are able only to build a shallow finite approximation of the data-structures created during a program's execution.

The initial goal of the SLAyer project is to develop an automatic tool that will allow us to prove non-trivial properties of data-structures constructed during the execution of industrial software components with 100,000 lines of code or less.

SLAyer's home is at the Microsoft Research laboratory at Cambridge University. SLAyer is a member of the East London Massive, and also has many ties to the TERMINATOR project.

Collaborators: Cristiano Calcagno, Dino Distefano, Peter O'Hearn, Mooly Sagiv, Hongseok Yang. Interns: Sergii Avilov, Nathan Chong, Arlen Cox, Alexey Gotsman, Christoph HaaseJael Kriener, Stephen Magill, Jacopo Mantovani, Thomas Wies, Greta Yorsh.

Try it

Downloads
People
Josh Berdine
Josh Berdine

Byron Cook
Byron Cook

Samin Ishtiaq
Samin Ishtiaq

Matthew Parkinson
Matthew Parkinson

Publications