Computer Science Technical Reportshttp://hdl.handle.net/1813/56032017-11-14T10:31:26Z2017-11-14T10:31:26ZUndecidable Problems for Probabilistic Network ProgrammingKahn, Davidhttp://hdl.handle.net/1813/517652017-07-08T07:09:53Z2017-07-07T00:00:00ZUndecidable Problems for Probabilistic Network Programming
Kahn, David
The software defined networking language NetKAT is able to verify many useful properties of networks automatically via a PSPACE decision procedure for program equality. However, for its probabilistic extension ProbNetKAT, no such decision procedure is known. We show that several potentially useful properties of ProbNetKAT are in fact undecidable, including emptiness of support intersection and certain kinds of distribution bounds and program comparisons. We do so by embedding the Post Correspondence Problem in ProbNetKAT via direct product expressions, and by directly embedding probabilistic ﬁnite automata.
2017-07-07T00:00:00ZFlow-Limited AuthorizationArden, Owenhttp://hdl.handle.net/1813/461982017-02-08T08:01:26Z2017-01-01T00:00:00ZFlow-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)Ferraiuolo, AndrewXu, RuiZhang, DanfengMyers, Andrew C.Suh, G. Edwardhttp://hdl.handle.net/1813/458982017-01-30T06:01:31Z2017-01-29T00:00:00ZLightweight 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 AlgebrasEsik, ZoltanKozen, Dexterhttp://hdl.handle.net/1813/450542016-12-07T06:01:47Z2016-01-01T00:00:00ZOn 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 ReportArden, OwenMyers, Andrew C.http://hdl.handle.net/1813/424062016-09-14T16:55:40Z2016-09-13T00:00:00ZA 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 ControlKozyri, ElisavetDesharnais, JoséeTawbi, Nadiahttp://hdl.handle.net/1813/445642016-08-10T05:00:40Z2016-08-09T00:00:00ZBlock-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:00ZJRIF: Reactive Information Flow Control for JavaKozyri, ElisavetArden, OwenMyers, Andrew C.Schneider, Fred B.http://hdl.handle.net/1813/411942016-02-17T16:25:24Z2016-02-12T00:00:00ZJRIF: 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:00ZFlow-Limited AuthorizationArden, OwenLiu, JedMyers, Andrewhttp://hdl.handle.net/1813/401382015-07-09T02:50:00Z2015-05-08T00:00:00ZFlow-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 Linear List Merging AlgorithmHopcroft, John E.Ullman, Jeffrey D.http://hdl.handle.net/1813/108102015-07-08T02:31:17Z2008-05-14T13:42:16ZA 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 NetsMeiling, Erikhttp://hdl.handle.net/1813/75162015-07-07T22:39:38Z1979-12-01T00:00:00ZOn 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 AdaGries, Davidhttp://hdl.handle.net/1813/75152015-07-08T00:42:47Z1979-11-01T00:00:00ZCand 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)Levin, Gary Marchttp://hdl.handle.net/1813/75142015-07-07T22:52:46Z1979-11-01T00:00:00ZA 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 DeductionLeivant, Danielhttp://hdl.handle.net/1813/75132015-07-07T23:03:19Z1979-11-01T00:00:00ZOn Linear Natural Deduction
Leivant, Daniel
NO ABSTRACT SUPPLIED
1979-11-01T00:00:00ZThe System Architecture for CORE: A Tolerant Program Development EnvironmentArcher, James E., Jr.Conway, Richard W.Shore, Andrew I.Silver, Leonard S.http://hdl.handle.net/1813/75122015-07-08T00:07:31Z1979-10-01T00:00:00ZThe 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 SupervisorArcher, James E., Jr.Shore, Andrew I.http://hdl.handle.net/1813/75112015-07-07T22:33:10Z1979-10-01T00:00:00ZA 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-MatricesLuk, Franklin T.Pagano, Marcellohttp://hdl.handle.net/1813/75102015-07-07T22:49:28Z1979-10-01T00:00:00ZQuadratic 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 AdaArcher, James E., Jr.http://hdl.handle.net/1813/75092015-07-08T00:29:35Z1979-10-01T00:00:00ZAda/CS - An Instructional Subset of the Programming Language Ada
Archer, James E., Jr.
NO ABSTRACT SUPPLIED
1979-10-01T00:00:00ZA Unified View of SemanticsMajster, Mila E.http://hdl.handle.net/1813/75082015-07-08T01:34:19Z1979-10-01T00:00:00ZA Unified View of Semantics
Majster, Mila E.
NO ABSTRACT SUPPLIED
1979-10-01T00:00:00ZEfficient On-Line Construction and Correction of Position TreesMajster, Mila E.http://hdl.handle.net/1813/75072015-07-08T00:38:07Z1979-10-01T00:00:00ZEfficient 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 SemaphoresSchneider, Fred B.http://hdl.handle.net/1813/75062015-07-08T00:17:56Z1979-09-01T00:00:00ZEnsuring 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 ProgramsSchneider, Fred B.http://hdl.handle.net/1813/75052015-07-07T22:47:27Z1979-09-01T00:00:00ZSynchronization 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. LiptonLeivant, Danielhttp://hdl.handle.net/1813/75042015-07-08T01:01:26Z1979-09-01T00:00:00ZOn 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 DevelopmentBates, Joseph Louishttp://hdl.handle.net/1813/75032015-07-07T23:07:22Z1979-08-01T00:00:00ZA Logic For Correct Program Development
Bates, Joseph Louis
1979-08-01T00:00:00ZThe Complexity of Parallel ComputationsWyllie, James C.http://hdl.handle.net/1813/75022015-07-07T23:02:53Z1979-08-01T00:00:00ZThe 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 ProblemDietz, Paul F.Furst, MerrickHopcroft, John E.http://hdl.handle.net/1813/75012015-07-08T01:14:49Z1979-07-01T00:00:00ZA 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 PermutationMelville, Robert C.http://hdl.handle.net/1813/75002015-07-07T23:35:46Z1979-07-01T00:00:00ZA 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 MethodsDennis, John E. Jr.Walker, Homer F.http://hdl.handle.net/1813/74992015-07-07T23:47:59Z1979-07-01T00:00:00ZConvergence 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 MethodsDennis, John E. Jr.Walker, Homer F.http://hdl.handle.net/1813/74982015-07-07T23:57:05Z1979-07-01T00:00:00ZLocal 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 ConstructsMcGuire, Marguerite Elainehttp://hdl.handle.net/1813/74972015-07-07T23:33:13Z1979-07-01T00:00:00ZEfficiency 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 IntroductionTeitelbaum, Timhttp://hdl.handle.net/1813/74962015-07-07T23:39:58Z1979-07-01T00:00:00ZThe 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 GLeivant, Danielhttp://hdl.handle.net/1813/74952015-07-08T00:08:50Z1979-07-01T00:00:00ZOn 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)Gries, DavidLevin, Gary Marchttp://hdl.handle.net/1813/74942015-07-07T22:45:06Z1979-05-01T00:00:00ZA Procedure Call Proof Rule (With a Simple Explanation)
Gries, David; Levin, Gary Marc
NO ABSTRACT SUPPLIED
1979-05-01T00:00:00ZUpson's Familiar QuotationsGaulle, Alhttp://hdl.handle.net/1813/74932015-07-07T22:30:39Z1979-05-01T00:00:00ZUpson'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 DecompositionPaige, ChrisVan Loan, Charleshttp://hdl.handle.net/1813/74922015-07-07T23:30:15Z1979-09-01T00:00:00ZA Hamiltonian-Schur Decomposition
Paige, Chris; Van Loan, Charles
1979-09-01T00:00:00ZComputer Science and the Liberal Arts StudentVan Loan, Charleshttp://hdl.handle.net/1813/74912015-07-08T00:18:48Z1979-05-01T00:00:00ZComputer 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 VectorsSteensgaard-Madsen, Jorgenhttp://hdl.handle.net/1813/74902015-07-07T23:59:10Z1979-04-01T00:00:00ZRepresentation 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 ProgramsSchneider, Fred B.Bernstein, A. J.http://hdl.handle.net/1813/74892015-07-08T01:45:51Z1979-03-01T00:00:00ZOn 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 HierarchyBreidbart, Sethhttp://hdl.handle.net/1813/74882015-07-07T23:44:57Z1979-03-01T00:00:00ZAPL 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:00ZThe Cornell Program Synthesizer: A Microcomputer Implementationof PL/CSTeitelbaum, Timhttp://hdl.handle.net/1813/74872015-07-07T22:50:37Z1979-03-01T00:00:00ZThe Cornell Program Synthesizer: A Microcomputer Implementationof PL/CS
Teitelbaum, Tim
NO ABSTRACT SUPPLIED
1979-03-01T00:00:00ZComments on a Draft Pascal StandardSteensgaard-Madsen, Jorgenhttp://hdl.handle.net/1813/74862015-07-08T00:06:33Z1979-02-01T00:00:00ZComments on a Draft Pascal Standard
Steensgaard-Madsen, Jorgen
NO ABSTRACT SUPPLIED
1979-02-01T00:00:00ZA Progress Report on Automatic Information RetrievalSalton, Gerardhttp://hdl.handle.net/1813/74852015-07-07T23:02:46Z1979-02-01T00:00:00ZA Progress Report on Automatic Information Retrieval
Salton, Gerard
This study is a state-of-the-art report of work in automatic information retrieval. Various enhancements of operational on-line retrieval systems are described such as the utilization of special front-end devices providing compatibility among different search services, the introduction of fast back-end search devices, and the use of local clustering and query reformulation operations designed to improve retrieval output. Certain new algorithms for fast text matching and for optimum term weighting are also mentioned, as are advances in the construction of theoretical retrieval models.
1979-02-01T00:00:00ZImplementation of an Unrestricted File Organization for Micro-PL/CSArcher, James E. Jr.http://hdl.handle.net/1813/74842015-07-08T00:51:14Z1979-02-01T00:00:00ZImplementation of an Unrestricted File Organization for Micro-PL/CS
Archer, James E. Jr.
Micro PL/CS is a version of PL/CS developed for a single-user, interactive environment. A file system extension makes PL/CS self-sufficient for standalone file processing and secondary storage management. The basis of the file system extension is the Unrestricted File Organization which provides a free mixture of sequential, indexed and random file operations. The structure, operation, and system-interfaced procedures of the UFO are presented and explained. The Micro-PL/CS file extension implementation is then sketched in terms of the UFO primitives.
1979-02-01T00:00:00ZA File System Extension to Micro-PL/CSArcher, James E., Jr.http://hdl.handle.net/1813/74832015-07-07T22:59:52Z1979-02-01T00:00:00ZA File System Extension to Micro-PL/CS
Archer, James E., Jr.
Micro-PL/CS is a version of PL/CS developed for interactive use with a dedicated microprocessor. A file system extension is proposed to give PL/CS a simple, but extremely powerful file system capability. The system allows for the creation and manipulation of files for sequential, random, or keyed access (or any combination) in an unrestricted manner. Essential to the capability is a set of built-in functions and pseudo-variables which allow file manipulation without syntactic complication.
1979-02-01T00:00:00ZMechanisms for Specifying Scheduling PoliciesSchneider, Fred B.Bernstein, A. J.http://hdl.handle.net/1813/74822015-07-08T00:55:59Z1979-02-01T00:00:00ZMechanisms for Specifying Scheduling Policies
Schneider, Fred B.; Bernstein, A. J.
Extensions to concurrent programming languages are presented which allow control of scheduling policies previously defined by the run-time support system. It is shown that the use of these mechanisms simplifies the solutions of concurrent programming problems. In addition, the proposed extensions allow easy identification of those aspects of a program concerned with performance, thereby making programs easier to read and understand. Keywords: concurrent pascal, monitors, communicating sequential processes, operating systems, scheduling algorithms.
1979-02-01T00:00:00ZA Citation Study of the Computer Science LiteratureSalton, GerardBergmark, D.http://hdl.handle.net/1813/74812015-07-07T22:33:03Z1979-01-01T00:00:00ZA Citation Study of the Computer Science Literature
Salton, Gerard; Bergmark, D.
The bibliographic references and citations which exist between documents in a given collection environment can be used to study the history and scope of particular subject areas and to assess the importance of individual authors, documents, and journals. A clustering study of the computer science literature is described using bibliographic citations as a clustering criterion, and conclusions are drawn regarding the scope of computer science, and the characteristics of individual documents in the area.
1979-01-01T00:00:00ZSuggestions for a Uniform Representation of Query and Record Content in Data Base and Document RetrievalSalton, Gerardhttp://hdl.handle.net/1813/74802015-07-07T22:43:47Z1979-01-01T00:00:00ZSuggestions for a Uniform Representation of Query and Record Content in Data Base and Document Retrieval
Salton, Gerard
A standard approach is introduced for the representation of information content in data base and document retrieval environments. The use of composite concept vectors representing individual information items leads to a uniform system in different retrieval situations for the identification of answers in response to incoming information requests.
1979-01-01T00:00:00ZSorting and Searching Using Controlled Density ArraysMelville, Robert C.Gries, Davidhttp://hdl.handle.net/1813/74792015-07-08T00:30:49Z1978-12-01T00:00:00ZSorting and Searching Using Controlled Density Arrays
Melville, Robert C.; Gries, David
Algorithms like insertion sort run slowly because of costly shifting of array elements when a value is inserted or deleted. The amount of shifting, however, can be reduced by leaving gaps - unused array locations into which new values can be inserted - at regular intervals in the array. The proper arrangement of gaps is maintained by periodic adjustment. We demonstrate this technique with a stable comparison sort algorithm with expected time $O(N \log N)$, worst case time $O(N \sqrt{N})$, and space requirements 2N. We conjecture that, by using an interpolation search, the expected time can be reduced to $O(N \log \log N)$. By comparison, Quicksort takes expected time $O(N \log N)$, worst case time $O(N^{2})$ and space $N + \log N$. Second, we show that for any fixed $d \geq 2$ a table management algorithm can be constructed that can process a sequence of $N$ instructions chosen from among INSERT, DELETE, SEARCH, and, MIN in worst case time $O(N^{1+1/d})$. Experiments with a version of the algorithms using $d=2$ show a marked improvement over balanced tree schemes for $N$ as large as several thousand.
1978-12-01T00:00:00ZAn Axiomatic Approach to Information Flow in Parallel ProgramsAndrews, Gregory R.Reitman, Richard P.http://hdl.handle.net/1813/74782015-07-07T23:59:09Z1978-12-01T00:00:00ZAn Axiomatic Approach to Information Flow in Parallel Programs
Andrews, Gregory R.; Reitman, Richard P.
This paper presents a new, axiomatic approach to information flow in sequential and parallel programs. Flow axioms that capture the information flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by a variety of examples. The applications of flow proofs to certifying information flow policies and solving the confinement problem are considered. It is also shown that flow axioms and correctness axioms can be combined to form an even more powerful proof system. Keywords and Phrases: information flow, information security, security certification, parallel programs, axiomatic logic, proof rules.
1978-12-01T00:00:00ZSynchronizing ResourcesAndrews, Gregory R.http://hdl.handle.net/1813/74772015-07-08T00:29:22Z1978-12-01T00:00:00ZSynchronizing Resources
Andrews, Gregory R.
A new proposal for synchronization and communication in parallel programs is presented. The proposal, called synchronization resources, combines and extends aspects of procedures, coroutines, monitors, communicating sequential processes, and distributed processes. It provides a single notation for parallel programming with or without shared variables and is suited for either shared or distributed memory architectures. The essential new concepts are operations, input statements, multiple processes and resources. The proposal is illustrated by solving a variety of parallel programming problems. Key Words and Phrases: parallel programming, processes, synchronization, process communication, monitors, distributed processing, programming languages, operating systems, data bases. CR Categories: 4.20, 4.22, 4.32, 4.35
1978-12-01T00:00:00ZThe Logic of AliasingCartwright, RobertOppen, Derekhttp://hdl.handle.net/1813/74762015-07-08T01:37:36Z1978-11-01T00:00:00ZThe Logic of Aliasing
Cartwright, Robert; Oppen, Derek
We give a new version of Hoare's logic which correctly handles programs with aliased variables. The central proof rules of the logic (procedure call and assignment) are proved sound and complete.
1978-11-01T00:00:00Z