AIC Seminar Series

We discuss the generation of concurrent garbage collectors by an automated refinement process in Kestrel’s Specware system. Starting from a formal specification of requirements, we apply a sequence of transformations that generate correct-by-construction refinements, ultimately resulting in the generation of efficient compilable code.

To handle the specification and refinement of stateful/concurrent processes, we are developing techniques for a mixed algebraic/coalgebraic-style of specification within the higher-order logic of Specware’s MetaSlang language. In addition to generic techniques for algorithm design, we developed new coalgebraically-oriented techniques for invariant maintenance and refining the types of observers. We generate refinements using purely functional calculation based on the axioms and theorems of the domain specification. Our goal is to generate code and proofs at the same time. As a final step, we transform the coalgebraic operators to stateful form and encapsulate the top-level processes as threads.

Dr. Douglas R. Smith is a Principal Scientist at Kestrel Institute and serves as President of Kestrel Technology LLC (both in Palo Alto). He is a Fellow of the American Association of Artificial Intelligence (AAAI) and an ASE Fellow (Automated Software Engineering). During 1986-2000, he periodically taught an advanced graduate course on knowledge-based software development at Stanford University. Dr. Smith served as Chairman of IFIP Working Group 2.1 on Algorithmic Languages and Calculi during 1994-2000.

Dr. Smith’s research interests have centered around formal specifications, automated inference, and program synthesis. He has led the development of a series of software synthesis systems, including KIDS (Kestrel Interactive Development System), Specware, Designware, and Planware. Applications have included a variety of complex high-performance schedulers for the US Air Force.

Dr. Smith has over 30 years experience in the field of automated program synthesis and has published over 100 papers. He has one patent. He received the Ph.D. in Computer Science from Duke University in 1979.

Please arrive at least 10 minutes early in order to sign in and be escorted to the conference room. SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the visitors lot in front of Building E, and should follow the instructions by the lobby phone to be escorted to the meeting room. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page.

©2013 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy