Computer Science
http://hdl.handle.net/1813/517
2017-05-25T21:55:09ZFlow-Limited Authorization
http://hdl.handle.net/1813/46198
Flow-Limited Authorization
Arden, Owen
Enforcing the confidentiality and integrity of information is critical in
distributed applications. Production systems typically use some form of
authorization mechanism to protect information, but these mechanisms do not
typically provide end-to-end information security guarantees. Information flow
control mechanisms provide end-to-end security, but their guarantees break down
when trust relationships may change dynamically, a common scenario in production
environments. This dissertation presents flow-limited authorization, a new
foundation for enforcing information security.
Flow-limited authorization is an approach to
authorization in that it can be used to reason about whether a principal is
permitted to perform an action. It is an approach to information flow control
in that it can be used to reason about whether a flow of information is secure.
This dissertation presents the theoretical foundation of this approach,
the Flow-Limited Authorization Model (FLAM). FLAM uses a novel principal algebra
that unifies authority and information flow policies and a logic for making
secure authorization and information flow decisions. This logic ensures that
such decisions cannot be influenced by attackers or leak confidential
information.
We embed the FLAM logic in a core programming model, the Flow-Limited
Authorization Calculus (FLAC). FLAC programs selectively enable flows of
information; the type system ensures that attackers cannot create unauthorized
flows. A well-typed FLAC not only ensures proper authorization, but also secure
information flow.
The FLAC approach to secure programming is instantiated in \textsc{Flame}, a
library and compiler plugin for enforcing flow-limited authorization in Haskell
programs. Flame uses type-level constraints and monadic effects to statically
enforce flow-limited authorization for Haskell programs in a modular way.
2017-01-01T00:00:00ZLightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)
http://hdl.handle.net/1813/45898
Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)
Ferraiuolo, Andrew; Xu, Rui; Zhang, Danfeng; Myers, Andrew C.; Suh, G. Edward
Hardware-based mechanisms for software isolation are becoming
increasingly popular, but implementing these mechanisms correctly has
proved difficult, undermining the root of security.
This work introduces an effective way to formally verify important
properties of such hardware security mechanisms. In our approach,
hardware is developed using a lightweight security-typed hardware
description language (HDL) that performs static information flow analysis.
We show the
practicality of our approach by implementing and verifying a
simplified but realistic multi-core prototype of the ARM TrustZone
architecture.
To make the security-typed HDL expressive enough to verify
a realistic processor, we develop new type system features.
Our experiments suggest that information flow analysis
is efficient, and programmer effort is modest. We also show that information
flow constraints are an effective way to detect hardware
vulnerabilities, including several found in commercial processors.
2017-01-29T00:00:00ZOn Free ω-Continuous and Regular Ordered Algebras
http://hdl.handle.net/1813/45054
On Free ω-Continuous and Regular Ordered Algebras
Esik, Zoltan; Kozen, Dexter
Let E be a set of inequalities between finite Σ-terms. Let V_ω and V_r denote the varieties of all ω-continuous ordered Σ-algebras and regular ordered Σ-algebras satisfying E, respectively. We prove that the free V_r-algebra R(X) on generators X is the subalgebra of the corresponding free V_ω-algebra F_ω(X) determined by those elements of F_ω(X) denoted by the regular Σ-coterms. We actually establish this fact as a special case of a more general construction for families of algebras specified by syntactically restricted completeness and continuity properties. Thus our result is also applicable to ordered regular algebras of higher order.
2016-01-01T00:00:00ZA Calculus for Flow-Limited Authorization: Technical Report
http://hdl.handle.net/1813/42406
A Calculus for Flow-Limited Authorization: Technical Report
Arden, Owen; Myers, Andrew C.
Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as membership lists and passwords. Previous formal models for authorization do not fully address the security implications of permitting trust relationships to change, which limits their ability to reason about authority that derives from dynamic computation. Our goal is a way to construct dynamic authorization mechanisms that do not violate confidentiality or integrity.; We introduce the Flow-Limited Authorization Calculus (FLAC), which is both a simple, expressive model for reasoning about dynamic authorization and also an information flow control language for securely implementing various authorization mechanisms. FLAC combines the insights of two previous models: it extends the Dependency Core Calculus with features made possible by the Flow-Limited Authorization Model. FLAC provides strong end-to-end information security guarantees even for programs that incorporate and implement rich dynamic authorization mechanisms. These guarantees include noninterference and robust declassification, which prevent attackers from influencing information disclosures in unauthorized ways. We prove these security properties formally for all FLAC programs and explore the expressiveness of FLAC with several examples.
2016-09-13T00:00:00ZBlock-safe Information Flow Control
http://hdl.handle.net/1813/44564
Block-safe Information Flow Control
Kozyri, Elisavet; Desharnais, Josée; Tawbi, Nadia
Flow-sensitive dynamic enforcement mechanisms for information flow labels offer increased permissiveness.
However, these mechanisms may leak sensitive information when deciding to block insecure executions.
When enforcing two labels (e.g., secret and public), sensitive information is leaked from the context in which this decision is taken.
When enforcing arbitrary labels, additional sensitive information is leaked from the labels
involved in the decision to block an execution.
We give examples where, contrary to a common belief, a mechanism designed to enforce
two labels may not be able to enforce arbitrary labels, due to this additional leakage.
In fact, it is not trivial to design
a dynamic enforcement that offers increased permissiveness,
handles multiple labels, and does not introduce information leakage due to blocking insecure executions.
In this paper, we present a dynamic enforcement mechanism of information flow labels
that has all these three attributes.
Our mechanism is not purely dynamic, since it uses a light-weight, on-the-fly,
static analysis of untaken branches. We prove that the set of all normally terminated
and blocked traces of a program, which is executed under our mechanism, satisfies
noninterference, against principals that make observations throughout execution.
2016-08-09T00:00:00Z00_A Directory of the Oral Histories of Computer Science at Cornell University
http://hdl.handle.net/1813/44201
00_A Directory of the Oral Histories of Computer Science at Cornell University
Cooke, J. Robert
2016-06-16T00:00:00ZJRIF: Reactive Information Flow Control for Java
http://hdl.handle.net/1813/41194
JRIF: Reactive Information Flow Control for Java
Kozyri, Elisavet; Arden, Owen; Myers, Andrew C.; Schneider, Fred B.
A reactive information flow (RIF) automaton for a value v specifies (i) allowed uses for v and (ii) the RIF automaton for any value that might be directly or indirectly derived from v. RIF automata thus specify how transforming a value alters how the result might be used. Such labels are more expressive than existing approaches for controlling downgrading. We devised a type system around RIF automata and incorporated it into Jif, a dialect of Java that supports a classic form of labels for information flow. By implementing a compiler for the resulting JRIF language, we demonstrate how easy it is to replace a classic information-flow type system by a more expressive RIF-based type system. We programmed two example applications in JRIF, and we discuss insights they provide into the benefits of RIF-based security labels.
2016-02-12T00:00:00ZA Conversation with Fred Schneider
http://hdl.handle.net/1813/41370
A Conversation with Fred Schneider
Schneider, Fred B.; Gries, David
Fred Schneider, an expert in concurrent and distributed systems and in computer and cybersecurity, shares insights about how his professional interests evolved, and provides sweeping views about how his field and department have changed.; Fred B. Schneider joined Cornell Computer Science in 1978 and is currently (2016) Chair of CS. His research has
focused on various aspects of trustworthy systems, from operating systems to formal methods to legal and economic
measures for improving trustworthiness.
Fred is a member of the National Academy of Engineering and a foreign member of the Norwegian Academy of
Technological Science. He has an honorary doctorate from the University of Newcastle-upon-Tyne, and he received
two awards for seminal research (IEEE Piore award and the SOSP Hall of Fame award).
Besides being recognized for technical contributions, Fred has served on numerous government and industry
boards and committees, and he just received the “Service to CRA Award” for his contributions to the Computing
Research Association.
Here, Fred shares insights about how his professional interests evolved and provides sweeping views about how his
field and department have changed.
Running Time: 43 min. http://hdl.handle.net/1813/41370
2015-09-09T00:00:00ZA Conversation with Claire Cardie
http://hdl.handle.net/1813/41216
A Conversation with Claire Cardie
Cardie, Claire; Constable, Robert L.
Claire Cardie discusses the role of Gerard Salton, natural language processing and the creation of the Information Science Department.; Claire Cardie joined CS in 1994, helping CS get a foothold in Artificial Intelligence. Part of her research was in
statistical machine learning methods to identify opinions and other subjective language in online text. This led to
the social media startup Appinions Inc., which provided services that let people see the web through the lens of
peoples’ opinions. Appinions was sold in 2015 to ScribbleLive.
Her achievements include a Faculty Early CAREER award from the NSF, election as a Councillor of the Association
for the Advancement of AI, election as Secretary of the Association for Computational Linguistics, and
selection as an ACL Fellow.
Claire has done her share of service to Cornell. With the support and urging of CS, Claire led the development
of the IS (Information Science) major in three colleges and the founding of the Department of IS, serving as first
chair.
Along with interviewer Bob Constable, Claire discusses what the department was like when she joined it, including
her interactions with Gerry Salton (father of Information Retrieval), natural language processing, the creation
of the IS Department, and more.
Running Time: 53 min. http://hdl.handle.net/1813/41216
2015-09-09T00:00:00ZA Conversation with Ken Birman
http://hdl.handle.net/1813/41207
A Conversation with Ken Birman
Birman, Ken; Van Renesse, Robbert
Ken Birman discusses the origins of cloud computing.; Ken Birman, who joined CS in 1981, exemplifies the successful synergy of research and entrepreneurial activities.
His research in distributed systems led to his founding ISIS Distributed Systems, Inc., in 1988, which developed
software used by the New York Stock Exchange (NYSE) and Swiss Exchange, the French Air Traffic Control system,
the AEGIS warship, and others. He started two other companies, Reliable Network Solutions and Web Sciences
LLC.
This entrepreneurship has in turn generated new research ideas and has also led to Ken’s advising various organizations
on distributed systems and cloud computing, including the French Civil Aviation Organization, the northeastern
electric power grid, NATO, the US Treasury, and the US Air Force.
Ken has received several awards for his research, among them the IEEE Tsutomu Kanai Award for his work on
trustworthy computing, the Cisco “Technology Visionary” award, and the ACM SIGOPS Hall of Fame Award. He
also has written two successful texts.
Here, Ken and interviewer Robbert Van Renesse discuss the origins of cloud computing.
Running Time: 46 min. http://hdl.handle.net/1813/41207
2015-09-10T00:00:00ZA Conversation with Dexter Kozen
http://hdl.handle.net/1813/41206
A Conversation with Dexter Kozen
Kozen, Dexter; Constable, Robert L.
Kozen discusses his experiences at Cornell – his research and teaching experience, textbooks, participation in sports & music, etc.; Dexter Kozen got his PhD from CS at Cornell in 1977. After he spent time doing research at IBM, we drew him
back to the faculty in 1985.
Dexter has made lasting, fundamental contributions to diverse areas such as algorithms, complexity, logics, semantics
of programming languages, and computer security. The CS Department’s environment, which encourages
collaboration of people in different areas, both experimental and theoretical, has had a synergistic effect on both
his and others’ research.
One computer scientist said that: a winning combination of brilliance, depth, and elegance captures the essence
of Kozen’s work over the years. And it shows in the influence Dexter has had. He received the LICS Test-of-Time
Award for one of his papers, the EATCS Award from the European Association for Theoretical Computer Science,
the W. Wallace McDowell Award from the IEEE Computer Society, and two prizes from the Polish Ministry of
Education. He also has several teaching awards from Cornell. Further, he has written textbooks on the theory of
computation, automata theory, dynamic logic, and algorithms.
With interviewer Bob Constable, Dexter discusses his research and teaching experience, textbooks, participation
in sports and music, and more.
Running Time: 45 min. http://hdl.handle.net/1813/41206
2015-09-09T00:00:00ZA Conversation with Charlie Van Loan
http://hdl.handle.net/1813/41201
A Conversation with Charlie Van Loan
Van Loan, Charlie; Bala, Kavita
Van Loan discusses his experiences with teaching, writing textbooks, administering degree programs, MatLab, matrices and more.; Charlie Van Loan, who joined the CS Department in 1975, is well known for his work in scientific computing,
especially in “Matrix Computations”. His text with that title, written with Gene Golub and first published in 1983,
is now in its fourth edition. Website scholar.google.com claims 52,900 citations! It’s one of the most highly cited
texts in all of mathematics and computing.
Charlie has helped shape the direction and tone of the department in many ways. He served as chair for 7 years.
He directed the undergrad program for 9 years, the MEng program for 3 years, and the PhD program for 5 years.
He has several awards from Cornell for his teaching and advising, and two PhD advisees chose him for the Merrill
Scholar Faculty Impact Award.
Even as he retires (June 2016), Charlie continues serving Cornell, for he was elected Dean of the Faculty and assumed
that position on July 1.
Van Loan, with the help of interviewer Kavita Bala, discusses his experiences with teaching, writing textbooks,
administering degree programs, MatLab, matrices, and more.
Running Time: 56 min. http://hdl.handle.net/1813/41201
2015-09-15T00:00:00ZA Conversation with Tim Teitelbaum
http://hdl.handle.net/1813/40865
A Conversation with Tim Teitelbaum
Teitelbaum, Tim; Gries, David
A discussion of the teaching of large, introductory courses in programming in the early days-using the Terak and Macintosh computers and
the development of integrated programming environments that implement language-aware editing capabilities.; Tim Teitelbaum carried a major load in the teaching end of the department, especially the intro programming
courses. In the late 1970’s, Tim, along with PhD student Tom Reps, took advantage of the new desktop computer,
the Terak, to build the Cornell Program Synthesizer, a seminal, ground-breaking environment for developing and
testing programs. Cornell immediately adopted it for their intro Pascal courses, and its use spread to many other
universities. Tim and Tom went further to develop the Program Synthesizer Generator, to make it easier to create
such environments for any language, and turned it into a general tool for static analysis of programs.
In 1988, they founded GrammaTech to promote its use. Now, Grammatech, with over 20 PhD employees, is a
leading developer of software-assurance tools and advanced cyber-security solutions. Tim became Prof Emeritus
in 2010 to devote full time to GrammaTech.
Tim and David talk about the teaching of large, introductory courses in programming in the early days using the
Terak and Macintosh computers and the development of integrated programming environments that implement
language-aware editing capabilities.
Running Time: 36 min. http://hdl.handle.net/1813/40865
2015-09-10T00:00:00ZA Conversation with David Gries
http://hdl.handle.net/1813/40576
A Conversation with David Gries
Gries, David; Constable, Robert L.
David Gries joined Cornell in 1969. He was chair of CS in the 1980s and associate dean of engineering for 8 years
in the 2000s.
His research was on compiler writing and areas related to formal programming methodology. He is known for his
texts on programming, on compiler writing (the first such text, in 1971), on the science of programming, and on
logic and discrete math.
He has two honorary doctorates and four awards from the leading computing societies for contributions to education.
He was among the first ten Cornell faculty to receive the Weiss Presidential Fellow award for contributions
to undergrad education. He was Chair of the Computer Science Board when it became the CRA (Computing Research
Association) and opened an office in Washington to represent the interests of computing in academia. He
received the CRA award for service to the computing community.
David and Bob talk about David’s time as a grad student at the Munich Institute of Technology and the early days
in the Cornell CS Department.
Running Time: 51 min. http://hdl.handle.net/1813/40576
2015-07-21T00:00:00ZA Conversation with John E. Hopcroft
http://hdl.handle.net/1813/40568
A Conversation with John E. Hopcroft
Hopcroft, John E.; Gries, David
This ACM Turing Award recipient talks about research, textbooks, working with graduate students, his role as a senior statesman of his field and concludes with some words of wisdom.; John E. Hopcroft has contributed massively to research, education, and service like no other.
His research in theory and algorithms won him the Turing Award in 1986. His early texts set the direction and tone
for the new field of CS. His service as Dean of Engineering, member of the National Science Board, and advisor
on education and research to universities and governments around the world is mind boggling. With too many
awards and society memberships to mention (including at least 5 honorary degrees), in 2016, 52 years after entering
the field, John is still going strong.
Here, John talks about research, textbooks, working with graduate students, and his role as a senior statesman,
concluding with some words of wisdom.
Running Time: 37 min. http://hdl.handle.net/1813/40568
2015-07-21T00:00:00ZA Conversation with Richard W. Conway
http://hdl.handle.net/1813/40564
A Conversation with Richard W. Conway
Conway, Richard W.; Gries, David
Dick Conway came to Cornell in 1949, as a freshman. He received the first PhD from Operations Research and
Industrial Engineering (1958), was instrumental in the creation of the CS Department (1965) and was a founding
member, spent two years as the first Director of Cornell’s Office of Computer Services, and later joined the Johnson
Graduate School of Management. In all these positions, he made significant contributions.
His 1967 co-authored text “Theory of Scheduling” placed the study of production scheduling on a formal foundation.
INFORMS lists the book as a landmark in the timeline of Operations Research. He developed and implemented
the programming languages CORC (1958) and CUPL (1962). In the 1970’s, he developed and implemented
PL/C, with an emphasis on error correction in the compiler, and co-authored a programming text. In the
Johnson Graduate School, Dick introduced and implemented the idea of an immersion course, where students
took one 15-credit course, “Semester in Manufacturing”, spending half the time visiting manufacturing plants and
the other half in the classroom.
Dick is a member of the National Academy of Engineering.
Dick and David Gries discuss the beginnings of CS at and what it was like in the 1970s.
Running Time: 58 min. http://hdl.handle.net/1813/40564
2015-07-21T00:00:00ZA Conversation with Robert L. Constable
http://hdl.handle.net/1813/40560
A Conversation with Robert L. Constable
Constable, Robert L.; Gries, David
Over 40 years ago, Bob Constable and his students started designing a logical language for specifying programming
tasks and mathematical problems. The system, called Nuprl, is known since 1984 for being able to synthesize
correct-by-construction programs from formal proofs in constructive type theory.
The Nuprl Library holds over 15,000 mathematical theorems, with a database of 450,000 proof steps, dealing with
pure mathematics as well as proofs of programs. Bob received the 2014 Herbrand Award for this pioneering research
in automated reasoning.
Bob was also the leading force in Cornell’s creation of CIS ---the Faculty of Computing and Information Science
---which has helped bring computing and computer science into every Cornell college. Bob served as first dean of
CIS for ten years.
Bob and interviewer David Gries talk about the old days in CS.
Running Time: 47 min. http://hdl.handle.net/1813/40560
2015-07-21T00:00:00ZA Conversation with Anil Nerode
http://hdl.handle.net/1813/40527
A Conversation with Anil Nerode
Nerode, Anil; Gries, David
Anil Nerode is the Goldwin Smith Professor of Mathematics. He joined the Cornell Math Department in 1959. His
interests are in mathematical logic, the theory of automata, computability and complexity theory, the calculus of
variations, distributed systems, and artificial intelligence. CS people know him for the very early Myhill–Nerode
theorem, which gives necessary and sufficient conditions for a formal language to be regular.
Anil has long been a friend of CS. He was acting director of the Center for Applied Math from 1964-1965, when
the formation of the CS Department was underway. That put him on the committee that worked to start the CS
Department. He was the one who suggested Juris Hartmanis for the first chair of CS and, about 35 years later, he
said that Juris “was far and away the best chairman of any department”.
In this interview, Anil and interviewer David Gries discuss the start of the CS department.
Running Time: 55 min. http://hdl.handle.net/1813/40527
2014-10-16T00:00:00ZFlow-Limited Authorization
http://hdl.handle.net/1813/40138
Flow-Limited Authorization
Arden, Owen; Liu, Jed; Myers, Andrew
Because information flow control mechanisms often rely on an underlying
authorization mechanism, their security guarantees can be
subverted by weaknesses in authorization. Conversely, the security
of authorization can be subverted by information flows that
leak information or that influence the delegation of authority among
principals.
We argue that interactions between information flow and authorization
create security vulnerabilities that have not been fully identified or
addressed in prior work.
We explore how the security of decentralized information
flow control (DIFC) is affected by
three aspects of its underlying authorization mechanism: first,
delegation of authority between principals; second, revocation of
previously delegated authority; third, information flows created by
the authorization mechanisms themselves. It is no surprise
that revocation poses challenges, but we show that even delegation
is problematic because it enables unauthorized
downgrading. Our solution is a new security model, the Flow-Limited
Authorization Model (FLAM), which offers a new, integrated approach to
authorization and information flow control.
FLAM ensures robust authorization, a novel security condition for
authorization queries that ensures attackers cannot influence
authorization decisions or learn confidential trust relationships.
We discuss our prototype implementation and its algorithm for
proof search.
Content file updated at author's request on 2015-06-04.
2015-05-08T00:00:00ZA Conversation with Juris Hartmanis
http://hdl.handle.net/1813/14934
A Conversation with Juris Hartmanis
Hartmanis, Juris
Juris Hartmanis is video taped in a far-reaching conversation (70 minutes) with colleague David Gries. They discuss Hartmanis’ childhood and family background and his immigration to the United States. Next they trace his extraordinary career at the GE Research Laboratory, where he collaborated with Richard Stearns on pioneering research that eventually was recognized by ACM’s prestigious, highest honor – the Turing Award. After having served earlier as an Instructor in Cornell’s Mathematics Department, Juris returned to Cornell as a full professor and the founding chair of a new department of Computer Science. This Department was embedded in two colleges, Engineering
and Arts and Sciences. Cornell was among the first Universities to establish a Department of Computer Science. His pioneering work on computational
complexity blossomed into a new field and under his leadership the Computer Science department matured into a robust, national leader with a strong theoretical emphasis.
After a successful stint at the National Science Foundation leading the transition
of the academic research network NSFnet to become the Internet, he returned to Cornell. At Cornell he continues an active program of research and maintains a leadership role in developing information technologies that have become a ubiquitous element across the entire Cornell academic scene.; Juris Hartmanis joined Cornell in 1965 as the founding chair of the new Department of Computer Science. One
of the first CS departments (the first started in 1964), CS was embedded in two colleges, Engineering and Arts &
Sciences. Under his leadership, CS matured into a robust, national leader with a strong theoretical emphasis.
Juris came from GE, where he collaborated with Richard Stearns on pioneering research that was later recognized
by ACM’s prestigious, highest honor: the Turing Award. Fittingly, Juris is known as “the father of computational
complexity”. He is a member of the NAE and NAS, has honorary doctorates, and received the Grand Medal of the
Latvian Academy of Sciences.
Like most of the CS faculty, Juris spent time in the service of the CS community. He chaired a National Research
Council Study, resulting in the book “Computing the Future”. In 1996-1998, he was Assistant Director of the NSF
Directorate of Computer and Information Science and Engineering (CISE).
In this conversation (70 minutes), Juris and David talk about his childhood, his family background, his immigration
to the US, and his career.
Running Time: 70 min. http://hdl.handle.net/1813/14934
2010-03-31T00:00:00ZA Linear List Merging Algorithm
http://hdl.handle.net/1813/10810
A Linear List Merging Algorithm
Hopcroft, John E.; Ullman, Jeffrey D.
A linear list merging algorithm and its analysis is presented. Starting with n lists, each containing a single element, the algorithm will execute an arbitrary sequence of requests to merge lists and to find the name of the list currently containing a given element. If the length of the sequence of requests is bounded by a constant times n, then the execution time of the algorithm on a random access computer is bounded by a constant times n.
2008-05-14T13:42:16ZOn the Modelling Power of Petri Nets
http://hdl.handle.net/1813/7516
On the Modelling Power of Petri Nets
Meiling, Erik
The behavior of a Petri net is expressed as a formal language. Certain families of Petri net languages are characterized by propositions similar to the classical pumping theorems. The results are used to give examples of behaviors that cannot be expressed by languages in these families.
1979-12-01T00:00:00ZCand and Cor Before and Then or Else in Ada
http://hdl.handle.net/1813/7515
Cand and Cor Before and Then or Else in Ada
Gries, David
NO ABSTRACT SUPPLIED
1979-11-01T00:00:00ZA Proof Technique for Communicating Sequential Processes(With an Example)
http://hdl.handle.net/1813/7514
A Proof Technique for Communicating Sequential Processes(With an Example)
Levin, Gary Marc
We present proof rules for an extension of the Communicating Sequential Processes proposed by Hoare. The send and receive statements are treated symmetrically, simplifying the rules and allowing send to appear in guards. An example is given to explain the use of the technique. This is an outline of a substantial part of a PhD thesis that is expected to be completed in June 1980.
1979-11-01T00:00:00ZOn Linear Natural Deduction
http://hdl.handle.net/1813/7513
On Linear Natural Deduction
Leivant, Daniel
NO ABSTRACT SUPPLIED
1979-11-01T00:00:00ZThe System Architecture for CORE: A Tolerant Program Development Environment
http://hdl.handle.net/1813/7512
The System Architecture for CORE: A Tolerant Program Development Environment
Archer, James E., Jr.; Conway, Richard W.; Shore, Andrew I.; Silver, Leonard S.
CORE is a program development environment intended primarily to explore a highly tolerant useer interface. In some respects the internal architecture is also novel. It permits a highly interactive and supportive user interface to be implemented with processing routines which are essentially oblivious to any user interaction.
1979-10-01T00:00:00ZA Program Development System Execution Supervisor
http://hdl.handle.net/1813/7511
A Program Development System Execution Supervisor
Archer, James E., Jr.; Shore, Andrew I.
The Cornell Program Development System is an experimental vehicle to explore the applicability of highly cooperative tactics to a contemporary development environment. The CPDS provides significant facilities for modifying and immediately executing programs. The execution supervisor and the internal user program representation it uses to implement these facilities are described.
1979-10-01T00:00:00ZQuadratic Programming with M-Matrices
http://hdl.handle.net/1813/7510
Quadratic Programming with M-Matrices
Luk, Franklin T.; Pagano, Marcello
In this paper, we study the problem of quadratic programming with M-matrices. We describe (1) an effective algorithm for the case where the variables are subject to a lower bound constraint, and (2) an analogous algorithm for the case where the variables are subject to lower and upper bounds constraints. We demonstrate the special monotone behavior of the iterate and gradient vectors. The result on the gradient vector is new. It leads us to consider a simple updating procedure which preserves the monotonicity of both vectors. The procedure uses the fact that an M-matrix has a non-negative inverse. Two new algorithms are then constructed by incorporating this updating procedure into the two given algorithms. We give numerical examples which show that the new methods can be more efficient than the original ones.
1979-10-01T00:00:00ZAda/CS - An Instructional Subset of the Programming Language Ada
http://hdl.handle.net/1813/7509
Ada/CS - An Instructional Subset of the Programming Language Ada
Archer, James E., Jr.
NO ABSTRACT SUPPLIED
1979-10-01T00:00:00ZA Unified View of Semantics
http://hdl.handle.net/1813/7508
A Unified View of Semantics
Majster, Mila E.
NO ABSTRACT SUPPLIED
1979-10-01T00:00:00ZEfficient On-Line Construction and Correction of Position Trees
http://hdl.handle.net/1813/7507
Efficient On-Line Construction and Correction of Position Trees
Majster, Mila E.
This paper presents an on-line algorithm for the construction of position trees, i.e. an algorithm which constructs the position tree for a given string while reading the string from left to right. In addition, an on-line correction algorithm is presented which - upon a change in the string - can be used to construct the new position tree. Moreover, special attention is paid to computers with small memory. Compactification of the trees and transport costs between main and secondary storage are discussed.
1979-10-01T00:00:00ZEnsuring Consistency in a Distributed Database System by Use of Distributed Semaphores
http://hdl.handle.net/1813/7506
Ensuring Consistency in a Distributed Database System by Use of Distributed Semaphores
Schneider, Fred B.
Solutions to the database consistency problem in distributed databases are developed. It is shown how any solution to the consistency problem for a centralized database system that involves locking can be adapted for use in distributed systems. This is done, constructively, in two steps. First, it is shown how locking can be implemented in terms of semaphores. Then, a semaphore implementation that is suitable for use in distributed systems is developed.
1979-09-01T00:00:00ZSynchronization in Distributed Programs
http://hdl.handle.net/1813/7505
Synchronization in Distributed Programs
Schneider, Fred B.
A technique for solving synchronization problems in distributed programs is described. Use of this technique in environments in which processes may fail is discussed. The technique can be used to solve synchronization problems directly, to implement new synchronization mechanisms (which are presumably well suited for use in distributed programs), and to construct distributed versions of existing synchronization mechanisms. Use of the technique is illustrated with implementations of distributed semaphores and a conditional message passing facility.
1979-09-01T00:00:00ZOn Easily Infinite Sets and On a Statement of R. Lipton
http://hdl.handle.net/1813/7504
On Easily Infinite Sets and On a Statement of R. Lipton
Leivant, Daniel
For a complexity measure $\kappa$, a set is $\kappa$-infinite if it contains a $\kappa$-decidable infinite subset. For a time-based $\kappa$, we prove that there is a recursive S s.t. both S and its complements, $\bar{S}$, are infinite but not $\kappa$-infinite. Lipton [6] states that the existence of a recursive set S s.t. neither S nor $\bar{S}$ os polynomially infinite is not a purely logical consequence of $\prod^{0}_{2}$ theorems of Peano's Arithmetic PA. His proof uses a construction of an algorithm within a non-standard model of of Arithmetic, in which the existence of infinite descending chains in such models is overlooked. We give a proof of a stronger statement to the effect that the existence of a recursive set S s.t. neither S nor $\bar{S}$ is linearly infinite is not a tautological consequence of all true $\prod^{0}_{2}$ assertions. We comment on other aspects of [6], and show $(\S 2)$ that a tautological consequence of true $\prod^{0}_{2}$ assertions may not be equivalent (in PA, say) to a $\prod^{0}_{2}$ sentence. The three sections of this paper use techniques of Recursion Theory, Proof Theory and Model Theory, respectively.
1979-09-01T00:00:00ZA Logic For Correct Program Development
http://hdl.handle.net/1813/7503
A Logic For Correct Program Development
Bates, Joseph Louis
1979-08-01T00:00:00ZThe Complexity of Parallel Computations
http://hdl.handle.net/1813/7502
The Complexity of Parallel Computations
Wyllie, James C.
Recent advances in microelectronics have brought closer to feasibility the construction of computers containing thousands (or more) of processing elements. This thesis addresses the question of effective utilization of such processing power. We study the computational complexity of synchronous paarallel computations using a model of computation based on random access machines operating in parallel and sharing a common memory, the P-RAM. Two main areas within the field of parallel computational complexity are investigated. First, we explore the power of the P-RAM model viewed as an abstract computing device. Later, we study techniques for developing efficient algorithms for parallel computers. We are able to give concise characterizations of the power of deterministic and nondeterministic P-RAMS in terms of the more widely known space and time complexity classes for multi-tape Turing machines. Roughly speaking, time-bounded deterministic P-RAMS are equivalent in power to (can accept the same sets as) space-bounded Turing machines, where the time and space bounds differ by at most a polynomial. In the context of comparing models of computation, we consider such polynomial differences in resources to be insignificant. Adding the feature of nondeterminism to the time-bounded P-RAM changes its power to that of a nondeterministic Turing machine with an exponentially higher running time. The later sections of the thesis examine algorithm design techniques for parallel computers. We first develop efficient procedures for some common operations on linked lists and arrays. Given this background, we introduce three techniques that permit the design of parallel algorithms that are efficient in terms of both their time and processor requirements. We illustrate the use of these techniques by presenting time and processor efficient algorithms for three problems, in each case improving upon the best previously known parallel resource bounds. We show how to compute minimum string edit distances, using the technique of pairwise function composition. We describe an algorithm for the off-line MIN that organizes its computation in the form of a complete binary tree. Finally, we present an algorithm for undirected graph connectivity that relies on redundancy in its representation of the input graph.
1979-08-01T00:00:00ZA Linear Time Algorithm for the Generalized Consecutive Retrieval Problem
http://hdl.handle.net/1813/7501
A Linear Time Algorithm for the Generalized Consecutive Retrieval Problem
Dietz, Paul F.; Furst, Merrick; Hopcroft, John E.
THe Generalized Consecutive Retrieval Problem (GCRP) is to find a directed tree on $n$ records in which each of $k$ subsets forms a directed path. The problem arises in organizing information for efficient retrieval. A linear time algorithm for the GCRP is given. Further generalization leads to problems that are complete for NP.
1979-07-01T00:00:00ZA Time-Space Tradeoff for In-Place Array Permutation
http://hdl.handle.net/1813/7500
A Time-Space Tradeoff for In-Place Array Permutation
Melville, Robert C.
NO ABSTRACT SUPPLIED
1979-07-01T00:00:00ZConvergence Theorems for Least Change Secant Update Methods
http://hdl.handle.net/1813/7499
Convergence Theorems for Least Change Secant Update Methods
Dennis, John E. Jr.; Walker, Homer F.
The purpose of this paper is to present a convergence analysis of the least change secant methods in which part of the derivative matrix being approximated is computed by other means. The theorems and proofs given here can be viewed as generalizations of those given by Broyden-Dennis-More and by Dennis-More. The analysis is done in the orthogonal projection setting of Dennis-Schnabel and many readers might feel that it is easier to understand. The theorems here readily imply local and q-superlinear convergence of all the standard methods in addition to proving these results for the first time for the sparse symmetric method of Marwil and Toint and the nonlinear least squares method of Dennis-Gay-Welsch.
1979-07-01T00:00:00ZLocal Convergence Theorems for Quasi-Newton Methods
http://hdl.handle.net/1813/7498
Local Convergence Theorems for Quasi-Newton Methods
Dennis, John E. Jr.; Walker, Homer F.
This paper presents generalizations of the two results which have been useful for analyzing methods of the form $x_{k+1} = x_{k} - B_{k}^{-1}F(x_{k})$. The bounded deterioration theorem of Broyden-Dennis-More is generalized to show that if \{$B_{k}$\} or \{$B_{k}^{-1}$\} is of bounded deterioration as a sequence of approximants to some $B_{*}$ or $B_{*}^{-1}$ then the iteration above has the same local convergence properties and arbitrarily nearly the same linear rate as would be achieved by the stationary iteration function which uses $B_{k} = B_{*}$. The characterization theorem for superlinear convergence given by Dennis-More is then generalized to give conditions under which the rates are the same. In the case when $B_{*} = F'(x_{*})$, these results reduce to those already known.
1979-07-01T00:00:00ZEfficiency Considerations In Implementing Dijkstra's Guarded Command Constructs
http://hdl.handle.net/1813/7497
Efficiency Considerations In Implementing Dijkstra's Guarded Command Constructs
McGuire, Marguerite Elaine
The guarded command alternative and iterative constructs proposed by E. W. Dijkstra subsume the conventional alternative and iterative constructs. The extra flexibility of these guarded command constructs enables the programmer to express his ideas more directly and clearly. Moreover, Dijkstra has developed a calculus for the derivation of correct programs that utilizes these guarded command constructs. This thesis addresses the problem of efficiently implementing these guarded command constructs. Several new optimizations that are particularly well suited to the guarded command constructs are described. The most useful is the elimination of redundant boolean expressions. This optimization provides a means of implementing the guarded command alternative statement with efficiency comparable to the IF-THEN-ELSE statement. The main contribution of this thesis is a detailed description of an algorithm for eliminating redundant boolean expressions. The algorithm itself is presented in a program written in a PASCAL supplemented with the guarded command constructs. The basis method involves considering individual execution paths through the guarded command construct and applying rules of inference to recognize and avoid evaluation of many boolean expressions. It is shown that the number of execution paths through a guarded command construct remains small enough to make this method practical.
1979-07-01T00:00:00ZThe Cornell Program Synthesizer: A Tutorial Introduction
http://hdl.handle.net/1813/7496
The Cornell Program Synthesizer: A Tutorial Introduction
Teitelbaum, Tim
This tutorial introduces a novice student to the basic facilities of the Cornell Program Synthesizer for developing programs written in the PL/CS dialect of PL/I. No knowledge of programming is assumed or required. It is assumed that you possess a Synthesizer diskette and have access to a TERAK microcomputer.
1979-07-01T00:00:00ZOn the Proof Theory of the Modal Logic G
http://hdl.handle.net/1813/7495
On the Proof Theory of the Modal Logic G
Leivant, Daniel
NO ABSTRACT SUPPLIED
1979-07-01T00:00:00ZA Procedure Call Proof Rule (With a Simple Explanation)
http://hdl.handle.net/1813/7494
A Procedure Call Proof Rule (With a Simple Explanation)
Gries, David; Levin, Gary Marc
NO ABSTRACT SUPPLIED
1979-05-01T00:00:00ZUpson's Familiar Quotations
http://hdl.handle.net/1813/7493
Upson's Familiar Quotations
Gaulle, Al
This report is a compilation of several hundred examples of context free language and very irregular expressions. Contributions were submitted over the last five years by numerous computer science graduate students who collected these now immortal words in classes and seminars. We wish to express our gratitude to the faculty, guest lecturers, and students who provided the bulk of this work.
1979-05-01T00:00:00ZA Hamiltonian-Schur Decomposition
http://hdl.handle.net/1813/7492
A Hamiltonian-Schur Decomposition
Paige, Chris; Van Loan, Charles
1979-09-01T00:00:00ZComputer Science and the Liberal Arts Student
http://hdl.handle.net/1813/7491
Computer Science and the Liberal Arts Student
Van Loan, Charles
The computer science education of nontechnical liberal arts students is a matter of increasing concern. In this paper it is argued that computer scientists should promote and teach their subject more in line with the traditional aims of liberal education when dealing with students of this type. A framework for doing this is presented which involves a broad view of "computer literacy" based upon what other authors have written about "scientific literacy." The structure of a computer science appreciation course is outlined which embodies the ideas of liberal education described. The importance of historical perspective is emphasized. Key Words and Phrases: Computer literacy, liberal arts student, liberal education, history of computation, scientific literacy.
1979-05-01T00:00:00ZRepresentation of Almost Constant Vectors
http://hdl.handle.net/1813/7490
Representation of Almost Constant Vectors
Steensgaard-Madsen, Jorgen
An example in a recent report on the programming language Russell has illustrated difficulties related to user defined storage management. Here is demonstrated how the dynamic approach to encapsulation earlier proposed by the author provides means to solve the particular storage management problem. The method used is, however, easily generalized to other similar cases. In addition to the example a number of notational conveniences are introduced. One that allows abbreviated references to components of record-like structures is called controlled coercion. Another allows a function-like use of classes. Keywords: Classes, abstract data types, storage management, programming languages.
1979-04-01T00:00:00ZOn Restrictions to Ensure Reproducible Behavior in Concurrent Programs
http://hdl.handle.net/1813/7489
On Restrictions to Ensure Reproducible Behavior in Concurrent Programs
Schneider, Fred B.; Bernstein, A. J.
One of the major difficulties encountered when dealing with concurrent programs is that reproducible behavior may not be assumed. As a result, it is difficult to validate and debug such systems. In this paper, structural restrictions are presented that ensure that reproducible behavior will occur in concurrent programs. The application of this to system design is discussed. Keywords: time dependent behavior, concurrency, synchronization, monitors, Concurrent Pascal.
1979-03-01T00:00:00ZAPL and the Grzegorczyk Hierarchy
http://hdl.handle.net/1813/7488
APL and the Grzegorczyk Hierarchy
Breidbart, Seth
We show in this paper that the set of "traditional" APL 1-liners (using arithmetic functions only) compute precisely the set of functions in the class E4 of Grzegorczyk hierarchy (the class immediately above the elementary functions). We also show that if we extend the set of 1-liners to include either the "execute" operator, or 1 line programs with gotos, then any partial recursive function can be computed.
1979-03-01T00:00:00Z