Dr. Douglas R. Smith

DRS
Contact
e-mail:

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

Dr. Smith’s research interests have centered on correct-by-construction program synthesis, formal specifications, algorithm and system design theories, planning/scheduling algorithms, the automatic enforcement of cross-cutting safety and security policies, and system code generation from formalized design patterns and software architectures. Recent projects have focused on generation of complex air operations plans (DARPA RSPACE, AFRL Fight Tonight), synthesis of OS kernel codes with proofs of their correctness (DARPA CRASH), synthesis of secure communication codes together with proofs (DARPA HACMS), planning tools for cyber missions (DARPA PlanX), synthesis of high-performance constraint solvers (DoD), and system design by model refinement (Sandia).

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

Selected Papers

  • Deductive Model Refinement
    Douglas R. Smith and Srinivas Nedunuri
    Proceedings of the 16th NASA Formal Methods Symposium (NFM 2024)
    Springer LNCS 14627, 2024, pages 147-165.

  • Model Refinement (Extended)
    Douglas R. Smith and Srinivas Nedunuri
    Technical Report, Kestrel Institute, October 2021.

  • Transformations for Generating Type Refinements
    Douglas R. Smith and Stephen J. Westfold
    in: Formal Methods: FM 2019 International Workshops,
    Springer LNCS 12233, pp 371-387.

  • Quantifier Elimination in Ordered Domains
    Douglas R. Smith
    Technical Report, Kestrel Institute, October 2019.

  • Synthesis of Concurrent Garbage Collectors
    Douglas R. Smith and Stephen J. Westfold
    Technical Report, Kestrel Institute, October 2015.

  • Toward the Synthesis of Constraint Solvers
    Douglas R. Smith and Stephen J. Westfold
    Technical Report, Kestrel Institute, November 2013.

  • Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms
    Srinivas Nedunuri, Douglas Smith, and William Cook
    in Proceedings of 18th Intl. Symp. on Formal Methods 2012,
    Springer LNCS 7436, Paris, France, August 2012.

  • Theory and Techniques for Synthesizing a Family of Graph Algorithms
    Srinivas Nedunuri, Douglas Smith, and William Cook
    in Proceedings of the First Workshop on Synthesis (SYNT 2012), Electronic Proceedings in Theoretical Computer Science 84, Berkeley, California, USA, 7-8 July 2012, 33-46.

  • Cost-Based Learning for Planning
    Srinivas Nedunuri, William Cook, and Douglas Smith
    in Proceedings of the 3rd Workshop on Planning and Learning (ICAPS), Freibourg, Germany, June 2011, 68-75.

  • A Class Of Greedy Algorithms and its Relation to Greedoids
    Srinivas Nedunuri, William Cook, and Douglas Smith
    in Proceedings of the Intl. Colloq. on Theoretical Aspects of Computing (ICTAC 2010), Springer LNCS 6255, Pages 352-366.

  • Synthesis of Greedy Algorithms Using Dominance Relations
    Srinivas Nedunuri, Douglas R. Smith, and William Cook
    in Proceedings of the Second NASA Formal Methods Symposium, Washington, DC, April 2010.

  • Formal Derivation of Concurrent Garbage Collectors
    Dusko Pavlovic, Peter Pepper, and Douglas R. Smith
    in Mathematics of Program Construction 2010 (MPC10), Springer LNCS 6120, July 2010, 353-376 (long version at https://arxiv.org/abs/1006.4342)

  • Tactical Synthesis of Efficient Global Search Algorithms
    Srinivas Nedunuri, William Cook and Douglas Smith
    in Proceedings of the NASA Formal Methods Symposium, NASA Ames Research Center, April 2009.

  • Synthesis of Satisfiability Solvers
    Douglas R. Smith and Stephen J. Westfold
    Technical Report, Kestrel Institute, April 2008.

  • Generating Programs plus Proofs by Refinement
    Douglas R. Smith
    in Verified Software: Theories, Tools, Experiments, Eds. Bertrand Meyer and Jim Woodcock,
    Springer-Verlag LNCS 4171, 2008,182-188.

  • Evolving Specification Engineering
    Dusko Pavlovic, Peter Pepper, and Doug Smith
    Proceedings of 12th International Conference on Algebraic Methodology And Software Technology (AMAST 2008), Eds. J. Meseguer and G. Rosu, Springer-Verlag LNCS 5140, July 2008,
    Urbana, IL, USA, 299-314.

  • Aspects as Invariants
    Douglas R. Smith
    Automatic Program Development: a Tribute to Robert Paige,
    Eds. O. Danvy, F.Henglein, H. Mairson, and A. Pettorosi, Springer-Verlag, 2008.

  • Transformation Automata and Policy Enforcement
    Douglas R. Smith
    Proceedings of the Sixth Workshop on Foundations of Aspect-Oriented Languages (FOAL 2007), ACM Press (ACM Digital Library), Vancouver, British Columbia, Canada, 13 March 2007.

  • Software Development by Refinement
    Douglas R. Smith and Cordell Green
    IEEE Intelligent Systems, November 2006, 75-77.

  • Toward the Industrial Scale Development of Custom Static Analyzers,
    J. Anton, E. Bush, A. Goldberg, K. Havelund, D. Smith, A. Venet,
    Proceedings of the NIST Static Analysis Summit, 2006.

  • Roadmap for Enhanced Languages and Methods to Aid Verification
    Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, and Aaron Stump,
    in Proceedings of Generative Programming and Component Engineering (GPCE-06), 2006.

  • Composition by Colimit and Formal Software Development
    Douglas R. Smith
    Algebra, Meaning, and Computation: A Festschrift in Honor of Prof. Joseph Goguen,
    Eds. Futatsugi, Jouannaud, and Meseguer, Springer-Verlag Festschrift series, 2006.

  • Comprehension by Derivation
    Douglas R. Smith
    Invited paper, Proceedings of the 13th International Workshop on Program Comprehension, IEEE Computer Society Press, Los Alamitos, CA, May 2005, pp 3-9.

  • A Generative Approach to Aspect-Oriented Programming
    Proceedings of the Third International Conference on Generative Programming and Component Engineering (GPCE 04), Vancouver, October, 2004, 39-54.

  • Derivation of Glue Code for Agent Interoperation
    M. Burstein, D. McDermott, D.R. Smith, and S.J. Westfold,
    invited paper in Journal of Autonomous Agents and Multi-Agent Systems 6, 2003, pp. 265-286.

  • Planware II: Synthesis of Schedulers for Complex Resource Systems
    Marcel Becker, Limei Gilham, Douglas R. Smith,
    submitted for publication, 2003.

  • Colimits for Concurrent Collectors
    Dusko Pavlovic, Peter Pepper, Douglas R. Smith.
    Festschrift for Zohar Manna, Springer-Verlag, LNCS, 2003, 568-597.

  • Software Development by Refinement
    Dusko Pavlovic and Douglas R. Smith,
    in UNU/IIST 10th Anniversary Colloquium, Formal Methods at the Crossroads: From Panaea to Foundational Support, Springer-Verlag LNCS 2757, 2003, 267-286.

  • Guarded Transitions in Evolving Specifications
    Dusko Pavlovic and Douglas R. Smith,
    in Proceedings of 9th International Conference on Algebraic Methodology And Software Technology (AMAST 2002), Eds. H. Kirchner and C. Ringeissen, Springer-Verlag LNCS 2422, 2002, 411-425.

  • Overcoming Ontology Mismatches in Transactions with Self-Describing Service Agents
    D. McDermott, M. Burstein, and D.R. Smith,
    in The Emerging Semantic Web, Eds I.Cruz, S. Decker, J. Euzenat, and D. McGuinness, IOS press, Amsterdam, 2002.

  • Composition and Refinement of Evolving Specifications
    Matthias Anlauff, Dusko Pavlovic, and Douglas R. Smith,
    invited paper in Proceedings of Workshop on Evolutionary Formal Software Development, July 2002, Copenhagen, Denmark.

  • The Roles of Witness-Finding in Software Synthesis
    Douglas R. Smith,
    Working Notes of the 2002 AAAI Symposium on Logic-Based Program Synthesis, AAAI Press, Menlo Park, March 2002.

  • Composition and Refinement of Behavioral Specifications
    Dusko Pavlovic and Douglas R. Smith,
    Proceedings of the Sixteenth International Conference on Automated Software Engineering, IEEE Computer Society Press, Coronado Island, CA, 2001, 157-165.

  • System Construction via Evolving Specifications
    Dusko Pavlovic and Douglas R. Smith,
    in Complex and Dynamic Systems Architectures (CDSA 2001), Brisbane, Australia, 2001.

  • Synthesis of Efficient Constraint Satisfaction Programs
    Westfold, S.J. and Smith, D.R.
    Knowledge Engineering Review 16(1), Special Issue on AI and OR, 2001, 69-84.

  • Derivation of Glue Code for Agent Interoperation
    M. Burstein, D. McDermott, D.R. Smith, and S.J. Westfold,
    Proceedings of the Agents 2000 Conference, Barcelona, Spain, May 2000 (revised version to appear in Journal of Autonomous Agents and Multi-Agent Systems, special issue on best papers of Agents 2000).

  • Formal Derivation of Agent Interoperation Code
    M. Burstein, D. McDermott, D.R. Smith, and S.J. Westfold,
    Formal Approaches to Agent-Based Systems Workshop, NASA Goddard Space Flight Center, MD, April 2000.

  • Designware: Software Development by Refinement
    Douglas R. Smith,
    invited paper in Proceedings of the Eighth International Conference on Category Theory and Computer Science (CTCS'98), Edinburgh, September, 1999.

  • Mechanizing the Development of Software (PS)
    Douglas R. Smith,
    in Calculational System Design, Proceedings of the NATO Advanced Study Institute, Eds. M. Broy and R. Steinbrueggen, IOS Press, Amsterdam, 1999, 251-292.

  • Planware – Domain-Specific Synthesis of High-Performance Schedulers (PS)
    Lee Blaine, Limei Gilham, Junbo Liu, Douglas R. Smith, and Stephen Westfold,
    in Proceedings of the Thirteenth Automated Software Engineering Conference, IEEE Computer Society Press, Los Alamitos, California, October, 1998, 270-280.

  • A High-level Derivation of Global Search Algorithms (with Constraint Propagation) (PS)
    Peter Pepper and Douglas R. Smith,
    Science of Computer Programming, Special Issue on FMTA (Formal Methods: Theory and Applications), Vol 28 (1996), 247-271.

  • Synthesis of Planning and Scheduling Software (PS)
    Douglas R. Smith, Eduardo A. Parra, and Stephen J. Westfold,
    Advanced Planning Technology, Ed. A. Tate, AAAI Press, Menlo Park, California, 1996, 226-234.

  • Toward a Classification Approach to Design (PS)
    Douglas R. Smith,
    Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology, AMAST'96, LNCS, Springer Verlag, 1996, 62-84.

  • Synthesis of Schedulers for Planned Shutdowns of Power Plants (PS)
    Carla P. Gomes, Douglas R. Smith, and Stephen J. Westfold,
    Proceedings of the Eleventh Knowledge-Based Software Engineering Conference, IEEE Computer Society Press, Los Alamitos, California, September 1996, 12-20.

  • ITAS: A Portable Interactive Transportation Scheduling Tool Using a Search Engine Generated from Formal Specifications (PS)
    Mark B. Burstein and Douglas R. Smith,
    Proceedings of the Third International Conference on Artificial Intelligence Planning Systems (AIPS-96), Edinburgh, U.K., May 1996, 35-44.

  • Toward Practical Applications of Software Synthesis (PS)
    Douglas R. Smith and Cordell Green,
    Proceedings of FMSP'96, The First Workshop on Formal Methods in Software Practice. San Diego, CA, January 1996, 31–39.

  • Synthesis of Constraint Algorithms
    Smith, D.R. and Westfold, S.J.,
    in Principles and Practice of Constraint Programming, V. Saraswat and P. Van Hentenryck Eds., MIT Press, 1995, 173-182.

  • Synthesis of High-Performance Transportation Schedulers (PS)
    Douglas R. Smith, Eduardo A. Parra and Stephen J. Westfold,
    February 1995, Kestrel Institute Technical Report KES.U.95.1.

  • Transformational Approach to Transportation Scheduling (PS)
    Douglas R. Smith and Eduardo A. Parra,
    Proceedings of the 8th Knowledge-Based Software Engineering Conference, (Best Paper Award), September 1993, IEEE Computer Society Press, 60-68. Figure 1 (included in PDF version), Figure 2 (included in PDF version).

  • Toward the Synthesis of Constraint Propagation Algorithms
    Smith, D.R.,
    in Logic Program Synthesis and Transformation, Y. Deville (Ed.), Workshops in Computing Series, Springer-Verlag, 1994, 1-9.

  • Constructing Specification Morphisms (PS)
    Douglas R. Smith,
    Journal of Symbolic Computation, Special Issue on Automatic Programming, Vol 16, No 5-6, 1993, pp. 571-606.

  • Automating the Design of Algorithms
    Smith, D.R.,
    in Formal Program Development, IFIP TC2/WG2.1 State-of-the-Art Report, Eds. B. Moeller, H. Partsch, S. Schumann, LNCS 755, Springer-Verlag, 1993, 324-354.

  • Derivation of Parallel Sorting Algorithms (PS)
    Douglas R. Smith,
    Parallel Algorithm Derivation and Program Transformation, Eds. R. Paige, J. Reif, and R. Wachter, Kluwer Academic Publishers, 1993, 55-69.

  • Track Assignment in an Air Traffic Control System: A Rational Reconstruction of System Design
    Douglas R. Smith,
    July 1991 Kestrel Institute Technical Report KES.U.91.9, 106pp.

  • Structure and Design of Problem Reduction Generators (PS)
    Douglas R. Smith,
    Constructing Programs from Specifications, B. Moeller, Ed., North Holland, 1991.

  • KIDS: A Knowledge-Based Software Development System (PS)
    Douglas R. Smith,
    Automating Software Design, Eds. M. Lowry and R. McCartney, MIT Press, 1991, 483-514.

  • KIDS: A Semi-Automatic Program Development System (PS)
    Douglas R. Smith,
    IEEE Transactions on Software Engineering — Special Issue on Formal Methods, Vol. 16, No. 9, September 1990.

  • Algorithm Theories and Design Tactics
    Douglas R. Smith and Michael R. Lowry,
    Science of Computer Programming 14(2-3), Special Issue on the Mathematics of Program Construction, October 1990, 305-321. (also in Proceedings of the International Conference on the Mathematics of Program Construction, LNCS 375, Springer-Verlag, 1989.)

  • Automating the Development of Software
    Smith, D.R.,
    in Proceedings of the Fifth Annual Knowledge-Based Software Assistant Conference, Liverpool, New York, September, 1990, 13-27.

  • Knowledge-Based Software Development Tools
    Smith, D.R. and Pressburger, T.T.,
    in Software Engineering Environments, P. Brereton, Ed., Ellis Horwood Ltd., Chichester, 79-103, 1988.

  • Applications of a Strategy for Designing Divide-and-Conquer Algorithms
    Smith, D.R.,
    Science of Computer Programming Volume 8, Issue 3 (1987), 213-229.

  • Reformulation: An Approach to Efficient Constraint Validation
    Qian, X.L., and Smith, D.R.,
    in Proceedings of the Thirteenth VLDB Conference, Brighton, England, 1987, 417-425.

  • On the Design of Generate-and-Test Algorithms: Subspace Generators
    Smith, D.R.,
    in Program Specification and Transformation, L.G.L.T. Meertens (Editor), North-Holland Publishing Co., Amsterdam, 1987, 207-220.

  • Top-Down Synthesis of Divide-and-Conquer Algorithms
    Smith, D.R.,
    Artificial Intelligence Volume 27, Issue 1 (1985), 43-96 (reprinted in Readings in Artificial Intelligence and Software Engineering, Eds. C. Rich and R. Waters, Morgan Kaufmann Pub. Co., Los Altos, CA, 1986, 35-61).

  • Reasoning by Cases and the Formation of Conditional Programs
    Smith, D.R.,
    in Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, CA, August 1985, 215-218.

  • The Design of Divide and Conquer Algorithms
    Smith, D.R.,
    Science of Computer Programming Volume 5, Issue 1 (1985), 37-58.

  • The Synthesis of LISP Programs from Examples: A Survey
    Smith, D.R.,
    in Automatic Program Construction Techniques, Eds. A.W. Biermann, G. Guiho, and Y. Kodratoff, MacMillan Publishing Company, New York, 1984, 307-324.

  • Random Trees and the Analysis of Branch and Bound Procedures
    Smith, D.R.,
    Journal of the ACM, Volume 31 Issue 1 (January 1984), 163-188.

  • A Problem Reduction Approach to Program Synthesis
    Smith, D.R.,
    in Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany, August 1983, 32-36.

  • Derived Preconditions and Their Use in Program Synthesis
    Smith, D.R.,
    in Sixth Conference on Automated Deduction, Ed. D.W. Loveland, Lecture Notes in Computer Science 138, Springer-Verlag, New York, 1982, 172-193.

  • A Design for an Automatic Programming System
    Smith, D.R.,
    in Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, BC, Canada, August 1981, 1027-1029.

  • A Survey of the Synthesis of LISP Programs from Examples
    Smith, D.R.,
    in Proceedings of the International Workshop on Program Construction, Bonas, France, September 1980.

  • A Production Rule Mechanism for Generating LISP Code
    Biermann, A.W. and Smith, D.R.,
    IEEE Transactions on Systems, Man, and Cybernetics (SMC-9), Volume 9 Issue 5 (May 1979), 260-276.

  • Hierarchical Synthesis of LISP Scanning Programs
    Biermann, A.W. and Smith, D.R.,
    Information Processing 77, Ed. B. Gilchrist, North Holland Publishing Company, Amsterdam, 1977, 41-45.