Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

AIC Seminar Series

Synthesis of Concurrent Garbage Collectors

Douglas R. SmithKestrel Institute[Home Page]

Notice:  Hosted by Richard Waldinger

Date:  2011-08-25 at 16:00

Location:  EJ228 (SRI E building)  (Directions)


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.

   Bio for Douglas R. Smith

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.

   Note for Visitors to SRI

Please arrive at least 10 minutes early as you will need to sign in by following instructions by the lobby phone at Building E. (or call Wilma Lenz at 650 859 4904, or Vicenta at Lopez at 650 859 5750). SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the parking lots off Fourth Street. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page. There are two entrances to SRI International located on Ravenswood Ave. Please check the Builing E entrance signage.

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