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.
Collaborators: Cristiano Calcagno, Dino Distefano, Peter O'Hearn, Mooly Sagiv, Hongseok Yang. Interns: Sergii Avilov, Nathan Chong, Arlen Cox, Alexey Gotsman, Christoph Haase, Jael Kriener, Stephen Magill, Jacopo Mantovani, Thomas Wies, Greta Yorsh.
The SLAyer source has been released under the MIT license.
- Josh Berdine and Nikolaj Bjørner, Computing All Implied Equalities via SMT-based Partition Refinement, no. MSR-TR-2014-57, April 2014.
- Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, and Christoph M. Wintersteiger, Resourceful Reachability as HORN-LA, in International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Springer, 15 December 2013.
- Christoph Haase, Samin Ishtiaq, Joel Ouaknine, and Matthew Parkinson, SeLoger: A Tool for Graph-Based Reasoning in Separation Logic , in Computer Aided Verification (CAV), 2013.
- Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph M. Wintersteiger, Diagnosing Abstraction Failure for Separation Logic-based Analyses, in Proceedings of the 24th International Conference on Computer Aided Verification (CAV), Springer, July 2012.
- Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph M. Wintersteiger, Diagnosing Abstraction Failure for Separation Logic-based Analyses, no. MSR-TR-2012-44, April 2012.
- Josh Berdine, Byron Cook, and Samin Ishtiaq, SLAyer: Memory Safety for Systems-level Code, in CAV, 2011.
- Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn, Scalable Shape Analysis for Systems Code, in Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, Springer Verlag, 2008.
- Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, and Josh Berdine, Heap Decomposition for Concurrent Shape Analysis, in Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings, Springer Verlag, 2008.
- Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv, Thread-Modular Shape Analysis, in Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, ACM, 2007.
- Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv, Shape Analysis by Graph Decomposition, in Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, Springer Verlag, 2007.
- Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, and Hongseok Yang, Shape Analysis for Composite Data Structures, in Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, Springer, 2007.
- Stephen Magill, Josh Berdine, Edmund M. Clarke, and Byron Cook, Arithmetic Strengthening for Shape Analysis, in Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings, Springer Verlag, 2007.
- Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv, Local Reasoning for Storable Locks and Threads, in Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings, Springer Verlag, 2007.
- Alexey Gotsman, Josh Berdine, and Byron Cook, Interprocedural Shape Analysis with Separated Heap Abstractions, in Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings, Springer, 2006.
- Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O'Hearn, Automatic Termination Proofs for Programs with Shape-Shifting Heaps, in Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Springer, 2006.