Towards Increased Productivity of Algorithm Implementation
Table of Contents:
- Principal Investigator.
- Productivity Measures.
- Summary of Objectives and Approach.
- Detailed Summary of Technical Progress.
- Transitions and DOD Interactions.
- Software and Hardware Prototypes.
- List of Publications.
- Invited and Contributed Presentations.
- Honors, Prizes or Awards Received.
- Project Personnel Promotions.
- Project Staff.
- Multimedia URL.
- Keywords.
- Business Office.
- Expenditures.
- Students.
- Book Plans.
- Sabbatical Plans.
- Related Research.
- History.
Principal Investigator.
- PI Name: Robert A. Paige
- PI Institution: New York University
- PI Phone Number: (212) 998-3156
- PI Fax Number: (212) 995-4124
- PI Street Address: CIMS, 251 Mercer St.
- PI City,State,Zip: New York, NY 10012
- PI E-mail Address: paige@cs.nyu.edu
- PI URL Home Page: http://cs.nyu.edu/cs/faculty.html
- Grant Title: Towards Increased Productivity of
Algorithm Implementation
- Grant/Contract Number: N00014-93-I-0924
- Mipr Number:
- R&T Number: 4331017---01
- Period of Performance: 01 Oct. 94 - 30 Sep. 95
- Today's Date: 05-11-95
Productivity Measures.
- Number of refereed papers submitted not yet published: 2
- Number of refereed papers published: 5
- Number of unrefereed reports and articles: 2
- Number of books or parts thereof submitted but not published: 0
- Number of books or parts thereof published: 0
- Number of project presentations: 9
- Number of patents filed but not yet granted: 0
- Number of patents granted and software copyrights: 0
- Number of graduate students supported >= 25% of full time: 1
- Number of post-docs supported >= 25% of full time: 0
- Number of minorities supported: 0
Summary of Objectives and Approach.
-
Our long term objective is to dramatically improve the programming
productivity of algorithm implementation and labor-intensive software.
Our approach is based on very high level compiler technology with
a generic (as opposed
to domain specific) problem domain, an automatic (as opposed to
interactive) software development methodology, and the production
of high performance (as opposed to prototype) code.
-
During the grant reporting period, the emphasis has been on developing
and applying formal semantics-based reasoning to simultaneously
design algorithms, analyze their asymptotic complexity, and implement
them in high performance code. One aspect of this approach
involved the development of a type and subtype system that abstracts
a sequential
RAM model of computation, and that provides a high level set theoretic
programming language with computational transparency. Another aspect
involved the use of mechanical proof checking to prove the correctness of
transformations that form the basic lemmas in a program derivation.
Detailed Summary of Technical Progress.
-
Our initial thrust was to provide new semantic foundations for finite
differencing based on Hoare Logic. Bard Bloom and I rewrote our paper
for Science of Programming
to incorporate these ideas, which allowed us to rederive more formally
our new ready simulation algorithm and its asymptotic complexity analysis.
The new derivation is ideally suited for mechanical proof checking, and
Alfredo Ferro's group at the U. of Catania in Italy has taken up the
challenge. Ferro and his colleage D. Cantone will be visiting Courant
later this year to combine his expertise (in fast decision procedures
in fragments of set theory) with our transformational methodology.
-
Building on the more solid semantic ground of Bloom and Paige, Keller
and I launched a difficult and comprehensive experiment to combine
algorithm design, analysis, and implementation within a mechanically
checked formal derivation. The type and subtype system developed earlier
with Cai and Henglein was extended to support a computationally
transparent partition datatype. This extension proved useful in
deriving two new DFA minimization algorithms that improved upon the
classical algorithms of Hopcroft and Cardon and Crochemore. The main
proof obligation in the derivation was supported by 7000 lines of
proofware that was passed through Keller's working set theoretic proof checker.
Although the protracted labor involved in building and executing this
proofware was almost overwhelming, the
expense was somewhat offset by a successful reuse of major portions of these
proofs. In particular, the DFA minimization algorithm is obtained by
specializing and then extending the last step in the derivation of the
a high level bisimulation algorithm. This work will appear in Comm. of
Pure and Applied Math.
-
Two other new results can be reported. With Klarlund and his team at the
U. of Aarhus, a new improved incremental BDD-based DFA minimization
algorithm was designed and implemented within the MONA verification tool.
This tool makes use of the second order monadic calculus of strings,
a succinct predicate oriented characterization of regular languages,
in variaous applications of automatic verification.
The work was reported at the TACAS software tool workshop, and our paper
was selected for a special issue of LNCS.
-
We have been studying Willard's RCS theory over a period of years in hopes
of gaining incite into how language abstraction can be used to obtain
algorithmic results. Under the assumption that hashing
unit space data takes unit time, Willard defined subclasses of relational
calculus queries that could be executed in low expected
polynomial time and space
with respect to the input/output space. Previously we reported that
by associating expected complexity with set theoretic terms, Willard's
proofs could be compressed by eliminating redundancy and by replacing raw
counting arguments with more algebraic reasoning. We were also able to
map the linear time fragment of RCS queries into the `simple' subclass
of the linear time set theoretic language of Cai and Paige (cf. POPL 87).
Last year with Deepak Goyal we used our computationally transparent
type and subtype system to obtain an algorithmic improvement.
By typing our set theoretic implementation of RCS, we were able
to prove that the
the linear time fragment of Willard's RCS queries
can be implemented in linear worst case time.
Transitions and DOD Interactions.
Software and Hardware Prototypes.
- Prototype Name: Maximimum Ready Simulation Program
- Type: Algorithm
- URL: http://cs.nyu.edu/cs/faculty/paige/software.html
- Availability: accessible via WWW
- Description: This prototype SETL2 program
computes the maximum ready simulation relation between two
finite transition processes.
- Demonstration Examples: Test Cases and documentation
may be found at the preceding URL.
List of Publications.
-
Bloom, B. and Paige, R., "Transformational Design and Implementation Of a
New Efficient Solution to the Ready Simulation Problem," Science of
Computer Programming, 24(3), June 1995, pp. 189-220.
-
Bouma, W., Cai, J., Fudos, I., Hoffmann, C., and Paige, R., "A Geometric
Constraint Solver," CAD, Vol. 27, No. 6, June, 1995, pp. 487-501.
-
Cai, J. and Paige, R., "Using Multiset Discrimination To Solve Language
Processing Problems Without Hashing," Theoretical Computer Science,
vol 145, Num 1-2, July, 1995, pp. 189-228.
-
Chang, C. and Paige, R., "From Regular Expressions to DFA's Using
Compressed NFA's," accepted for publication, Theoretical Computer Science,
1995.
-
Keller, J. P. and Paige, R., "Program Derivation With Verified
Transformations - A Case Study," in The Houses That Jack Built,
pp. 151 - 208, New York University, Proc. Symp. Celebrating the
Scientific Trajectory of Jack Schwartz, ed. E. Schonberg, May, 1995,
long form accepted in Communications of Pure and Applied Mathematics,
Vol 48, 1995.
-
Henriksen, J., Jensen, J., Jorgensen, M., Klarlund, N., Paige,
R., Rauhe, T., and Sandholm, A., "Mona: Monadic Second-Order Logic In
Practice," Proc. TACAS (Workshop on Tools and Algorithms for
Construction and Analysis of Systems), BRICS Notes Series NS-95-2,
U. of Aarhus, May, 1995, pp. 58-73,; selected to appear in LNCS,
1090, 1995.
-
Paige, R., "Analysis and Transformation of Set-Theoretic Languages,"
Mini-Course Notes, BRICS Notes Series, NS-95-5, University of Aarhus,
Aarhus, Denmark, August 1995.
Invited and Contributed Presentations.
-
Seminar, U. of Lund, "Towards Increased Productivity of Algorithm
Implementation," Aug. 1995.
-
Seminar, U. of Lund, "Viewing A Transformational System at Work,"
Aug. 1995.
-
Minicourse, 4 Lectures with System Demonstration at the
BRICS Center, U. of Aarhus, "Analysis and Transformation
of Set-Theoretic Languages", Aarhus, Denmark, Aug. 1995.
-
Presentation at Atlantique Workshop, "A Reconstruction and
Extension of Willard's Predicate Retrieval Theory," San Diego,
CA., June 1995.
-
Presentation at Symp. Celebrating the Scientific Trajectory
of Jack Schwartz, "Program Derivation With Verified
Program Transformation - A Case Study," New York City, May 1995.
-
MASPLAS 95, Research in Transformational Programming at NYU,
D. Goyal, A. Leung, M. Marinescu, R. Paige, A. Rudra, C. Yung
E. Stroudsburg, PA., Apr. 1995.
Honors, Prizes or Awards Received.
- Invited Speaker at Symp. Celebrating the Scientific Trajectory
of Jack Schwartz, New York City, May 1995.
Project Personnel Promotions.
Project Staff.
- Name: Dr. Robert Paige
- Homepage
- Position: Professor
- Task: Principal Investigator
Multimedia URL.
- EOYL FY95
- QUAD FY95
- EOYL FY94
- Research Project
-
U. of Aarhus On-Line Minicourse on Research
-
Citation To Project Found at CMU in home page on
Semantics-Based Program Analysis and Manipulation
Keywords.
- Transformations
- Algorithm Derivation
- Program Development
- Productivity
Business Office
- Business Office Phone Number: 212-998-3372
- Business Office Fax Number: 212-995-4121
- Business Office Email: hayes@best.nyu.edu
Expenditures
- Est. FY96: 100%
- FY95: 90%
- FY94: 98%
Students
- Name: [Mr|Ms|Dr] Student_name_goes_here
- Homepage
- Position: Your_student_position_title_goes_here
- Nationality: Your_student_nationality_goes_here
- Available for Summer at DoD Lab: Your_guess_goes_here
- Task: Your_student_prj_task_description_goes_here
- Thesis: Your_student_thesis_description_goes_here
Book Plans
Sabbatical Plans
Related Research
-
Semantics-Based Program Analysis and Manipulation
-
IFIP Working Group 2.1---Algorithmic Languages and Calculi
-
BRICS (Basic Research in Computer Science, U. of Aarhus
History