The paper "Verifying LTL properties of hybrid systems with K-liveness" by Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta has been published in the proceedings of the International Conference on Computer-Aided Verification (CAV 2014). The paper presents a new algorithm to verify temporal properties of hybrid automata. This algorithm is used in D-MILS to verify functional, real-time and safety properties of MILS-AADL models.