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)
Publications
- 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
Tools
Download SLAyer.zip
