Elan: The Event Logic Assistant

Award Information
Agency:
Department of Defense
Branch
Air Force
Amount:
$749,860.00
Award Year:
2009
Program:
STTR
Phase:
Phase II
Contract:
FA9550-09-C-0081
Award Id:
83348
Agency Tracking Number:
F074-019-0231
Solicitation Year:
n/a
Solicitation Topic Code:
n/a
Solicitation Number:
n/a
Small Business Information
33 Thornwood Drive, Suite 500, Ithaca, NY, 14850
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
101321479
Principal Investigator:
MarkBickford
Senior Principal Scientist
(607) 257-1975
mark@atc-nycorp.com
Business Contact:
RichardSmith
Controller
(607) 257-1975
rick@atc-nycorp.com
Research Institute:
Cornell University
Dan Whitaker
Office of Sponsored Research
373 Pine Tree Road
Ithaca, NY, 14850
(607) 255-5337
Nonprofit college or university
Abstract
Distributed systems have become too complex to develop and maintain without the aid of mathematical techniques supported by automated tools. Abstraction has been the most reliable means for gaining intellectual control of such complexities. Over the past several years, ATC-NY and Cornell University have developed the event logic formalism to support specification and reasoning about distributed systems at a high level of abstraction and the refinement of specifications to a level of abstraction from which it is possible to generate code. The Elan (Event Logic Assistant) tool suite will provide highly automated support for both reasoning and code generation. In Phase II we will prototype the first two Elan products: E#, an extensible notation for programming in event logic, and an E# compiler that generates code for F#, a functional programming language developed and supported by Microsoft Research. The Phase II effort will also integrate E# with the Nuprl logical programming environment, laying the foundation for future research that extends Elan to an environment for developing critical code formally verified to meet its high-level specifications. Phase II builds on Phase I research that introduced new methods for developing distributed algorithms with event logic and new proof tactics in Nuprl. BENEFIT: Distributed systems have become too complex to understand without mathematical techniques. Elan, by providing a programmer's interface to these techniques, will significantly advance our ability to apply them to large scale real-world systems.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government