Formal methods in the THETA kernel. - Mike Seager; David Guaspari; Matthew Stillerman; Carla Marceau (S&P, 1995)