Development of a constraint-based airlift scheduler by program synthesis from formal specifications

20 January 2003

proceedings article
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 267-270
https://doi.org/10.1109/ase.1999.802313

Abstract

We describe the formal specification and automated synthesis of a strategic airlift scheduler for the Air Mobility Command of the U. S. 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.

Keywords

This publication has 3 references indexed in Scilit:

Synthesis of schedulers for planned shutdowns of power plants
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
Scheduling an Asynchronously Shared Resource
Lecture Notes in Computer Science, 1996
KIDS: a semiautomatic program development system
IEEE Transactions on Software Engineering, 1990