|
1/24/2008: 15:00—15:50 at Glasgow East 117
John D. Ramsdell of the MITRE Corporation will speak in this CS Department Seminar.
Practical application of formal methods to high assurance software development requires careful engineering tradeoffs. For modest sized tasks, we have found success by using prototyping to drive the design specification and verification as well as using the design to drive the coding.
The genesis of these ideas was as a result of the construction of a formally verified implementation of a programming language (Scheme) in the early 1990s. The talk will describe the use of these ideas in the modern context of implementing a protocol analysis tool, along with the newly developed technique of purposely prototyping the same algorithm in more than one language.
Bio: John D. Ramsdell holds a Ph.D. in Applied Mathematics from Harvard University. He has been employed by The MITRE Corporation since 1983.
Dr. Ramsdell specializes in distributed computing, especially as it relates to computer security and computer supported cooperative workspaces. His activities contributed to the implementation of a simple, secure, distributed instant messaging system called SIMP. His computer security work includes protocol analysis.
In the past, Dr. Ramsdell specialized in formal verification, and programming languages with a special interest in parallel and functional programming. His activities have contributed to the construction of a verified processor which executes functional programs, and the construction of a formally verified implementation of a programming language (Scheme).
Please contact Prof. Squire with questions.
View the flyer here.
|
