Development of a Constraint-Based Airlift Scheduler by Program Synthesis from Formal Specifications

DOI 10.1109/ase.1999.802313 dblp

Abstract

We describe the formal specification and automated synthesis of a strategic airlift scheduler for the Air Mobility Command of the US Air Force. The program synthesis system, the Kestrel Interactive Development System, composes a formal domain theory with a formal description of a class of algorithms (global search with constraint propagation) to produce provably correct and highly efficient code that outperforms more conventional approaches to this scheduling problem.

BibTeX

@inproceedings{Emerson-Burstein:ASE99,
  author    = {Thomas Emerson and
               Mark H. Burstein},
  title     = {Development of a {Constraint-Based} Airlift Scheduler by Program Synthesis from Formal Specifications},
  booktitle = {ASE},
  pages     = {267--270},
  publisher = {{IEEE} Computer Society},
  year      = {1999},
}

Development of a Constraint-Based Airlift Scheduler by Program Synthesis from Formal Specifications

Abstract

Related papers