Computer Sciencehttps://hdl.handle.net/1813/5172020-05-31T10:11:16Z2020-05-31T10:11:16ZOne-way Functions Exist iff Kt-Complexity is Hard-on-Averagehttps://hdl.handle.net/1813/697082020-03-28T07:04:34Z2020-03-27T00:00:00ZOne-way Functions Exist iff Kt-Complexity is Hard-on-Average
2020-03-27T00:00:00ZRIF: Reactive Information Flow LabelsKozyri, ElisavetSchneider, Fred B.https://hdl.handle.net/1813/65012.22020-02-20T08:10:47Z2019-04-08T00:00:00ZRIF: Reactive Information Flow Labels
Kozyri, Elisavet; Schneider, Fred B.
Restrictions that a reactive information flow (RIF) label imposes on a value are determined by the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as a fitting security policy, because noninterference is not suitable. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: RIF automata are general-purpose and based on finite-state automata; κ-labels concern confidentiality in programs that use cryptographic operations.
2019-04-08T00:00:00ZUsing Information Flow to Design an ISA that Controls Timing ChannelsZagieboylo, DrewSuh, Gookwon EdwardMyers, Andrew C.https://hdl.handle.net/1813/664882019-06-18T07:10:50Z2019-01-01T00:00:00ZUsing Information Flow to Design an ISA that Controls Timing Channels
Zagieboylo, Drew; Suh, Gookwon Edward; Myers, Andrew C.
Information-flow control (IFC) enforcing languages
can provide high assurance that software does not leak information or allow an attacker to influence critical systems. IFC
hardware description languages have also been used to design
secure circuits that eliminate timing channels. However, there
remains a gap between IFC hardware and software; these two
components are built independently with no abstraction for how
to compose their security guarantees. This paper presents a
proposal for an instruction set architecture (ISA) that can provide
the appropriate abstraction for joining hardware and software
IFC mechanisms. Our ISA describes a RISC-V processor that
tracks information-flow labels at run time and uses these labels
to eliminate or mitigate timing channels. To make the ISA more
practical, it allows constrained downgrading of information; it
permits trading off security for performance; and still offers
control primitives such as system calls. We prove timing-sensitive
noninterference modulo downgrading and nonmalleability for
programs executing our ISA. This involves novel restrictions on
the mutability of labels beyond previous dynamic IFC systems.
Furthermore, we define specific security conditions which correct
hardware can implement to provide software-level security and
sketch how such hardware may be designed and verified.
2019-01-01T00:00:00ZBeyond Labels: Permissiveness for Dynamic Information Flow EnforcementKozyri, ElisavetSchneider, Fred B.Bedford, AndrewDesharnais, JoséeTawbi, Nadiahttps://hdl.handle.net/1813/64488.22019-05-10T07:10:30Z2019-02-28T00:00:00ZBeyond Labels: Permissiveness for Dynamic Information Flow Enforcement
Kozyri, Elisavet; Schneider, Fred B.; Bedford, Andrew; Desharnais, Josée; Tawbi, Nadia
Flow-sensitive labels used by dynamic enforcement mechanisms might themselves encode sensitive information, which can leak. Metalabels, employed to represent the sensitivity of labels, exhibit the same problem. This paper derives a new family of enforcers k-Enf , for k>1 that uses label chains, where each label defines the sensitivity of its predecessor. These enforcers satisfy Block-safe Noninterference (BNI), which proscribes leaks from observing variables, label chains, and blocked executions. Theorems in this paper characterize where longer label chains can improve the permissiveness of dynamic enforcement mechanisms that satisfy BNI. These theorems depend on semantic attributes---k-precise, k-varying, and k-dependent---of such mechanisms, as well as on initialization, threat model, and lattice size.
2019-02-28T00:00:00ZX-Containers: Breaking Down Barriers to Improve Performance and Isolation of Cloud-Native ContainersShen, ZhimingSun, ZhenSela, Gur-EyalBagdasaryan, EugeneDelimitrou, ChristinaVan Renesse, RobbertWeatherspoon, Hakimhttps://hdl.handle.net/1813/586622019-06-18T06:00:46Z2018-08-29T00:00:00ZX-Containers: Breaking Down Barriers to Improve Performance and Isolation of Cloud-Native Containers
Shen, Zhiming; Sun, Zhen; Sela, Gur-Eyal; Bagdasaryan, Eugene; Delimitrou, Christina; Van Renesse, Robbert; Weatherspoon, Hakim
“Cloud-native” container platforms, such as Kubernetes, have become an integral part of production cloud environments. One of the principles in designing cloud-native applications is called “Single Concern Principle”, which suggests that each container should handle a single responsibility well. Due to the resulting change in the threat model, process isolation within the container becomes redundant in most single-concerned containers, and inter-container isolation becomes increasingly important. In this paper, we propose a new exokernel-inspired architecture called X-Containers that improves both the security and the performance of cloud-native containers. We show that, through relatively minor modifications, the Xen hypervisor can serve as an exokernel, and Linux can be turned into a LibOS. Doing so results in a highly secure and efficient LibOS platform that, unlike other available LibOSes, supports binary compatibility and multicore processing. X-Containers have up to 27× higher raw system call throughput compared to Docker containers, while also significantly outperforming recent container platforms such as Google’s gVisor, Intel’s Clear Containers, as well as Library OSes like Unikernel and Graphene on web benchmarks.
2018-08-29T00:00:00ZSecurity Results for SIRRTL, A Hardware Description Language for Information Flow SecurityFerraiuolo, Andrewhttps://hdl.handle.net/1813/576732018-12-12T18:15:51Z2017-12-01T00:00:00ZSecurity Results for SIRRTL, A Hardware Description Language for Information Flow Security
Ferraiuolo, Andrew
This document establishes security results for SIRRTL, a secure variant of the
FIRRTL intermediate language. We developed ChiselFlow, a variant of the Chisel
hardware design language [1] for information flow security. ChiselFlow extends
Chisel, a hardware description language embedded in Scala. ChiselFlow allows
the hardeware designer to describe security policies about the hardware that are
checked at design-time. Much like Chisel, ChiselFlow gains much of the expressive
power of the rich host language, Scala. However, security enforcement is done
by a small intermediate language called SIRRTL, so the trusted component of ChiselFlow
is small. ChiselFlow emits SIRRTL, a variant of the FIRRTL intermediate
language augmented with an information flow type system. ChiselFlow supports
security policies that depend on the run-time values of signals, though these policies
are checked purely at design-time by SIRRTL. In this document, we prove that
well-typed SIRRTL modules enforce a timing safe variant of noninterference. We
constructed the HyperFlow processor using ChiselFlow thereby establishing high
assurance in the implementation of the processor.
2017-12-01T00:00:00ZHyperFlow: A Processor Architecture for Timing-Safe Information-Flow SecurityFerraiuolo, AndrewZhao, YuqiSuh, G. EdwardMyers, Andrew C.https://hdl.handle.net/1813/570202018-12-12T19:23:51Z2018-05-01T00:00:00ZHyperFlow: A Processor Architecture for Timing-Safe Information-Flow Security
Ferraiuolo, Andrew; Zhao, Yuqi; Suh, G. Edward; Myers, Andrew C.
This paper presents HyperFlow, a processor that
enforces secure information flow, including control over timing
channels. The design and implementation of HyperFlow offer security
assurance because it is implemented using a security-typed
hardware description language that enforces secure information
flow. Unlike prior information-flow secured processors that aim
to strictly enforce noninterference, HyperFlow supports complex
information flow policies that can be configured at run time, and
provides support for secure interprocess communication (IPC)
and system calls. The architecture also offers a new model for
process isolation in which memory protection is provided via
information flow control with strong security assurance while
allowing IPC and shared memory. HyperFlow is designed to support
practical applications and system architectures. It therefore
supports decentralized information flow mechanisms that allow
controlled communication among mutually distrusting processes,
mediated by dynamic, fine-grained labels. Static information-
flow verification of such a complex processor architecture poses
significant challenges, which require contributions in both the
hardware architecture and the security type system. The paper
discusses the architecture decisions that make the processor
secure and describes a new secure HDL, named ChiselFlow, that
allows these decisions to be verified in a lightweight way. The
HyperFlow architecture is also prototyped on a fully-featured
processor that offers a complete RISC-V instruction set, and is
shown to have moderate overhead on area and performance.
2018-05-01T00:00:00ZUndecidable Problems for Probabilistic Network ProgrammingKahn, Davidhttps://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, Owenhttps://hdl.handle.net/1813/461982018-12-12T18:17:00Z2017-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. Edwardhttps://hdl.handle.net/1813/458982019-02-08T16:57:30Z2017-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, Dexterhttps://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.https://hdl.handle.net/1813/424062019-08-20T19:33:03Z2016-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, Nadiahttps://hdl.handle.net/1813/445642018-12-12T19:14:51Z2016-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:00Z00_A Directory of the Oral Histories of Computer Science at Cornell UniversityCooke, J. Roberthttps://hdl.handle.net/1813/442012016-06-17T05:02:48Z2016-06-16T00:00:00Z00_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 JavaKozyri, ElisavetArden, OwenMyers, Andrew C.Schneider, Fred B.https://hdl.handle.net/1813/411942018-12-12T19:20:25Z2016-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:00ZA Conversation with Fred SchneiderSchneider, Fred B.Gries, Davidhttps://hdl.handle.net/1813/413702016-06-16T15:41:15Z2015-09-09T00:00:00ZA 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 CardieCardie, ClaireConstable, Robert L.https://hdl.handle.net/1813/412162016-06-16T15:35:36Z2015-09-09T00:00:00ZA 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 BirmanBirman, KenVan Renesse, Robberthttps://hdl.handle.net/1813/412072016-06-16T15:32:23Z2015-09-10T00:00:00ZA 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 KozenKozen, DexterConstable, Robert L.https://hdl.handle.net/1813/412062016-06-16T15:39:48Z2015-09-09T00:00:00ZA 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 LoanVan Loan, CharlieBala, Kavitahttps://hdl.handle.net/1813/412012016-06-16T15:43:13Z2015-09-15T00:00:00ZA 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 TeitelbaumTeitelbaum, TimGries, Davidhttps://hdl.handle.net/1813/408652016-06-16T15:42:35Z2015-09-10T00:00:00ZA 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 GriesGries, DavidConstable, Robert L.https://hdl.handle.net/1813/405762016-06-16T15:37:40Z2015-07-21T00:00:00ZA 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. HopcroftHopcroft, John E.Gries, Davidhttps://hdl.handle.net/1813/405682016-06-16T15:39:11Z2015-07-21T00:00:00ZA 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. ConwayConway, Richard W.Gries, Davidhttps://hdl.handle.net/1813/405642016-06-16T15:37:02Z2015-07-21T00:00:00ZA 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. ConstableConstable, Robert L.Gries, Davidhttps://hdl.handle.net/1813/405602016-06-16T15:36:20Z2015-07-21T00:00:00ZA 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 NerodeNerode, AnilGries, Davidhttps://hdl.handle.net/1813/405272016-06-16T15:40:36Z2014-10-16T00:00:00ZA 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 AuthorizationArden, OwenLiu, JedMyers, Andrewhttps://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 Conversation with Juris HartmanisHartmanis, Jurishttps://hdl.handle.net/1813/149342016-06-16T15:38:32Z2010-03-31T00:00:00ZA 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 AlgorithmHopcroft, John E.Ullman, Jeffrey D.https://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, Erikhttps://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, Davidhttps://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 Marchttps://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, Danielhttps://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.https://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.https://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, Marcellohttps://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.https://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.https://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.https://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.https://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.https://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, Danielhttps://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 Louishttps://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.https://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.https://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.https://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.https://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.https://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 Elainehttps://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, Timhttps://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, Danielhttps://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 Marchttps://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, Alhttps://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, Charleshttps://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, Charleshttps://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, Jorgenhttps://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.https://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, Sethhttps://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, Timhttps://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, Jorgenhttps://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, Gerardhttps://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.https://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.https://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.https://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.https://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, Gerardhttps://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, Davidhttps://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.https://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.https://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, Derekhttps://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:00ZA Survey of Graduate Programs in Computer ScienceConway, Richard W.https://hdl.handle.net/1813/74752015-07-07T23:39:26Z1978-11-01T00:00:00ZA Survey of Graduate Programs in Computer Science
Conway, Richard W.
NO ABSTRACT SUPPLIED
1978-11-01T00:00:00ZClasses and Objects - A Dynamic ApproachSteensgaard-Madsen, Jorgenhttps://hdl.handle.net/1813/74742015-07-08T00:50:50Z1978-11-01T00:00:00ZClasses and Objects - A Dynamic Approach
Steensgaard-Madsen, Jorgen
Data encapsulation, abstract data types and classes are terms associated with a concept not fully clarified or accepted. This paper presents a class concept that differs slightly from previous definitions by the associated dynamics. This allows us to interpret nested and recursive classes as well as class parameters. We will distinguish between types and classes and permit types as parameters in a way that allows simple implementation. A number of examples will be given to illustrate the class concept itself and its application to access control problems for concurrent programs. Synchronization primitives will be viewed as classes and the need for explicit high-level constructs like monitors is questioned. Keywords: Programming language, encapsulation, abstract data type, class, object, synchronization, monitor.
1978-11-01T00:00:00ZA Note on the Sparse Complete SetsFortune, Stevenhttps://hdl.handle.net/1813/74732015-07-08T00:12:56Z1978-10-01T00:00:00ZA Note on the Sparse Complete Sets
Fortune, Steven
Hartmanis and Berman have conjectured that all NP-complete sets are polynomial time isomorphic. A consequence of the conjecture is that there are no sparse NP-complete sets. We show that the existence of an NP-complete set whose complement is sparse implies P = NP. We also show that if there is a polynomial time reduction with sparse range to a PTAPE-complete set, then P=PTAPE. Keywords: reduction, polynomial time, nondeterministic polynomial time, complete sets, sparsity.
1978-10-01T00:00:00ZA Hessenberg-Schur Method for the Problem AX + XB = CGolub, Gene H.Nash, StephenVan Loan, Charleshttps://hdl.handle.net/1813/74722015-07-07T23:41:03Z1978-10-01T00:00:00ZA Hessenberg-Schur Method for the Problem AX + XB = C
Golub, Gene H.; Nash, Stephen; Van Loan, Charles
ONe of the most effective methods for solving the matrix equation AX + XB = C is the Bartels-Stewart algorithm. Key to this technique is the orthogonal reduction of A and B to triangular form using the QR algorithm for eigenvalues. A new method is proposed which differs from the Bartels-Stewart algorithm in that A is only reduced to Hessenberg form. The resulting algorithm is between 30 and 70 percent faster depending upon the dimensions of the matrices A and B. The stability of the new method is demonstrated through a roundoff error analysis and supported by numerical tests. Fianlly, it is shown how the techniques described can be applied and generalized to other matrix equation problems.
1978-10-01T00:00:00ZA Note on the Evaluation of Matrix PolynomialsVan Loan, Charleshttps://hdl.handle.net/1813/74712015-07-07T22:34:13Z1978-09-01T00:00:00ZA Note on the Evaluation of Matrix Polynomials
Van Loan, Charles
The problem of evaluating a polynomial p(x) in a matrix A arises in many applications, e.g. the Taylor approximation of $e^{A}$. The $O(\sqrt{q}n^{3})$ algorithm of Paterson and Stockmeyer has the drawback that it requires $O(\sqrt{q}n^{2})$ storage, where $q$ is the degree of $p$ and $n$ is the dimension of $A$. An algorithm which greatly reduces this storage requirement without undue loss of speed is presented.
1978-09-01T00:00:00ZUnsymmetric Positive Definite Linear SystemsGolub, Gene H.Van Loan, Charleshttps://hdl.handle.net/1813/74702015-07-07T22:51:44Z1978-09-01T00:00:00ZUnsymmetric Positive Definite Linear Systems
Golub, Gene H.; Van Loan, Charles
Is it necessary to pivot when solving an unsymmetric positive definite linear system $Ax = b?$ Define $T = (A + A^{T})/2$ and $S=(A+AA^{T})/2$. It is shown that pivoting is unnecessary if the quantitity is $\Vert S T^{-1} S \Vert_{2}/ \Vert A \Vert_{2}$ is suitably small with respect to the working machine precision.
1978-09-01T00:00:00ZAn Efficient Algorithm for Testing Losslessness of Joins in Relational Data BasesLiu, LishingDemers, Alan J.https://hdl.handle.net/1813/74692015-07-08T01:03:31Z1978-09-01T00:00:00ZAn Efficient Algorithm for Testing Losslessness of Joins in Relational Data Bases
Liu, Lishing; Demers, Alan J.
Answering queries in a relational database model often requires the computation of joins of relations. Losslessness of joins is an important property for joins of relations to be semantically meaningful. In this paper we present an $O(n^{3})$ algorithm for testing losslessness of joins in relational databases with functional dependencies, which improves the $O(n^{4})$ result by Aho, Beeri and Ullman.
1978-09-01T00:00:00ZInformation Flow in Parallel Programs: An Axiomatic ApproachReitman, Richard P.https://hdl.handle.net/1813/74682015-07-08T00:08:48Z1978-08-01T00:00:00ZInformation Flow in Parallel Programs: An Axiomatic Approach
Reitman, Richard P.
The information flow problem is concerned with controlling the transmission of information in computer systems. This thesis addresses this problem by developing an axiomatic logic that captures the information flow semantics of a program. Using this technique the scope of information flow analysis is extended from terminating sequential programs to parallel programs in which non-termination, synchronization and deadlock are possible. Once the information flow generated by a program has been determined, it is easy to check whether or not the program satisfies a given security policy. The main contribution of the thesis is an axiomatic proof system for determining the flow of information produced by sequential or parallel programs. Just as proofs of correctness capture the effect of program execution upon the values in variables, proofs of information flow capture the effect of program execution upon the information in variables. An advantage of this approach is that once a flow proof of a program has been generated, various security policies, such as high water mark or final value, can be verified readily. Although flows in parallel programs need to be determined so that confidentiality in shared systems can be maintained, current information flow techniques are limited to terminating sequential programs. The thesis addresses this problem by capturing the flows generated by programs containing independent processes that synchronize with each other. The practicability of the method is demonstrated by developing the flow semantics for Concurrent Pascal.
1978-08-01T00:00:00ZRelative Succinctness of Representations of Languages and Separation of Complexity ClassesHartmanis, Jurishttps://hdl.handle.net/1813/74672015-07-07T22:45:23Z1978-08-01T00:00:00ZRelative Succinctness of Representations of Languages and Separation of Complexity Classes
Hartmanis, Juris
In this paper we study the relative succinctness of different representations of polymomial time languages and investigate what can and cannot be formally verified about these representations. We also show that the relative succintness of different representations of languages is directly related to the separation of the corresponding complexity classes; for example, PTIME $\neq$ NPTIME if and only if the relative succintness of representing languages in PTIME by deterministic and nondeterministic clocked polynomial time machines is not recursively bound which happens if and only if the relative succintness of these representations is not linearly bounded.
1978-08-01T00:00:00ZAn Improved Simulation Result for Ink Bounded Turing MachinesMelville, Robert C.https://hdl.handle.net/1813/74662015-07-08T00:55:58Z1978-08-01T00:00:00ZAn Improved Simulation Result for Ink Bounded Turing Machines
Melville, Robert C.
A (one tape, deterministic) Turing machine is $f(n)$ ink bounded if the machine changes a symbol of its work tape at most $O(f(n))$ times while processing any input of length $n$. The main result of our paper is the construction of an "ink efficient" universal machine which, for any $f(n)$ ink bounded machine $M$ and input $x$, can simulate the processing of $M$ on $x$ or detect that $M$ is looping infinitely on input $x$. The universal machine requires $O(f(n)^{1+\epsilon)$ ink for this simulation where $\epsilon$ is an arbitrarily small positive number. As a corollary, we establish that the class of all $f(n)$ ink bounded computations is properly contained in the class of all $g(n)$ ink bounded computations assuming $\stackrel{inf}{n \rightarrow \infty} \frac{f(n)^{1+\varepsilon}}{g(n)} = 0$ and a technical condition on g.
1978-08-01T00:00:00ZOne-Way Log-Tape ReductionsHartmanis, JurisImmerman, NeilMahaney, Stephen R.https://hdl.handle.net/1813/74652015-07-07T23:13:15Z1978-07-01T00:00:00ZOne-Way Log-Tape Reductions
Hartmanis, Juris; Immerman, Neil; Mahaney, Stephen R.
One-way log-tape (1-L) reductions are mappings defined by log-tape Turing machines whose read head on the input can only move to the right. The 1-L reductions provide a more refined tool for studying the feasible complexity classes than the P-time [2,7] or log-tape [4] reductions. Although the 1-L computations are provably weaker than the feasible classes L, NL, P and NP, the known complete sets for those classes are complete under 1-L reductions. However, using known techniques of counting arguments and recursion theory we show that certain log-tape reductions cannot be 1-L and we construct sets that are complete under log-tape reductions but not under 1-L reductions.
1978-07-01T00:00:00ZOn the Succintness of Different Representations of LanguagesHartmanis, Jurishttps://hdl.handle.net/1813/74642015-07-08T00:46:10Z1978-06-01T00:00:00ZOn the Succintness of Different Representations of Languages
Hartmanis, Juris
The purpose of this paper is to give simple new proofs of some interesting recent results about the relative succintness of different representations of regular, deterministic and unambiguous context-free languages and to derive some new results about how the relative succintness of representations change when the representations contain a formal proof that the languages generated are in the desired subclass of languages.
1978-06-01T00:00:00ZLeast Change Secant Updates for Quasi-Newton MethodsDennis, John E., Jr.Schnabel, Robert B.https://hdl.handle.net/1813/74632015-07-08T00:08:51Z1978-06-01T00:00:00ZLeast Change Secant Updates for Quasi-Newton Methods
Dennis, John E., Jr.; Schnabel, Robert B.
In many problems involving the solution of a system of nonlinear equations, it is necessary to keep an approximation to the Jacobian matrix which is updated at each iteration. Computational experience indicates that the best updates are those that minimize some reasonable measure of the change to the current Jacobian approximation subject to the new approximation obeying a secant condition and perhaps some other approximation properties such as symmetry. In this paper we extend the affine case of a theorem of Cheney and Goldstein on proximity maps of convex sets to show that a generalization of the symmetrization technique of Powell always generates least change updates. This generalization has such broad applicability that we obtain an easy unified derivation of all the most successful updates. Furthermore, our techniques apply to interesting new cases such as when the secant condition might be inconsistent with some essential approximation property like sparsity. We also offer advice on how to choose the properties which are to be incorporated into the approximations and how to choose the measure of changes to be minimized.
1978-06-01T00:00:00ZIs Sometimes Ever Better Than Always?Gries, Davidhttps://hdl.handle.net/1813/74622015-07-07T23:41:01Z1978-06-01T00:00:00ZIs Sometimes Ever Better Than Always?
Gries, David
The "intermittent assertion" method for proving programs correct is explained and compared to the conventional axiomatic method. Simple axiomatic proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given. A critical examination of the two methods leads to the opinion that the axiomatic method is preferable.
1978-06-01T00:00:00ZSolution of Definite Quadratic Programming ProblemsShubert, Gregory Donaldhttps://hdl.handle.net/1813/74612015-07-07T23:04:13Z1978-05-01T00:00:00ZSolution of Definite Quadratic Programming Problems
Shubert, Gregory Donald
A algorithm for solving the definite quadratic programming problem is presented. An implementation of this algorithm in FORTRAN is discussed. Numerical tests of this algorithm and a similar one not using the positive definiteness property show the former to be more stable. This algorithm is paarticularly suited for numerical methods for solving general nonlinear programming problems or minimax problems.
1978-05-01T00:00:00ZA Note on Rabin's Nearest-Neighbor AlgorithmFortune, StevenHopcroft, John E.https://hdl.handle.net/1813/74602015-07-07T22:53:54Z1978-04-01T00:00:00ZA Note on Rabin's Nearest-Neighbor Algorithm
Fortune, Steven; Hopcroft, John E.
Rabin has proposed a probabilistic algorithm for finding the closest pair of a set of points in Euclidean space. His algorithm is asymtomatically linear whereas the best of the known deterministic algorithms take order $n \log n$ time. We show that at least part of the speed up is due to the model rather than the probabilistic nature of the algorithm.
1978-04-01T00:00:00ZFirst Order Semantics: A Natural Programming Logic for Recursively Defined FunctionsCartwright, Roberthttps://hdl.handle.net/1813/74592015-07-08T00:55:49Z1978-04-01T00:00:00ZFirst Order Semantics: A Natural Programming Logic for Recursively Defined Functions
Cartwright, Robert
NO ABSTRACT SUPPLIED
1978-04-01T00:00:00ZA Note on Cryptography and NP$\cap$ CoNP-PBrassard, GilesFortune, StevenHopcroft, John E.https://hdl.handle.net/1813/74582015-07-07T22:31:59Z1978-04-01T00:00:00ZA Note on Cryptography and NP$\cap$ CoNP-P
Brassard, Giles; Fortune, Steven; Hopcroft, John E.
Diffie and Hellman [2] propose the use of the exponential function in a finite field for cryptographic purposes. The proposal is based on the conjecture that the inverse function, the logarithm, is not feasibly computable. We show that a proof of this conjecture would have important consequences for theoretical computer science, even under the assumption that P $neq$ NP.
1978-04-01T00:00:00ZThe Assertion Table System for the PL/CV2 Program VerifierKrafft, Dean B.https://hdl.handle.net/1813/74572015-07-07T23:53:53Z1978-04-01T00:00:00ZThe Assertion Table System for the PL/CV2 Program Verifier
Krafft, Dean B.
A system to implement the block structured storage of PL/CV2 assertions is described. The system allows certain simple logical deductions to be performed automatically. These include deductions involving propositional reasoning, associativity and commutativity of arithmetic operators, and reasoning about equality. The implementation is described at a conceptual level.
1978-04-01T00:00:00ZSuperlinear Convergence of a Minimax MethodHan, Shih-Pinghttps://hdl.handle.net/1813/74562015-07-07T22:43:25Z1978-02-01T00:00:00ZSuperlinear Convergence of a Minimax Method
Han, Shih-Ping
To solve a minimax problem Han [1977b] suggested the use of quadratic programs to find search directions. If the matrices in the quadratic programs are positive definite, the method can be shown convergent globally. In this paper we study that for efficiency the matrices should also be good approximations to a certain convex combination of Hessians on some subspace. Therefore, we suggest Powell's scheme [Powell 1977] for updating these matrices. By doing so, we can avoid computing Hessians. Meanwhile, the matrices maintain positive definiteness and Han's global convergence theorems can apply. Besides, the convergence of the resulting method is superlinear, indeed.
1978-02-01T00:00:00ZExploiting Sparsity in Newtown-Like MethodsMarwil, Earl S.https://hdl.handle.net/1813/74552015-07-07T22:58:48Z1978-02-01T00:00:00ZExploiting Sparsity in Newtown-Like Methods
Marwil, Earl S.
The basic problem considered here is to solve sparse systems of nonlinear equations. A system is considered to be sparse when the Jacobian has fewer than ten percent nonzero entries. Algorithms are presented and their convergence properties are analyzed. Schubert's method for solving sparse nonlinear equations is a modification of Broyden's method, a well known quasi-Newton method. The modification preserves the zero-nonzero structure defined by the sparse Jacobian in the sequence of approximate Jacobians. The algorithm is shown to satisfy the Bounded Deterioration Theorem of Broyden, Dennis and More to obtain a simple local convergence result. A more detailed study of the error bound in the Frobenfus norm shows that the method is superlinearly convergent. Schubert's method satisfies a minimum norm property and a Kantorovich analysis is also presented. A symmetric Schubert update is derived using an iterative projection technique of Dennis and Powell. The update is expressed in a closed form at the expense of an additional sparse linear system to be solved at each iteration in the algorithm. These sparse linear systems that occur all have the same structure which means they can be handled using the pre-processing performed when solving the first such system. Again the Frobenfus norm is used to estimate the error in the approximate Jacobian. The algorithm is locally and linearly convergent. The update is applicable to a symmetric nonlinear system, particularly those systems arising from unconstrained minimization problems with a continuous second derivative. Another method of solving sparse nonlinear equations using a matrix factorization is presented. Some theory of sparse linear equations is needed to maintain sparseness in triangular factors of a matrix. An approximate Jacobian is factored and one of the triangular factors is updated with Schubert's updating formula. After a finite number of iterations, a new approximate Jacobian is needed. Algorithms are suggested with local and superlinear convergence properties. The convergence depends on the local continuity of the matrix factorization. Finally, another application of Schubert's method is proposed for problems in which the Jacobian of the nonlinear system can be written as the direct sum of two transformations. One of these is assumed to be easily computed, and the other is assumed to be sparse. An algorithm is sketched and local and superlinear convergence properties are conjectured.
1978-02-01T00:00:00ZParallelism in Random Access MachinesFortune, StevenWyllie, James C.https://hdl.handle.net/1813/74542015-07-07T23:34:12Z1978-01-01T00:00:00ZParallelism in Random Access Machines
Fortune, Steven; Wyllie, James C.
A model of computation based on random access machines operating in parallel and sharing a common memory is presented. The computational power of this model is related to that of traditional models. In particular, deterministic parallel RAM's can accept in polynomial time exactly the sets accepted by polynomial tape bounded Turing machines; nondeterministic RAM's can accept in polynomial time exactly the sets accepted by nondeterministic exponential time bounded Turing machines. Similar results hold for other classes. The effect of limiting the size of the common memory is also considered.
1978-01-01T00:00:00ZLanguage Based Protection MechanismsEland, Nancyhttps://hdl.handle.net/1813/74532015-07-08T00:43:49Z1978-01-01T00:00:00ZLanguage Based Protection Mechanisms
Eland, Nancy
NO ABSTRACT SUPPLIED
1978-01-01T00:00:00ZMathematics and Information RetrievalSalton, Gerardhttps://hdl.handle.net/1813/74522015-07-07T23:15:43Z1978-01-01T00:00:00ZMathematics and Information Retrieval
Salton, Gerard
The development of a given discipline in science and technology often depends on the availability of theories capable of describing the processes which control the field and of modelling the interactions between these processes. The absence of an accepted theory of information retrieval has been blamed for the relative disorder and the lack of technical advances in the area. The main mathematical approaches to information retrieval are examined in this study, including both algebraic and probabilistic models, and the difficulties which impede the formalization of information retrieval processes are described. A number of developments are covered where new theoretical understandings have directly led to the improvement of retrieval techniques and operations.
1978-01-01T00:00:00ZThe Design of Parallel Systems: An Application and Evaluation of ModulaAndrews, Gregory R.https://hdl.handle.net/1813/74512015-07-07T23:37:42Z1978-01-01T00:00:00ZThe Design of Parallel Systems: An Application and Evaluation of Modula
Andrews, Gregory R.
Modula is a new programming language for implementing dedicated, parallel systems. Following a systematic design technique, this paper illustrates the use of Modula for the design of a message switching communication system. A message switching system poses a number of interesting problems: a high degree of concurrent activity exists, a variety of IO devices need to be controlled, messages can have multiple destinations, and messages can be preempted. The strengths and weaknesses of Modula with respect to these specific problems and its utility as a general purpose language are evaluated. Key Words and Phrases: structured multiprogramming, concurrent systems, Modula, message switching, software design, processes, monitors, modular design. CR Categories: 3.81, 4.2, 4.21, 4.3
1978-01-01T00:00:00ZModula and the Design of a Message Switching Communication SystemAndrews, Gregory R.https://hdl.handle.net/1813/74502015-07-07T23:53:21Z1978-01-01T00:00:00ZModula and the Design of a Message Switching Communication System
Andrews, Gregory R.
This report describes the functions of a message switching communications system and presents an implementation in terms of the Modula programming language. In particular, the report: (1) describes a representative application of the proposed new Department of Defense high order language; (2) presents a design technique for software specification; (3) develops Modula programs for each of the message switching components; and (4) evaluates the utility of Modula as a language for the design of large parallel systems.
1978-01-01T00:00:00ZAccess Control in Parallel ProgramsMcGraw, James R.Andrews, Gregory R.https://hdl.handle.net/1813/74492015-07-08T00:04:50Z1978-01-01T00:00:00ZAccess Control in Parallel Programs
McGraw, James R.; Andrews, Gregory R.
An important component of a programming language for writing operating systems, or other large parallel systems, is the set of access control facilities. Two principles for access control, expressive power and access validation, are discussed. Then two new language mechanisms are presented: one for expressing the static structure and access rights of parallel systems, the other for controlling dynamic access to shared objects (monitors). The use of the proposed mechanisms is illustrated by message passing and file systems. Finally, the relationship between the mechanisms and access validation is discussed and a solution to the safety problem for the facilities is given. Key Words and Phrases: access control, programming language, protection, security, processes, monitors, access safety. CR Categories: 4.20, 4.32, 4.35
1978-01-01T00:00:00ZA Brief Introduction to Quasi-Newton MethodsDennis, John E., Jr.https://hdl.handle.net/1813/74482015-07-07T23:39:51Z1977-11-01T00:00:00ZA Brief Introduction to Quasi-Newton Methods
Dennis, John E., Jr.
NO ABSTRACT SUPPLIED
1977-11-01T00:00:00ZAn Algorithm for Checking PL/CV Arithmetic InferencesChan, Tat-hunghttps://hdl.handle.net/1813/74472015-07-07T23:47:08Z1977-10-01T00:00:00ZAn Algorithm for Checking PL/CV Arithmetic Inferences
Chan, Tat-hung
This paper describes the operation and implementation of the arithmetic proof rule for the quantifier free integer arithmetic used in the PL/CV 2 program verification system. The general arithmetic satisfiability problem underlying the rule is shown to be NP complete.
1977-10-01T00:00:00ZStatic Restriction of the GOTO StatementBishop, T.Bodenstein, M.Conway, Richard W.https://hdl.handle.net/1813/74462015-07-08T00:46:47Z1977-10-01T00:00:00ZStatic Restriction of the GOTO Statement
Bishop, T.; Bodenstein, M.; Conway, Richard W.
NO ABSTRACT SUPPLIED
1977-10-01T00:00:00Z