About SLAyer
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.
Research Papers
Scalable shape analysis for systems code
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn
CAV'08 (Princeton)
Local reasoning for storable locks and threads
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
APLAS'07
(Singapore)
Shape analysis by graph decomposition
Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv
TACAS'07 (Braga)
Arithmetic strengthening for shape analysis
Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.
SAS'07
(Denmark)
Shape analysis for composite data structures
Josh Berdine,
Cristiano Calcagno,
Byron Cook,
Dino Distefano,
Peter O'Hearn,
Thomas Wies,
Hongseok Yang
CAV'07 (Berlin)
Thread-modular shape analysis
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
PLDI'07 (San Diego)
Automatic termination
proofs for programs with shape-shifting heaps
Josh Berdine, Byron Cook, Dino Distefano, Peter O'Hearn
CAV'06 (Seattle)
Interprocedural shape
analysis with separated heap abstractions
Alexey Gotsman, Josh Berdine, Byron Cook
SAS'06 (Seoul)