[Kestrel circling]

Home : Publications
 

Selected Publications
Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel
  • 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-376l
    (long version at http://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.
  • An Examination of Criticality-Sensitive Approaches to Coordination. Szekely, P., Neches, R., Maheswaran, R., Rogers, C., Sanchez, R., Becker, M., Fitzpatrick, S., Gati, G., Hanak, D., Karsai, G., and Van Buskirk, C. The Twenty-First National Conference on Artificial Intelligence (AAAI 2006), July 16-20, 2006, Boston, MA
  • CSC: Criticality-Sensitive Coordination. Szekely, P., Becker, M., Fitzpatrick, S., Gati, G., Hanak, D., Jin, J., Karsai, G., Maheswaran, R., Neches, R., Rogers, C., Sanchez, R., and Van Buskirk, C. Demonstration at Fifth International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), May 8-12, 2006, Hakodate, Japan.
  • Aspects as Invariants. Douglas R. Smith. In Automatic Program Development: a Tribute to Robert Paige, Eds. O. Danvy, F. Henglein, H. Mairson, and A. Pettorosi, Springer-Verlag, 2006.
  • Composition by Colimit and Formal Software Development. Douglas R. Smith. In Algebra, Meaning, and Computation: A Festschrift in Honor of Prof. Joseph Goguen, Eds. Futatsugi, Jouannaud, and Meseguer, Springer-Verlag LNCS 4060, pp. 317-332, 2006.
  • Deriving Secure Network Protocols for Enterprise Services Architectures. M. Anlauff, D. Pavlovic, and A. Suenbuel. ICC06, June 2006.
  • Accord Language Manual. Version 4.1.4. James McDonald and Douglas R. Smith. Kestrel Institute Technical Report KES.U.05.06, December 2005.
  • Accord Tutorial. Matthias Anlauff, James McDonald, and Douglas R. Smith. Kestrel Institute Technical Report KES U.05.05, December 2005.
  • FORGES: Formal Synthesis of Generators for Embedded Systems. Lindsay Errington. Kestrel Institute Technical Report KES.U.05.04, May 2005.
  • 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.
  • Plan Execution and Coordination. Pedro Szekely, Robert Neches, Marcel Becker, Stephen Fitzpatrick, Chris van Buskirk, Doug Fisher, and Gabor Karsai. Plan Execution: A Reality Check, Worshop at the Fifteenth International Conference on Automated Planning & Scheduling (ICAPS 2005), 5-10 June 2005, Monterey, CA.
  • Checking Access to Protected Members in the Java Virtual Machine. Alessandro Coglio. Journal of Object Technology. October 2005. Supersedes Kestrel Institute Technical Report KES.U.04.03 of February 2004.
  • Formal Techniques for Java-Like Programs (FTfJP. Alessandro Coglio with Marieke Huisman, Joseph Kiniry, Peter Muller, and Erik Poll. Object-Oriented Technology. ECOOP 2004 Workshop Reader, number 3344 in Lecture Notes in Computer Science (LNCS), pages 76-83, Springer-Verlag. January 2005.
  • Testing Semantics of State Machines and Process Logics. Dusko Pavlovic. Kestrel Institute Technical Report KES.U.05.03, October 2005.
  • A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets. Alessandro Coglio and Cordell Green. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments, October 2005.
  • The Dimension of the Vector Space Spanned by Sets of Radio-Interferometric Measurements. Lambert Meertens. Kestrel Institute Technical Report KES.U.05.02, July 2005.
  • An Encapsulated Authentication Logic for Reasoning About Key Distribution Protocols. Iliano Cervesato, Catherine Meadows, and Dusko Pavlovic. In, Proceedings of CSFW 2005, June 2005, Aix-en-Provence, France, Joshua Guttman (Ed.)
  • Deriving Secrecy (Encapsulating Authenticity) in Key Establishment Protocols. Dusko Pavlovic. Kestrel Institute Technical Report KES.U.05.01, May 2005.
  • Designing Constraint Maintainers for User Interaction. Lambert Meertens. Invited talk. In, Proc. Third Workshop on Programmable Structured Documents. Yokohama, Japan, January 26-28, 2005. PSD Laboratory, University of Tokyo, 2005.
  • A Generative Approach to Aspect-Oriented Programming. Douglas R. Smith. Proceedings of the Third International Conference on Generative Programming and Component Engineering (GPCE 04), Vancouver, October 2004, 39-54.
  • Deploying Localization Services in Wireless Sensor Networks. M. Anlauff and A. Suenbuel. International Workshop on Wireless AdHoc Networking, to be held in conjunction with The 24th IEEE International Conference on Distributed Computing Systems (ICDCS-2004), Tokyo, Japan, March 2004
  • Calculating the Sieve of Eratosthenes. Lambert Meertens. Journal of Functional Programming, 14(6):759-763, 2004
  • A Semantical Approach to Equilibria, Adaptation and Evolution. Dusko Pavlovic. Kestrel Institute Technical Report KES.U.04.06, December 2004.
  • Simple Verification Technique for Complex Java Bytecode Subroutines. Alessandro Coglio. Concurrency and Computation: Practice and Experience16(7):647-670, June 2004. Kestrel Institute Technical Report KES.U.04.05, June 2004. This paper supersedes Kestrel Institute Technical Report KES.U.02.04 of December 2001, revised May 2002. Short version, appeared in 4th ECOOP Workshop on Formal Techniques for Java-like Programs, June 2002.
  • The Distributed Construction of a Global Coordinate System in a Network of Static Computational Nodes from Inter-Node Distances. Lambert Meertens and Stephen Fitzpatrick. Kestrel Institute Technical Report KES.U.04.04, March 2004.
  • Checking Access to Protected Members in the Java Virtual Machine. Alessandro Coglio. Kestrel Institute Technical Report KES.U.04.03, February 2004.
  • Deriving, Attacking and Defending the GDOI Protocol. Cathy Meadows and Dusko Pavlovic. Kestrel Institute Technical Report KES.U.04.02, January 2004.
  • Deriving Authenticity and Integrity as Order of Actions. Dusko Pavlovic and Cathy Meadows. Kestrel Institute Technical Report KES.U.04.01, January 2004.
  • Deriving Evolutionary Software Systems for Distributed, Realtime Embedded Networks. M. Anlauff and A. Suenbuel. Integrated Design and Process Technology IDPT 2003, Austin, TX. December 2003.
  • Evolving Specifications: Deriving Component Based Applications. M. Anlauff and A. Suenbuel. 29th Euromicro Conference (EUROMICTRO 2003), Antalya, Turkey, IEEE Computer Society, September 2003.
  • Distributed Coordination through Anarchic Optimization. Abstract. Stephen Fitzpatrick and Lambert Meertens. In, Distributed Sensor Networks: A Multiagent Perspective, pp. 257-295; Victor Lesser, Charles L. Ortiz, Jr., & Milind Tambe (Eds.); Kluwer Academic Publishers, 2003; ISBN: 1-4020-7499-9. 
  • Component Based Software Engineering. Asuman Sunbul. In, Euromicro 2003 - Proceedings of the 29th Euromicro Conference. Belek-Antalya, Turkey, September 1-6, 2003. IEEE Computer Society, 2003.
  • Correct by Construction Components, Or: Would Nasreddin Use Components. Asuman Sunbul. In, Euromicro 2003 - Proceedings of the 29th Euromicro Conference. Belek-Antalya, Turkey, September 1-6, 2003. IEEE Computer Society, 2003. 
  • Colimits for Concurrent Collectors. Dusko Pavlovic, Peter Pepper, Douglas R. Smith. Festschrift for Zohar Manna, Springer-Verlag, LNCS, 2003. 
  • Toward Automatic Generation of Provably Correct Java Card Applets. Alessandro Coglio. 5th ECOOP Workshop on Formal Techniques for Java-like Programs,  July 2003.
  • 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.
  • Evolving Specifications. Dusko Pavlovic and Douglas R. Smith. In preparation, 2003.
  • Colimits for Concurrent Collectors. Dusko Pavlovic, Peter Pepper, and Douglas R. Smith. Submitted for publication. Kestrel Institute Technical Report KES.U.03.05, 2003.
  • 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, 2003.
  • Planware II: Synthesis of Schedulers for Complex Resource Systems. Marcel Becker, Limei Gilham, and Douglas R. Smith. Submitted for publication. Kestrel Institute Technical Report KES.U.03.04, May 2003.
  • Testing and Continuous State Systems.  Dusko Pavlovic. Kestrel Institute Technical Report KES.U.03.03, May 2003.
  • Code Generation for High-Assurance Java Card Applets. Alessandro Coglio. 3rd NSA Conference on High Confidence Software and Systems, pp. 85-93, April 2003.
  • Improving the Official Specification of Java Bytecode Verification. Alessandro Coglio. Concurrency and Computation: Practice and Experience, 15(2):155-179, February 2003. Preliminary version appeared in, 3rd ECOOP Workshop on Formal Techniques for Java Programs, June 2001. 
  • On Specification Carrying Software, Its Refinement and Composition. M. Anlauff and A. Suenbuel. Integrated Process and Design Technology IDPT 2002, Pasadena, CA, June 2002.
  • Experiments on Dense Graphs with a Stochastic, Peer-to-Peer Colorer. Stephen Fitzpatrick and Lambert Meertens. In, Probabilistic Approaches in Search. Workshop at Eighteenth National Conference on Artificial Intelligence (AAAI 2002), 28 July 2002, Edmonton, Alberta, Canada. Carla Gomes & Toby Walsh (Ed.), AAAI Press, Technical Report WS-02-14, ISBN 1-57735-167-3, pp. 24-28 
  • Asynchronous Execution and Communication Latency in Distributed Constraint Optimization. Lambert Meertens and Stephen Fitzpatrick. In, Proceedings of The Third International Workshop on Distributed Constraint Reasoning, First International Joint Conference on Autonomous Agents & Multiagent Systems (AAMAS 2002), 16 July 2002, Bologna, Italy, Makoto Yokoo (Ed.), pp. 80-85. 
  • Scalable, Anytime Constraint Optimization through Iterated, Peer-to-Peer Interaction in Sparsely-Connected Networks. Stephen Fitzpatrick and Lambert Meertens. In,  Proceedings of The Sixth Biennial World Conference on Integrated Design & Process Technology (IDPT 2002), 23-28 June 2002, Pasadena, California, U.S.A. H. Ehrig, B.J. Kramer & A. Ertas (Ed.), Society for Design and Process Science, ISSN No. 1090-9389
  • Towards the Formal Development of Embedded Systems. Douglas R. Smith. Kestrel Institute Technical Report KES.U.02.05, September 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.
  • Derivation of the JFK Protocol. Anupam Datta, John Mitchell, and Dusko Pavlovic. Kestrel Institute Technical Report KES.U.02.03, July 2002.
  • Authentication for Mobile IPv6. A. Datta, J.C. Mitchell, F. Muller, and D. Pavlovic. Kestrel Institute Technical Report KES.U.02.02, March 2002.
  • An Approach to the Generation of High-Assurance Java Card Applets. Alessandro Coglio. 2nd NSA Conference on High Confidence Software and Systems, pp. 69-77, March 2002.
  • 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.
  • Architectural Design of Evolutionary Software Systems. Asuman Suenbuel. In, Theory and Application of Abstract State Machines, A. Blass , E. Börger, Y. Gurevich, Eds. Dagstuhl Seminar, March 2002
  • Specifying Third Generation Middleware Techniques for NEST Applications. Asuman Suenbuel. In, Special Issue of the Journal of Design & Process Science on Component-Based System Development. 
  • Towards Component Based Systems: Refining Connectors. M. Anlauff and A. Suenbuel. In, REFINE 02: The BCS FACS Refinement Workshop - Electronic Notes in Theoretical Computer Science, 70(3), John Derrick et al., Eds., Elsevier, July 2002.
  • Specifying Components for NEST Applications. Asuman Suenbuel. In, Integrated Design & Process Science, Herbert Weber and Hartmut Ehrig, Eds. June, Pasadena, 2002.
  • 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. Kestrel Institute Technical Report KES.U.02.01, February 2002. 
  • Software Productivity through Automation and Design Knowledge. Cordell Green, Dusko Pavlovic, and Douglas R. Smith. Software Design and Productivity Workshop, Nashville TN, Dec 2001. 
  • Type Safety in the JVM: Some Problems in Java 2 SDK 1.2 and Proposed Solutions. Alessandro Coglio and Allen Goldberg. Concurrency and Computation: Practice and Experience, 13(13):1153-1171, November 2001. This paper supersedes Kestrel Institute Technical Report KES.U.00.3 of April 2000. Short version appeared in 2nd ECOOP Workshop on Formal Techniques for Java Programs, June 2000.
  • Evolutionary Development of Business Process Centered Architectures Using Component Technologies. A. Suenbuel, H. Weber and J. Padberg. Transactions of the SDPS, Journal of Integrated Design & Process Science, Vol 5, No. 3, September 2001, pp.13-24. Kestrel Institute Technical Report KES.U.01.11, September 2001.
  • Architectural Design of Evolutionary Software Systems in Continuous Software Engineering. Asuman Suenbuel. Stuttgart, DAV, 2001.
  • An Experimental Assessment of a Stochastic, Anytime, Decentralized, Soft Colourer for Sparse Graphs. Stephen Fitzpatrick and Lambert Meertens. Stochastic Algorithms: Foundations and Applications, Proceedings SAGA 2001, K. Steinhoefel, Ed. Berlin, Springer-Verlag LNCS 2264, 2001, pp. 49-64. Kestrel Institute Technical Report KES.U.01.10, December 2001.
  • Peer-to-Peer Coordination of Autonomous Sensors in High-Latency Networks using Distributed Scheduling and Data Fusion. Lambert Meertens and Stephen Fitzpatrick. Kestrel Institute Technical Report KES.U.01.09, December 2001.
  • Overcoming Ontology Mismatches in Transactions with Self-Describing Service Agents. D. McDermott, M. Burstein, and D.R. Smith. In, The Emerging Semantic Web. Eds Isabel Cruz, Stefan Decker, Jérôme Euzenat, and Deborah McGuinness, IOS press, Amsterdam, 2002. Kestrel Institute Technical Report KES.U.01.8, July 2001.
  • Synthesis of Efficient Constraint Satisfaction Programs. S.J. Westfold and D.R. Smith. Knowledge Engineering Reviews, Special Issue on AI and OR, 2001. Kestrel Institute Technical Report KES.U.01.7, July 2001.
  • Composition and Refinement of Behavioral Specifications. Dusko Pavlovic and Douglas R. Smith. Kestrel Institute Technical Report KES.U.01.6, July 2001.
  • Soft, Real-Time, Distributed Graph Coloring using Decentralized, Synchronous, Stochastic, Iterative-Repair, Anytime Algorithms: A Framework. Stephen Fitzpatrick and Lambert Meertens. Kestrel Institute Technical Report KES.U.01.5., May 2001.
  • Network Vulnerability Analysis - A Formal Approach. James McDonald and John Anton. Kestrel Institute Technical Report KES.U.01.4., March 2001.
  • SPECWARE - Producing Software Correct by Construction. James McDonald and John Anton. Kestrel Institute Technical Report KES.U.01.3., March 2001.
  • Categories of processes enriched in final coalgebras. Sava Krstic, John Launchbury, and Dusko Pavlovic. Proceedings of FoSSaCS 2001, Furio Honsell, (Ed.). Berlin, Springer-Verlag LNCS 2030, 2001, pp. 303-317. Kestrel Institute Technical Report KES.U.01.2, March 2001.
  • Process Fusion. Dusko Pavlovic. Kestrel Institute Technical Report KES.U.01.1, March 2001.
  • EPOXI. Dusko Pavlovic. Kestrel Institute Technical Report KES.U.00.9, January 2001.
  • Experiments Suggest High Level Formal Models and Automated Code Synthesis Significantly Increase Dependability. Cordell Green and Stephen Westfold. Kestrel Institute Technical Report KES.U.00.8, January 2001.
  • A Formal Specification of Java Class Loading. Z. Qian, A. Goldberg, and A. Coglio. Proc. 15th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00). ACM SIGPLAN Notices, v. 35(10), October 2000, pp. 325-336. Long version appeared as Kestrel Institute Technical Report KES.U.00.10, April 2000, revised July 2000.
  • Standard Fixpoint Iteration for Java Bytecode Verification. Zhenyu Qian. ACM Transactions on Programming Languages and Systems, Vol. 22(4), July 2000, pp. 638-672. 
  • Derivation of Glue Code for Agent Interoperation. M. Burstein, D. McDermott, D. R. Smith, and S.J. Westfold. Journal of Autonomous Agents and Multi-Agent Systems, 2000, (earlier version in Proceedings of the Agents 2000 Conference, Barcelona, Spain, May 2000). Kestrel Institute Technical Report KES.U.00.5, May 2000.
  • Formal Derivation of Agent Interoperation Code. M. Burstein, D. McDermott, D.R. Smith, and S.J. Westfold. Proceedings of the Formal Approaches to Agent-Based Systems Workshop, NASA Goddard Space Flight Center, MD, April 2000. Kestrel Institute Technical Report KES.U.00.4, April 2000.
  • Programming and Coalgebra of Processes. Sava Kristic, John Launchbury and Dusko Pavlovic. Kestrel Institute Technical Report KES.U.00.2, May 2000.
  • Protocol Composition and Correctness (Extended Abstract). Nancy Durgin, John Mitchell, and Dusko Pavlovic. Kestrel Institute Technical Report KES.U.00.1, January 2000.
  • Development of a Constraint-Based Airlift Scheduler by Program Synthesis from Formal Specifications. Thomas Emerson and Mark H. Burstein. Proceedings of the 14th IEEE International Conference on Automated Software Engineering. Orlando, FL, September 1999. Kestrel Institute Technical Report KES.U.99.9, September 1999.  
  • Designware: Software Development by Refinement. D. R. Smith. Proceedings of the Eighth International Conference on Category Theory and Computer Science Invited Paper, Edinburgh, September 1999. Kestrel Institute Technical Report KES.U.99.8, September 1999.
  • The Continuum as a Final Coalgebra. Dusko Pavlovic and Vaughan Pratt. Theoretical Computer Science. Kestrel Institute Technical Report KES.U.99.6, 1999.
  • On Coalgebra of Real Numbers. Dusko Pavlovic and Vaughan Pratt. Electronic Notes in Theoretical Computer Science, V 19, 1999. Kestrel Institute Technical Report KES.U.99.5, 1999.
  • Towards Semantics of Self-Adaptive Software. Dusko Pavlovic. Proceedings of the Workshop on Self-Adaptive Software, P. Robertson (Ed.), Springer Lecture Notes in Computer Science 1936, Berlin, 2001, pp. 50-64. Kestrel Institute Technical Report KES.U.99.4, 1999.
  • Semantics of First Order Parametric Specifications. Dusko Pavlovic. Formal Methods '99, J.M. Wing, J. Woodcock, and J. Davies (Eds.), Springer-Verlag LNCS 1708, Berlin, 1999, pp. 155-172. Kestrel Institute Technical Report KES.U.99.3, 1999.
  • Generic Programming -- An Introduction. Roland Backhouse, Patrik Jansson, Johan Jeuring, Lambert Meertens. Advanced Functional Programming (S. Doaitse Swierstra, editor), Springer-Verlag LNCS 1608, Berlin, 1999, pp. 28-115. Kestrel Institute Technical Report KES.U.99.2, 1999.
  • Mechanizing the Development of Software. D. R. Smith. Calculational System Design, Proceedings of the International Summer School Marktoberdorf, M. Broy (Ed.), NATO ASI Series, IOS Press, Amsterdam, 1999. Kestrel Institute Technical Report KES.U.99.1, March 1999.
  • A Formal Specification of a Large Subset of Java(tm) Virtual Machine Instructions for Objects, Methods and Subroutines. Zhenyu Qian. Formal Syntax and Semantics of Java(TM). Alves-Foss, J. (Ed.), Springer Verlag LNCS, 1999. 
  • Modularization and Interpolation. Grigori Mints. Kestrel Institute Technical Report KES.U.98.8, December 1998.
  • Axiomatization of a Skolem Function in Intuitionistic Logic. Grigori Mints. Kestrel Institute Technical Report KES.U.98.7, October 1998.
  • Planware -- Domain-Specific Synthesis of High-Performance Schedulers. Lee Blaine, Li-Mei Gilham, Junbo Liu, Douglas R. Smith, and Stephen Westfold. Proceedings of the Thirteenth Automated Software Engineering Conference, IEEE Computer Society Press, Los Alamitos, CA, October 1998, pp. 270-280. Kestrel Institute Technical Report KES.U.98.6, September 1998.
  • Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. Alessandro Coglio, Allen Goldberg, and Zhenyu Qian. Proceedings of the OOPSLA '98 Workshop on the Formal Underpinnings of Java, Vancouver, B.C., October 1998. 
  • Complexity and Correctness of Function Definitions. Grigori Mints. Kestrel Institute Technical Report KES.U.98.3, July 1998.
  • Domains of Functions. Grigori Mints. Kestrel Institute Technical Report KES.U.98.2, July 1998.
  • Nested Datatypes. Richard Bird, Lambert Meertens. Mathematics of Program Construction, MPC'98 (Johan Jeuring, editor), LNCS 1422, pp. 52-67, June 1998.
  • Calculus in Coinductive Form. D. Pavlovic and M.H. Escardo. Proceedings of LICS '98, Indianapolis, ID IEEE Computer Society Press, June 1998. Kestrel Institute Technical Report KES.U.98.1.
  • Guarded Induction on Final Coalgebras. Dusko Pavlovic. CMCS '98: First Workshop on Coalgebraic Methods in Computer Science, Lisbon, Portugal, March 1998.
  • A Specification of Java Loading and Bytecode Verification. Allen Goldberg. Proceedings, 5th ACM Conference on Computer and Communications Security, San Francisco, October 1998.
  • Refinement of Parameterized Algebraic Specifications. . Yellamraju V. Srinivas. IFIP TC2 Working Conference on Algorithmic Languages and Calculi, Le Bischenberg, France. Chapman & Hall, February, 1997.
  • The Architecture of Specware, a Formal Software Development System. Yellamraju V. Srinivas and James L. McDonald. Kestrel Institute Technical Report KES.U.96.7, August 1996.
  • Synthesis of Schedulers for Planned Shutdowns of Power Plants. 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.
  • State Transitions Modeled as Refinements. Philipp W. Kutter. Kestrel Institute Technical Report KES.U.96.6, July 1996.
  • Toward Practical Applications of Software Synthesis. 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.
  • Montages: Unified Static and Dynamic Semantics of Programming Languages. Philipp W. Kutter and Alfonso Pierantonio. Universita de L'Aquila, Technical Report 118/July 96.
  • Toward a Classification Approach to Design. Douglas R. Smith. Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology, AMAST'96, LNCS 1101, Springer Verlag, 1996.
  • Synthesis of Planning and Scheduling Software. Douglas R. Smith, Eduardo A. Parra, and Stephen J. Westfold. Advanced Planning Technology, Ed. A. Tate, AAAI Press, Menlo Park, California, 1996.
  • ITAS: A Portable Interactive Transportation Scheduling Tool Using a Search Engine Generated from Formal Specifications. Mark B. Burstein and Douglas R. Smith. Proceedings of the Third International Conference on Artificial Intelligence Planning Systems (AIPS-96), Edinburgh, May 1996.
  • A High-level Derivation of Global Search Algorithms (with Constraint Propagation). Peter Pepper and Douglas R. Smith. Science of Computer Programming, Special Issue on FMTA (Formal Methods: Theory and Applications), 1996.
  • Specification and Development of Parallel Algorithms with the Proteus System. Goldberg, A., Mills, P., Nyland, L.,Prins, P., Reif, J., Riely, J., DIMACS Workshop on Specification of Parallel Algorithms, G. Blelloch, M. Chandy, and S. Jagannathan, Ed. AMS, 1995, pp 383-399.
  • A Refinement Approach to Visualization. Allen Goldberg, Rafael Furst, Cordell Green, Kestrel Institute Technical Report KES.U.95.2, August 1995.
  • Synthesis of High-Performance Transportation Schedulers. Douglas R. Smith, Eduardo A. Parra and Stephen J. Westfold, February 1995, Kestrel Institute Technical Report KES.U.95.1.
  • Specware®: Formal Support for Composing Software. Y. V. Srinivas and Richard Jullig, Proceedings of the Conference on Mathematics of Program Construction, Kloster Irsee, Germany, July 1995. Kestrel Institute Technical Report KES.U.94.5.
  • Applications of feasible path analysis to program testing. Allen Goldberg, T. C. Wang, and D. Zimmerman. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), T. Ostrand, editor, Seattle, WA, August 17-19, 1994.
  • KITP-93: An automated Inference System for Program Analysis. Wang T.C. and Goldberg, Proceedings of 12th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence (ed. A. Bundy), vol. 814, pp. 831-836 (1994).
  • Augmenting Algebraic Specifications with Structured Sorts and Structural Subsorting. Yellamraju V. Srinivas, January 1994, Kestrel Institute Technical Report KES.U.94.1.
  • Transformational Approach to Transportation Scheduling. Douglas R. Smith and Eduardo A. Parra. Proceedings of the 8th Knowledge-Based Software Engineering Conference, Chicago, IL., Sept. 20-23, 1993, IEEE Computer Society Press, p60-68, (Best Paper Award). Kestrel Institute Technical Report KES.U.93.3, 8pp.
  • Diagrams for Software Synthesis. Richard Jullig and Yellamraju V. Srinivas, Proceedings of the 8th Knowledge-Based Software Engineering Conference, Sept. 20-23, 1993, Chicago, IL, IEEE Computer Society Press, p10-19. Kestrel Institute Technical Report KES.U.93.2, 9pp.
  • Referential Opacity in Non-Deterministic Data Refinement . Qian,X., Goldberg, A. ACM Letters on Programming Languages and Systems no. 1-4 pp 233-41, March 1993.
  • Constructing Specification Morphisms. Douglas R. Smith. Journal of Symbolic Computation, Special Issue on Automatic Programming, Vol 16, No 5-6, 1993, pp. 571-606. Kestrel Institute Technical Report KES.U.92.1, 35pp.
  • Derivation of Parallel Sorting Algorithms. Douglas R. Smith. Parallel Algorithm Derivation and Program Transformation, Eds. R. Paige, J. Reif, and R. Wachter, Kluwer Academic Publishers, 1993, 55-69. Kestrel Institute Technical Report KES.U.91.12, 14pp.
  • Structure and Design of Problem Reduction Generators. Douglas R. Smith. Constructing Programs from Specifications. B. Moller, Ed., North Holland, 1991. Kestrel Institute Technical Report KES.U.91.4, 33pp.
  • KIDS: A Knowledge-Based Software Development System. Douglas R. Smith. Automating Software Design, Eds. M. Lowry and R. McCartney, MIT Press, 1991, 483-514.
  • KIDS: A Semi-Automatic Program Development System. Douglas R. Smith. IEEE Transactions on Software Engineering --- Special Issue on Formal Methods, Vol. 16, No. 9., September 1990.
  • Report on a Knowledge-Based Software Assistant. Cordell Green, David Luckham, Robert Balzer, Thomas Cheatham, and Charles Rich. Kestrel Institute Technical Report KES.U.83.2, July 1983.

Archival List of Technical Reports (pre-1994)

 

 

- Back to Top -


- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -