Efficient software model checking of soundness of type systems. - Michael Roberson; Melanie Harries; Paul T. Darga; Chandrasekhar Boyapati (OOPSLA, 2008)