Making with Eclipse · Standard
Thursday, 14:00, 20 minutes | Stevens Creek
Proof of correctness of software is theoretically well understood, but rarely applied. Difficulties abound, from mathematical undecidability to philosophical chicken-and-egg questions to practical case explosion. Integration of development and proof on a pay-as-you-go basis overcomes all these problems. Evolution of this process will make correctness a routine byproduct of software development. The transcript and slides for the talk may be found at EclipseCon 2011 Slides
Frank Rimlinger (email@example.com) received his Ph.D. from the University of California at Berkeley, 1985. He worked for ten years as a research mathematician in the field of Combinatorial Group Theory and Low-Dimensional Topology. His thesis was published as AMS Memoir 361, Pregroups and Bass-Serre theory. Frank joined the National Security Agency in 1995, and for the last ten years has worked in the field of software assurance. He is the inventor of US Patent 7,788,659 B1, Method of converting computer program with loops to one without loops. In 2007 this technology was transferred to the NASA Software Release Authority, and is currently available as an open-source technology, the high-assurance software tool Mango, under the NOSA 1.3 license (NASA Open Source Agreement).