The members of this group are interested in developing tools and methods for reasoning about complex systems. Example application areas include operating systems, biological systems, or distributed algorithms. Particular projects include the SLAyer shape analysis engine, the Terminator termination prover, and BioCheck modelling and analysis tool for gene regulatory networks.
SLAyer: Memory Safety for Systems-Level Code
Making prophecies with decision predicates
Proving stabilization of biological systems
- Alexey Bakhirkin, Josh Berdine, and Nir Piterman, Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction, no. MSR-TR-2014-82, June 2014.
- 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.
- John Wickerson, Mike Dodds, and Matthew Parkinson, Ribbon Proofs for Separation Logic, in Proceedings of ESOP, 2013.
- Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang, Views: Compositional Reasoning for Concurrent Programs, in Proceedings of POPL, 2013.
- Kasper Svendsen, Lars Birkedal, and Matthew Parkinson, Modular Reasoning about Separation for Concurrent Data Structures, in Proceedings of ESOP, 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.
- Matthew J. Parkinson and Alexander J. Summers, The Relationship Between Separation Logic and Implicit Dynamic Frames, in Logical Methods in Computer Science, vol. 8, no. 3, 2012.
- Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson, Automatic safety proofs for asynchronous memory operations, in PPOPP, 2011.