We had a paper accepted to MEMOCODE 2015. The paper describes preliminary work implementing and formally verifying in Coq an upper bound altitude monitor and and upper bound vertical velocity monitor for a quadcopter. Check it out here.

Let us know if you’re going to be at MEMOCODE this year. We’d love to chat with you.