Gold sponsors

IBM Corporation

Jasmine Conseil logo

Cloudsoft logo

Sonatype logo

SAP logo

Xored logo

Oracle

Amazon logo

Silver sponsors

Blackberry logo

ZeroTurnaround logo

Amazon Web Services logo

bsi logo

OnPositive logo

Google

Nuxeo logo

Actuate

Bronze sponsors

github

froglogic

Microsoft logo

Paremus logo

JBoss logo

Genuitec logo

Juniper logo

Soyatec logo

itemis logo

Totvs logo

AccuRev logo

Activity sponsor

eclipsesource

Media sponsors

Methods & Tools logo


Practical Mathematical Proof of Correctness

Frank Rimlinger

Making with Eclipse · Standard
Thursday, 14:00, 20 minutes | Stevens Creek

Tags:
7
·
8
·
9
·
10
·
11
·
12
·
13
·
14
·
15
·
16
·
17
·
18

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 (frankrimlinger@gmail.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).

Slides

Download Material

Download file of related material.