Verification and Automatic Reasoning Group
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.
Recent Papers
SLAyer: Memory Safety for Systems-Level Code
Josh Berdine,
Byron Cook,
Samin Ishtiaq
CAV'11 (Snowbird)
Making prophecies with decision predicates
Byron Cook,
Eric Koskinen
POPL'11 (Austin)
Proving stabilization of biological systems
Byron Cook,
Jasmin Fisher,
Elzbieta Krepska,
Nir Piterman
VMCAI'11 (Austin)
Projects
Publications
- Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang, Views: Compositional Reasoning for Concurrent Programs, in Proceedings of POPL, 2013
- John Wickerson, Mike Dodds, and Matthew Parkinson, Ribbon Proofs for Separation Logic, in Proceedings of ESOP, 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
- Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, and Matthew J. Parkinson, jStar-eclipse: an IDE for automated verification of Java programs, in SIGSOFT FSE, 2011
- Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson, Safe asynchronous multicore memory operations, in ASE, 2011
Tools
Download SLAyer.zip
