SearchBrowse

close this section of the libraryftp://ftp.cis.ksu.edu (421)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/security.ps.Z, 19921002
1 A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof Masaaki Mizuno* and David Schmidt* Computing and Information Sciences Dept. Kansas State University Manhattan, KS 66506 USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/security.ps.Z, 19921002
1 A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof Masaaki Mizuno* and David Schmidt* Computing and Information Sciences Dept. Kansas State University Manhattan, KS 66506 USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/pods92.ps.Z, 19921014
Real-Time Integrity Constraints (extended abstract) Jan Chomickiy Computing and Information Sciences Kansas State University Manhattan, KS 66506-2302 chomicki@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/pods92.ps.Z, 19921014
Real-Time Integrity Constraints (extended abstract) Jan Chomickiy Computing and Information Sciences Kansas State University Manhattan, KS 66506-2302 chomicki@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/tdd93.ps.Z, 19921014
Temporal Deductive Databases Marianne Baudinet Universit e Libre de Bruxellesy Jan Chomicki Kansas State Universityz Pierre Wolper Universit e de Li egex October 13, 1992 Keywords: query processing, logic programming, temporal logic, constraint logic programming, expressiveness, computational
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/tdd93.ps.Z, 19921014
Temporal Deductive Databases Marianne Baudinet Universit e Libre de Bruxellesy Jan Chomicki Kansas State Universityz Pierre Wolper Universit e de Li egex October 13, 1992 Keywords: query processing, logic programming, temporal logic, constraint logic programming, expressiveness, computational
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/dom93.ps.Z, 19921014
Declarative Definition of Object-Oriented Multidatabase Mappings Jan Chomicki Kansas State Universityy Witold Litwin Universit e de Paris - Dauphinez
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/dom93.ps.Z, 19921014
Declarative Definition of Object-Oriented Multidatabase Mappings Jan Chomicki Kansas State Universityy Witold Litwin Universit e de Paris - Dauphinez
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/tods93.ps.Z, 19921109
Finite Representation of Infinite Query Answers Jan Chomickiy Tomasz Imieli nskiz Kansas State University Rutgers University November 9, 1992 Keywords: query processing, logic programming, Datalog , decidability, safety, computational complexity, non-standard query answers, non-Herbrand models. 1989 CR
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/tods93.ps.Z, 19921109
Finite Representation of Infinite Query Answers Jan Chomickiy Tomasz Imieli nskiz Kansas State University Rutgers University November 9, 1992 Keywords: query processing, logic programming, Datalog , decidability, safety, computational complexity, non-standard query answers, non-Herbrand models. 1989 CR
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr93-3.ps, 19930209
Communication Efficient Distributed Shared Memories Masaaki Mizuno Gurdip Singhy Michel Raynalz Mitchell L. Neilsenx
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr93-4.ps, 19930209
A Sequentially Consistent Distributed Shared Memory James Z. Zhou Masaaki Mizuno Gurdip Singhy Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr93-3.ps, 19930209
Communication Efficient Distributed Shared Memories Masaaki Mizuno Gurdip Singhy Michel Raynalz Mitchell L. Neilsenx
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr93-4.ps, 19930209
A Sequentially Consistent Distributed Shared Memory James Z. Zhou Masaaki Mizuno Gurdip Singhy Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/tr92-34.ps, 19930226
Impact of Synchrony and Topological Information on Leader Election Gurdip Singh Department of Computing and Information Sciences, 234 Nichols Hall, Kansas State University, Manhattan, Kansas 66506 email: singh@cis.ksu.edu KSU Technical Report 92-34
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/tr92-34.ps, 19930226
Impact of Synchrony and Topological Information on Leader Election Gurdip Singh Department of Computing and Information Sciences, 234 Nichols Hall, Kansas State University, Manhattan, Kansas 66506 email: singh@cis.ksu.edu KSU Technical Report 92-34
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/tr93-35.ps, 19930226
Efficient Execution of Write-only Transactions Gurdip Singh Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506 singh@cis.ksu.edu Techical Report 92-35
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/tr93-35.ps, 19930226
Efficient Execution of Write-only Transactions Gurdip Singh Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506 singh@cis.ksu.edu Techical Report 92-35
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/pods90.ps.Z, 19930227
Polynomial Time Query Processing in Temporal Deductive Databases Jan Chomicki Department of Computer Science University of North Carolina Chapel Hill, NC 27599 chomicki@cs.unc.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/pods90.ps.Z, 19930227
Polynomial Time Query Processing in Temporal Deductive Databases Jan Chomicki Department of Computer Science University of North Carolina Chapel Hill, NC 27599 chomicki@cs.unc.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/stagingCPS-popl93.ps.Z, 19930301
Separating Stages in the Continuation-Passing Style Transformation Julia L. Lawall Department of Computer Science Indiana University jll@cs.indiana.edu Olivier Danvy Department of Computing and Information Sciences Kansas State University y danvy@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/cps-sa.ps.Z, 19930301
CPS Transformation after Strictness Analysis Olivier Danvy and John Hatcliff Kansas State University Strictness analysis is a common component of compilers for call-by-name functional languages; the continuation-passing-style (CPS) transformation is a common component of compilers for call-byvalue
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/tutorial-PE.ps.Z, 19930301
Partial Evaluation: Principles and Perspectives Charles Consel Pacific Software Research Center Department of Computer Science and Engineering Oregon Graduate Institute of Science & Technology consel@cse.ogi.edu Olivier Danvy School of Computer Science Carnegie Mellon Universityy
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/stagingCPS-popl93.ps.Z, 19930301
Separating Stages in the Continuation-Passing Style Transformation Julia L. Lawall Department of Computer Science Indiana University jll@cs.indiana.edu Olivier Danvy Department of Computing and Information Sciences Kansas State University y danvy@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/rc.ps.Z, 19930301
Representing Control A Study of the CPS transformation Olivier Danvy Kansas State University y (danvy@cis.ksu.edu) Andrzej Filinski Carnegie Mellon University z (Andrzej.Filinski@cs.cmu.edu) February 1991; Revised June 1992
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/rc.ps.Z, 19930301
Representing Control A Study of the CPS transformation Olivier Danvy Kansas State University y (danvy@cis.ksu.edu) Andrzej Filinski Carnegie Mellon University z (Andrzej.Filinski@cs.cmu.edu) February 1991; Revised June 1992
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/thunks-wsa92.ps.Z, 19930301
Thunks (continued) Olivier Danvy, John Hatcliff Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506, USA e-mail: (danvy, hatcliff )@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/thunks-wsa92.ps.Z, 19930301
Thunks (continued) Olivier Danvy, John Hatcliff Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506, USA e-mail: (danvy, hatcliff )@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/tutorial-PE.ps.Z, 19930301
Partial Evaluation: Principles and Perspectives Charles Consel Pacific Software Research Center Department of Computer Science and Engineering Oregon Graduate Institute of Science & Technology consel@cse.ogi.edu Olivier Danvy School of Computer Science Carnegie Mellon Universityy
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/cps-sa.ps.Z, 19930301
CPS Transformation after Strictness Analysis Olivier Danvy and John Hatcliff Kansas State University Strictness analysis is a common component of compilers for call-by-name functional languages; the continuation-passing-style (CPS) transformation is a common component of compilers for call-byvalue
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/conc.ps, 19930304
Extraction of Logical Concurrency in Distributed Applications K. Ravindran && A. Thenmozhi Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/conc.ps, 19930304
Extraction of Logical Concurrency in Distributed Applications K. Ravindran && A. Thenmozhi Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/cmp_eff.ps, 19930308
Structural Complexity and Execution Efficiency of Distributed Application Protocols K. Ravindran && X. T. Lin Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/cmp_eff.ps, 19930308
Structural Complexity and Execution Efficiency of Distributed Application Protocols K. Ravindran && X. T. Lin Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/compiling-monads.ps.Z, 19930725
Compiling Monads Olivier Danvy, J urgen Koslowski, and Karoline Malmkjaer Department of Computing and Information Sciences Kansas State University y (danvy, koslowj, karoline)@cis.ksu.edu December 1991
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/compiling-monads.ps.Z, 19930725
Compiling Monads Olivier Danvy, J urgen Koslowski, and Karoline Malmkjaer Department of Computing and Information Sciences Kansas State University y (danvy, koslowj, karoline)@cis.ksu.edu December 1991
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/corr.ps.Z, 19931012
A Categorical Interpretation of Landin's Correspondence Principle Anindya Banerjee and David A. Schmidt Department of Computing and Information Sciences Kansas State University (banerjee, schmidt)@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/corr.ps.Z, 19931012
A Categorical Interpretation of Landin's Correspondence Principle Anindya Banerjee and David A. Schmidt Department of Computing and Information Sciences Kansas State University (banerjee, schmidt)@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hatcliff/thunks-tr93-15.ps.Z, 19931103
Thunks and the >=-calculus John Hatcliff y (hatcliff@cis.ksu.edu) Olivier Danvy z (danvy@daimi.aau.dk) September 2, 1993
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Danvy/thunks-tr93-15.ps.Z, 19931103
Thunks and the >=-calculus John Hatcliff y (hatcliff@cis.ksu.edu) Olivier Danvy z (danvy@daimi.aau.dk) September 2, 1993
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Danvy/thunks-tr93-15.ps.Z, 19931103
Thunks and the >=-calculus John Hatcliff y (hatcliff@cis.ksu.edu) Olivier Danvy z (danvy@daimi.aau.dk) September 2, 1993
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hatcliff/thunks-tr93-15.ps.Z, 19931103
Thunks and the >=-calculus John Hatcliff y (hatcliff@cis.ksu.edu) Olivier Danvy z (danvy@daimi.aau.dk) September 2, 1993
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hatcliff/mfps93.ps.Z, 19931110
On the Transformation between Direct and Continuation Semantics Olivier Danvy and John Hatcliff Aarhus University and Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hatcliff/mfps93.ps.Z, 19931110
On the Transformation between Direct and Continuation Semantics Olivier Danvy and John Hatcliff Aarhus University and Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hatcliff/thunks-wsa92.ps.Z, 19931110
Thunks (continued) Olivier Danvy, John Hatcliff Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506, USA e-mail: (danvy, hatcliff )@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hatcliff/cps-sa-tr92-31.ps.Z, 19931110
CPS Transformation after Strictness Analysis Olivier Danvy and John Hatcliff Kansas State University Strictness analysis is a common component of compilers for call-by-name functional languages; the continuation-passing-style (CPS) transformation is a common component of compilers for call-byvalue
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hatcliff/thunks-wsa92.ps.Z, 19931110
Thunks (continued) Olivier Danvy, John Hatcliff Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506, USA e-mail: (danvy, hatcliff )@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hatcliff/cps-sa-tr92-31.ps.Z, 19931110
CPS Transformation after Strictness Analysis Olivier Danvy and John Hatcliff Kansas State University Strictness analysis is a common component of compilers for call-by-name functional languages; the continuation-passing-style (CPS) transformation is a common component of compilers for call-byvalue
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/subst.ps.gz, 19940331
Substitution Revisited1 Allen Stoughton Computer Science Subject Group School of Mathematical and Physical Sciences University of Sussex Falmer, Brighton BN1 9QH, England
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/ppcf.ps.gz, 19940331
Parallel PCF has a Unique Extensional Model Allen Stoughton Computer Science and Artificial Intelligence School of Cognitive and Computing Sciences University of Sussex Falmer, Brighton BN1 9QH, England
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/subst.ps.gz, 19940331
Substitution Revisited1 Allen Stoughton Computer Science Subject Group School of Mathematical and Physical Sciences University of Sussex Falmer, Brighton BN1 9QH, England
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/within.ps.gz, 19940331
Studying the Fully Abstract Model of PCF within its Continuous Function Model 1 Achim Jung2 and Allen Stoughton3 Abstract. We give a concrete presentation of the inequationally fully abstract model of PCF as a continuous projection of the inductively reachable subalgebra of PCF's continuous function
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/within.ps.gz, 19940331
Studying the Fully Abstract Model of PCF within its Continuous Function Model 1 Achim Jung2 and Allen Stoughton3 Abstract. We give a concrete presentation of the inequationally fully abstract model of PCF as a continuous projection of the inductively reachable subalgebra of PCF's continuous function
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/efa.ps.gz, 19940331
Equationally Fully Abstract Models of PCF 1 Allen Stoughton Computer Science and Artificial Intelligence School of Cognitive and Computing Sciences University of Sussex Falmer, Brighton BN1 9QH, England 1 Introduction In Plotkin's applied typed lambda calculus PCF it is natural to consider one
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/por.ps.gz, 19940331
Interdefinability of Parallel Operations in PCF 1 Allen Stoughton Computer Science and Artificial Intelligence School of Cognitive and Computing Sciences University of Sussex Falmer, Brighton BN1 9QH, England
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/efa.ps.gz, 19940331
Equationally Fully Abstract Models of PCF 1 Allen Stoughton Computer Science and Artificial Intelligence School of Cognitive and Computing Sciences University of Sussex Falmer, Brighton BN1 9QH, England 1 Introduction In Plotkin's applied typed lambda calculus PCF it is natural to consider one
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/ppcf.ps.gz, 19940331
Parallel PCF has a Unique Extensional Model Allen Stoughton Computer Science and Artificial Intelligence School of Cognitive and Computing Sciences University of Sussex Falmer, Brighton BN1 9QH, England
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/por.ps.gz, 19940331
Interdefinability of Parallel Operations in PCF 1 Allen Stoughton Computer Science and Artificial Intelligence School of Cognitive and Computing Sciences University of Sussex Falmer, Brighton BN1 9QH, England
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/famopl.ps.gz, 19940401
Fully Abstract Models of Programming Languages Allen Stoughton School of Mathematical and Physical Sciences University of Sussex The preface and first chapter of a monograph that was published in 1988 in Pitman's Research Notes in Theoretical Computer Science series. Preface This monograph presents a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/famopl.ps.gz, 19940401
Fully Abstract Models of Programming Languages Allen Stoughton School of Mathematical and Physical Sciences University of Sussex The preface and first chapter of a monograph that was published in 1988 in Pitman's Research Notes in Theoretical Computer Science series. Preface This monograph presents a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/proto.ps.Z, 19940617
Action Semantics-Directed Prototyping Kyung-Goo Doh The University of Aizu David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/mfps94/program.ps.Z, 19940617
Tenth Workshop on the Mathematical Foundations of Programming Semantics Kansas State University March 20-23 1994 General Chairmen: Michael Mislove, Tulane University David Schmidt, Kansas State University Local Arrangements: David Schmidt, Kansas State University Maria Zamfir-Bleyberg, Kansas State
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/proto.ps.Z, 19940617
Action Semantics-Directed Prototyping Kyung-Goo Doh The University of Aizu David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/mfps94/program.ps.Z, 19940617
Tenth Workshop on the Mathematical Foundations of Programming Semantics Kansas State University March 20-23 1994 General Chairmen: Michael Mislove, Tulane University David Schmidt, Kansas State University Local Arrangements: David Schmidt, Kansas State University Maria Zamfir-Bleyberg, Kansas State
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/facets.ps.Z, 19940617
The Facets of Action Semantics: Some Principles and Applications (Extended Abstract) Kyung-Goo Doh The University of Aizu David A. Schmidt Kansas State Universityy
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/env.stack.ps.Z, 19940620
Stackability in the Typed Call-By-Value Lambda Calculus Anindya Banerjee and David A. Schmidt Department of Computing and Information Sciences Kansas State University y fbanerjee, schmidtg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/text/contents.ps, 19940621
Contents Series Foreword ix Preface xi 1 The Programming Language Core 1 1.1 A Core Imperative Language 1 1.2 Typing Rules 3 1.3 Induction and Recursion 6 1.4 Unicity of Typing 8 1.5 The Typing Rules Define the Language 10 1.6 The Semantics of the Core Language 12 1.7 Soundness of the Typing Rules 17
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/text/preface.ps, 19940621
Preface Although few programmers ever design a programming language, all programmers should understand the structuring techniques that a designer uses. Working from developments in lambda calculus and type theory, this textbook presents one such set of techniques. The book uses the techniques in a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/text/preface.ps, 19940621
Preface Although few programmers ever design a programming language, all programmers should understand the structuring techniques that a designer uses. Working from developments in lambda calculus and type theory, this textbook presents one such set of techniques. The book uses the techniques in a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/text/contents.ps, 19940621
Contents Series Foreword ix Preface xi 1 The Programming Language Core 1 1.1 A Core Imperative Language 1 1.2 Typing Rules 3 1.3 Induction and Recursion 6 1.4 Unicity of Typing 8 1.5 The Typing Rules Define the Language 10 1.6 The Semantics of the Core Language 12 1.7 Soundness of the Typing Rules 17
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hatcliff/thesis.ps.Z, 19940726
The Structure of Continuation-Passing Styles by John Mark Hatcliff B.A., Mount Vernon Nazarene College, 1988 M.Sc., Queen's University, 1991 A DISSERTATION submitted in partial fulfillment of the requirements for the degree DOCTOR OF PHILOSOPHY Department of Computing and Information Sciences College of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hatcliff/thesis.ps.Z, 19940726
The Structure of Continuation-Passing Styles by John Mark Hatcliff B.A., Mount Vernon Nazarene College, 1988 M.Sc., Queen's University, 1991 A DISSERTATION submitted in partial fulfillment of the requirements for the degree DOCTOR OF PHILOSOPHY Department of Computing and Information Sciences College of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/mcast_sw.ps, 19940809
Design of Multicast Packet Switches for High Speed Multi-service Networks K. Ravindran Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/mcast_sw.ps, 19940809
Design of Multicast Packet Switches for High Speed Multi-service Networks K. Ravindran Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/ilps94.ps.Z, 19940906
Datalog with Integer Periodicity Constraints David Toman, Jan Chomicki, and David S. Rogers Dept. of Comp. and Info. Sci. Kansas State University, Manhattan, KS{66506 fdavid,chomicki,rogersg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/ilps94.ps.Z, 19940906
Datalog with Integer Periodicity Constraints David Toman, Jan Chomicki, and David S. Rogers Dept. of Comp. and Info. Sci. Kansas State University, Manhattan, KS{66506 fdavid,chomicki,rogersg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/jlp94.ps.Z, 19940909
J. LOGIC PROGRAMMING 1993:12:1{199 1 DEPTH-BOUNDED BOTTOM-UP EVALUATION OF LOGIC PROGRAMS JAN CHOMICKI > We present here a depth-bounded bottom-up evaluation algorithm for logic programs. We show that it is sound, complete, and terminating for finiteanswer queries if the programs are syntactically
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/jlp94.ps.Z, 19940909
J. LOGIC PROGRAMMING 1993:12:1{199 1 DEPTH-BOUNDED BOTTOM-UP EVALUATION OF LOGIC PROGRAMS JAN CHOMICKI > We present here a depth-bounded bottom-up evaluation algorithm for logic programs. We show that it is sound, complete, and terminating for finiteanswer queries if the programs are syntactically
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/ipl90.ps.Z, 19941001
Generalized Closed World Assumption is 0 2-complete Jan Chomicki y V.S. Subrahmanian Dept. of Computer Science Dept.of Computer Science University of North Carolina University of Maryland Chapel Hill, NC 27599 College Park, MD 20742 chomicki@cs.unc.edu vs@mimsy.umd.edu October 1, 1994 Keywords: logic
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/ipl90.ps.Z, 19941001
Generalized Closed World Assumption is 0 2-complete Jan Chomicki y V.S. Subrahmanian Dept. of Computer Science Dept.of Computer Science University of North Carolina University of Maryland Chapel Hill, NC 27599 College Park, MD 20742 chomicki@cs.unc.edu vs@mimsy.umd.edu October 1, 1994 Keywords: logic
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/ieee94.ps.Z, 19941003
Temporal Integrity Constraints in Relational Databases Jan Chomicki Computing and Information Sciences Kansas State University Manhattan, KS 66506 chomicki@cis.ksu.edu 1 Introduction As historical databases become more widely used in practice , the need arises to address database integrity issues
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/ieee94.ps.Z, 19941003
Temporal Integrity Constraints in Relational Databases Jan Chomicki Computing and Information Sciences Kansas State University Manhattan, KS 66506 chomicki@cis.ksu.edu 1 Introduction As historical databases become more widely used in practice , the need arises to address database integrity issues
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/icdt95.ps.Z, 19941021
Constraint-Generating Dependencies Marianne Baudinet,1 Jan Chomicki,2 and Pierre Wolper3 1 Universit e Libre de Bruxelles, Informatique, 50 Avenue F.D. Roosevelt, C.P. 165, 1050 Brussels, Belgium Email: mb@cs.ulb.ac.be 2 Kansas State University, Dept of Computing and Information Sciences, 234 Nichols
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/icdt95.ps.Z, 19941021
Constraint-Generating Dependencies Marianne Baudinet,1 Jan Chomicki,2 and Pierre Wolper3 1 Universit e Libre de Bruxelles, Informatique, 50 Avenue F.D. Roosevelt, C.P. 165, 1050 Brussels, Belgium Email: mb@cs.ulb.ac.be 2 Kansas State University, Dept of Computing and Information Sciences, 234 Nichols
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/GradInfo/guide.to.PhD.ps, 19941107
A Guide to PhD Studies and Research Computing and Information Sciences Dept. Kansas State University Manhattan, Kansas Preface Several years ago, I chanced upon an internal report distributed by the Artificial Intelligence Department at Edinburgh University. The report, called The Researcher's Bible*,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/GradInfo/MS.manual.old.ps, 19941107
GUIDELINES FOR THE MASTER OF SCIENCE DEGREE IN THE DEPARTMENT OF COMPUTING AND INFORMATION SCIENCES KANSAS STATE UNIVERSITY SEPTEMBER 1992 GRADUATE STUDIES COMMITTEE Dr. Jan Chomicki Dr. William J. Hankley Dr. David A. Schmidt Head - 2 - I. INTRODUCTION These guidelines describe departmental and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/GradInfo/guide.to.PhD.ps, 19941107
A Guide to PhD Studies and Research Computing and Information Sciences Dept. Kansas State University Manhattan, Kansas Preface Several years ago, I chanced upon an internal report distributed by the Artificial Intelligence Department at Edinburgh University. The report, called The Researcher's Bible*,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howell/papers/iit.ps.Z, 19950120
On Non-Preemptive Scheduling of Recurring Tasks Using Inserted Idle Times Rodney R. Howell Muralidhar K. Venkatrao Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506 USA This author's current address is: Microsoft Corporation, One Microsoft Way, Redmond, WA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howell/papers/iit.ps.Z, 19950120
On Non-Preemptive Scheduling of Recurring Tasks Using Inserted Idle Times Rodney R. Howell Muralidhar K. Venkatrao Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506 USA This author's current address is: Microsoft Corporation, One Microsoft Way, Redmond, WA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howell/papers/ov.ps.Z, 19950120
Optimal Scheduling and Handling Potential Overload Rodney R. Howell Dept. of Computing and Information Sciences Kansas State University Manhattan, KS 66506 U.S.A.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howell/papers/ov.ps.Z, 19950120
Optimal Scheduling and Handling Potential Overload Rodney R. Howell Dept. of Computing and Information Sciences Kansas State University Manhattan, KS 66506 U.S.A.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/ictl94.ps.Z, 19950125
Temporal Query Languages: a Survey Jan Chomickiy January 24, 1995 Category: Survey Area: Temporal Databases
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/ictl94.ps.Z, 19950125
Temporal Query Languages: a Survey Jan Chomickiy January 24, 1995 Category: Survey Area: Temporal Databases
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/tkde95.ps.Z, 19950210
1 Implementing Temporal Integrity Constraints Using an Active DBMS Jan Chomicki and David Toman
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/tkde95.ps.Z, 19950210
1 Implementing Temporal Integrity Constraints Using an Active DBMS Jan Chomicki and David Toman
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/GradInfo/MS.manual.ps, 19950213
GUIDELINES FOR THE MASTER OF SCIENCE DEGREE IN THE DEPARTMENT OF COMPUTING AND INFORMATION SCIENCES KANSAS STATE UNIVERSITY January 1995 GRADUATE STUDIES COMMITTEE Dr. Rodney Howell Dr. Masaaki Mizuno Dr. David A. Schmidt Head - 2 - I. INTRODUCTION These guidelines describe departmental and university
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/GradInfo/MS.manual.ps, 19950213
GUIDELINES FOR THE MASTER OF SCIENCE DEGREE IN THE DEPARTMENT OF COMPUTING AND INFORMATION SCIENCES KANSAS STATE UNIVERSITY January 1995 GRADUATE STUDIES COMMITTEE Dr. Rodney Howell Dr. Masaaki Mizuno Dr. David A. Schmidt Head - 2 - I. INTRODUCTION These guidelines describe departmental and university
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/pods95.ps.Z, 19950314
Measuring Infinite Relations (Extended Abstract) Jan Chomicki Kansas State University chomicki@cis.ksu.edu Gabriel Kuper ECRC kuper@ecrc.de
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/pods95.ps.Z, 19950314
Measuring Infinite Relations (Extended Abstract) Jan Chomicki Kansas State University chomicki@cis.ksu.edu Gabriel Kuper ECRC kuper@ecrc.de
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/atlantique94.ps.Z, 19950420
Stackability in the Simply-Typed Call-By-Value Lambda Calculus Anindya Banerjee and David A. Schmidt y Department of Computing and Information Sciences Kansas State University z fbanerjee, schmidtg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/atlantique94.ps.Z, 19950420
Stackability in the Simply-Typed Call-By-Value Lambda Calculus Anindya Banerjee and David A. Schmidt y Department of Computing and Information Sciences Kansas State University z fbanerjee, schmidtg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/tods95.ps.Z, 19950522
Efficient Checking of Temporal Integrity Constraints Using Bounded History Encoding Jan Chomicki Computing and Information Sciences Kansas State University Manhattan, KS 66506 chomicki@cis.ksu.edu May 22, 1995 Keywords: database integrity, integrity constraints, temporal logic, temporal databases,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Chomicki/pods93.ps.Z, 19950522
On the Feasibility of Checking Temporal Integrity Constraints Jan Chomickiy Kansas State University Damian Niwi nskiz Warsaw University May 22, 1995 Keywords: integrity constraints, temporal logic, decidability, computational complexity, temporal databases. 1989 CR Classification: F.2.2, F.4.1, H.2.3.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/tods95.ps.Z, 19950522
Efficient Checking of Temporal Integrity Constraints Using Bounded History Encoding Jan Chomicki Computing and Information Sciences Kansas State University Manhattan, KS 66506 chomicki@cis.ksu.edu May 22, 1995 Keywords: database integrity, integrity constraints, temporal logic, temporal databases,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Chomicki/pods93.ps.Z, 19950522
On the Feasibility of Checking Temporal Integrity Constraints Jan Chomickiy Kansas State University Damian Niwi nskiz Warsaw University May 22, 1995 Keywords: integrity constraints, temporal logic, decidability, computational complexity, temporal databases. 1989 CR Classification: F.2.2, F.4.1, H.2.3.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Students/realizer/TR95-4.ps.Z, 19950604
Implementation of Intuitionistic Type Theory and Realizability Theory Yuki Komagata and David A. Schmidt Department of Computing and Information Sciences Kansas State University Manhattan, Kansas Technical Report Number: TR-CS-95-4
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Students/realizer/TR95-4.ps.Z, 19950604
Implementation of Intuitionistic Type Theory and Realizability Theory Yuki Komagata and David A. Schmidt Department of Computing and Information Sciences Kansas State University Manhattan, Kansas Technical Report Number: TR-CS-95-4
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/SAS95.ps.Z, 19950706
Natural-Semantics-Based Abstract Interpretation (Preliminary Version) David A. Schmidt Department of Computing and Information Sciences Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/SAS95.ps.Z, 19950706
Natural-Semantics-Based Abstract Interpretation (Preliminary Version) David A. Schmidt Department of Computing and Information Sciences Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/failure.ps, 19950712
Leader Election in the Presence of Link Failures Gurdip Singh Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/bfs.ps, 19950712
Adaptive Breadth-First Search Protocols Gurdip Singh Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/mst.ps, 19950712
A Highly Asynchronous Minimum Spanning Tree Protocol Gurdip Singh Department of Computing and Information Sciences, 234 Nichols Hall, Kansas State University, Manhattan, Kansas 66506 Arthur J. Bernstein Department of Computer Science SUNY at Stony Brook Stony Brook, Long Island, NY 11794.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/mst.ps, 19950712
A Highly Asynchronous Minimum Spanning Tree Protocol Gurdip Singh Department of Computing and Information Sciences, 234 Nichols Hall, Kansas State University, Manhattan, Kansas 66506 Arthur J. Bernstein Department of Computer Science SUNY at Stony Brook Stony Brook, Long Island, NY 11794.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/complete.ps, 19950712
Leader Election in Complete Networks Gurdip Singh Department of Computing and Information Sciences, 234 Nichols Hall, Kansas State University, Manhattan, Kansas 66506 email: singh@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/failure.ps, 19950712
Leader Election in the Presence of Link Failures Gurdip Singh Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/complete.ps, 19950712
Leader Election in Complete Networks Gurdip Singh Department of Computing and Information Sciences, 234 Nichols Hall, Kansas State University, Manhattan, Kansas 66506 email: singh@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/bfs.ps, 19950712
Adaptive Breadth-First Search Protocols Gurdip Singh Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/vita.ps, 19950714
August 1995 Curriculum Vitae David A. Schmidt Computing and Info. Sciences Department Kansas State University Manhattan, Kansas 66506 U.S.A. Phone: 913-532-6350 Fax: 913-532-7353 Internet: schmidt@cis.ksu.edu WWW URL: http://www.cis.ksu.edu/ schmidt/home.html Born: May 10, 1953, Colby, Kansas Degrees:
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/vita.ps, 19950714
August 1995 Curriculum Vitae David A. Schmidt Computing and Info. Sciences Department Kansas State University Manhattan, Kansas 66506 U.S.A. Phone: 913-532-6350 Fax: 913-532-7353 Internet: schmidt@cis.ksu.edu WWW URL: http://www.cis.ksu.edu/ schmidt/home.html Born: May 10, 1953, Colby, Kansas Degrees:
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/GradInfo/PhD.manual.old.ps, 19950717
GUIDELINES FOR THE DEGREE OF DOCTOR OF PHILOSOPHY IN THE DEPARTMENT OF COMPUTING AND INFORMATION SCIENCES KANSAS STATE UNIVERSITY February 1992 GRADUATE STUDIES COMMITTEE Dr. Austin Melton - Chair Dr. William Hankley Dr. Jan Chomicki - 2 - 1. INTRODUCTION 1a. This document describes requirements and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/thesis.ps, 19950822
DATA FLOW ANALYSIS FOR VERIFYING CORRECTNESS PROPERTIES OF CONCURRENT PROGRAMS A Dissertation Presented by MATTHEW B. DWYER Submitted to the Graduate School of the University of Massachusetts Amherst in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY September 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/thesis.ps, 19950822
DATA FLOW ANALYSIS FOR VERIFYING CORRECTNESS PROPERTIES OF CONCURRENT PROGRAMS A Dissertation Presented by MATTHEW B. DWYER Submitted to the Graduate School of the University of Massachusetts Amherst in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY September 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec2.ps, 19950824
Network: - a set of entities connected by communication links * telephone networks * internet * hardware circuits * U.S postal service Why Networks * allow communication * sharing of resources * increased reliability Components of a Network * host machine/entities * communication system - transmission
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/lec3.ps, 19950829
Protocol: Message format/encoding -control field -data field Formatting methods - Bit oriented - character oriented - byte-count oriented Train Example: Finite State Machine Model FSM = (I, O, S, T, L, so) I = set of input actions O = set of output actions S = set of states so = initial state T: S * I !
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec4.ps, 19950830
S: Repeat get D from network layer send D to R ackd := false while not ackd do receive M from R if M = nack then send D to R if M = ack then ack := true R: Repeat receive D from S if error(D) then send nack to S else send ack to S; deliver D to network layer data in array Sdata S: ns := 1 R !
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec5.ps, 19950905
1 2 3 4 5 rec_user rec_user -d0 -d1 1 2 3 4 5 send_user +d1 +d0 send_user timeout timeout +ack1 +ack0 -ack0 +d0 -ack1 +d1 Figure 1: 1 ns := 1 R ! (Sdata,ns); ns = ns + 1 2 R nack(s); if s > na then na := s 2 timeout ! ns := na 2 nr := 1; S (D,x) ! if x = nr then Rdata = D; nr := nr + 1 S !
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/compact.ps, 19950905
A Compact Petri Net Representation and Its Implications for Analysis * Matthew B. Dwyer Lori A. Clarke y dwyer@cis.ksu.edu clarke@cs.umass.edu Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 (913)532-6350 yDepartment of Computer Science
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/complete-ea.ps, 19950905
Data Flow Analysis Frameworks for Concurrent Programs (Extended Abstract) Matthew B. Dwyer Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 dwyer@cis.ksu.edu (913)532-6350 before 8/1/95: Department of Computer Science Lederle Graduate Research
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/dfa-dssa.ps, 19950905
A Flexible Architecture for Building Data Flow Analyzers 1 Matthew B. Dwyer Lori A. Clarke y dwyer@cis.ksu.edu clarke@cs.umass.edu Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 (913)532-6350 yDepartment of Computer Science University of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/compact.ps, 19950905
A Compact Petri Net Representation and Its Implications for Analysis * Matthew B. Dwyer Lori A. Clarke y dwyer@cis.ksu.edu clarke@cs.umass.edu Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 (913)532-6350 yDepartment of Computer Science
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/complete.ps, 19950905
Data Flow Analysis Frameworks for Concurrent Programs 1 Matthew B. Dwyer dwyer@cis.ksu.edu Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 (913)532-6350 1This work was supported by the Advanced Research Projects Agency under Grant
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/complete-ea.ps, 19950905
Data Flow Analysis Frameworks for Concurrent Programs (Extended Abstract) Matthew B. Dwyer Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 dwyer@cis.ksu.edu (913)532-6350 before 8/1/95: Department of Computer Science Lederle Graduate Research
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/dfa-dssa.ps, 19950905
A Flexible Architecture for Building Data Flow Analyzers 1 Matthew B. Dwyer Lori A. Clarke y dwyer@cis.ksu.edu clarke@cs.umass.edu Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 (913)532-6350 yDepartment of Computer Science University of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/complete.ps, 19950905
Data Flow Analysis Frameworks for Concurrent Programs 1 Matthew B. Dwyer dwyer@cis.ksu.edu Department of Computing and Information Sciences Nichols Hall Kansas State University Manhattan, KS 66506 (913)532-6350 1This work was supported by the Advanced Research Projects Agency under Grant
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec6.ps, 19950907
Sliding Window Protocol: S:ns := 1; na := 1 *,ns); ns++ 2R ack(s) !if s>na then na:=s 2timeout !ns:=na ]R:nr:=1 *=D; nr++ S!ack(nr) 1 Selective Retransmission S:ns:=1; na:=1 *,ns); ns++ 2R nack(s) !R!(Sdata,s); na:=s
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/parallel.ps, 19950912
Protocol Design by Parallel Composition* Gurdip Singh Department of Computing and Information Sciences 234 Nichols Hall, Kansas State University Manhattan, Kansas 66506 Arthur J. Bernstein Department of Computer Science SUNY at Stony Brook Stony Brook, Long Island, NY 11794.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/parallel.ps, 19950912
Protocol Design by Parallel Composition* Gurdip Singh Department of Computing and Information Sciences 234 Nichols Hall, Kansas State University Manhattan, Kansas 66506 Arthur J. Bernstein Department of Computer Science SUNY at Stony Brook Stony Brook, Long Island, NY 11794.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec7.ps, 19950912
High-Level Data Link Control Protocol (HDLC protocol) -several possible modes Frame types: 1. Information frames 2. Supervisory frames 3. Unnumbered frames Information frames |Flag |Address| Control|Info |FCS |Flag| 8 8 8 16 8 flag = 01111110 control field: |0 | N(S) |P/F| N(R) | 1 Supervisory frame
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/shared.ps, 19950912
A Compositional Approach for Designing Protocols* Gurdip Singh Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/shared.ps, 19950912
A Compositional Approach for Designing Protocols* Gurdip Singh Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec8.ps, 19950913
- S' is reachable from S in P if there exists an execution sequence s1; s2; :::; sn, where S = s1 and S' = sn - S is a reachable state of protocol P if S is reachable from the initial state in P - State(P) = set of reachable states of P - Unspecified reception: S = (u,v,x,y) is an unspecified reception
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/assign1.ps, 19950914
CIS 725: Advanced Computer Networks, Fall 95 Homework Assignment 1, Due lecture 12, 30 points (10%) 1. In the class, we discussed the half-duplex sliding window protocol (which handles message loss). Modify this protocol to handle full-duplex transmission. Assume that there exists two terminals, A and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/assign1.ps, 19950914
CIS 725: Advanced Computer Networks, Fall 95 Homework Assignment 1, Due lecture 12, 30 points (10%) 1. In the class, we discussed the half-duplex sliding window protocol (which handles message loss). Modify this protocol to handle full-duplex transmission. Assume that there exists two terminals, A and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/lec12.ps, 19950928
CREQ1 -REQ1 CCONF1 +REQ1 CIND2 CRES2 +ACK1 -ACK1 CRES1 CIND1 CREQ2 -REQ2 +REQ2 +ACK2 CCONF2 -ACK2 Figure 1: 1 CREQ1 -REQ1 +ACK1 CCONF DREQ1 DREQ1 DREQ1 DREQ1 DREQ1 -D +REQ1 CIND2 CRES2 -ACK1 +D -DIIND2
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/lec13.ps, 19951002
Medium Access Control (MAC) sublayer - between physical and data link layer - broadcast/multiaccess channels - N independent stations * each generates traffic independently * if two transmit at the same time both frames are garbled Pure ALOHA - A station transmits whenever it wants - sender detects
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/sync.ps, 19951004
Transport-oriented Service Models for Synchronization of Multimedia Data Streams K. Ravindran Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu Technical Report TR:93-8 January 1993 (revised in December 1994, August 1995)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/sync.ps, 19951004
Transport-oriented Service Models for Synchronization of Multimedia Data Streams K. Ravindran Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu Technical Report TR:93-8 January 1993 (revised in December 1994, August 1995)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/prog-assign.ps, 19951005
CIS 725: Advanced Computer Networks Programming Assignment 1 (75 points) The goal of this assignment is to develop a protocol for the Agreement problem. In the Agreement problem, each process i in the network has two variables ini and outi. At the beginning of the protocol, process i assigns a value to
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/prog-assign.ps, 19951005
CIS 725: Advanced Computer Networks Programming Assignment 1 (75 points) The goal of this assignment is to develop a protocol for the Agreement problem. In the Agreement problem, each process i in the network has two variables ini and outi. At the beginning of the protocol, process i assigns a value to
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec15.ps, 19951010
Protocol Validation: -check whether protocol specification meets the service specification Reachability analysis: - generate all reachable states analyze() f if (W is empty) return q = element from W add q to A if (q = error state) report error else f for each successor state s of q if (s 62 (A
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec16.ps, 19951018
B / lambda A/ 0 A/ 0 B / 1 A/ 1 A/ 0 B / 1 A/ 1 B / 0 B / 1 1 2 3 4 Figure 1: Transition tour: B A B A B A A A A A A A B B General algorithm To test transition (s1,s2): (1) apply reset to M (2) Find shortest path to s1 and apply input of the path (3) Apply input for transition (s1,s2) (4) check if state
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/lec19.ps, 19951023
End-to-End flow control Routing - Datagram routing * each packet is routing independently * unordered, unreliable - Virtual Circuit routing * set up a path for each connection * all messages are sent over this path * ordered, reliable 1 Routing table next hop information At each node i, for each
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/multiphase.ps, 19951024
On the Construction of Multiphase Communicating Protocols* Gurdip Singh and Madhavi Sammeta Department of Computing and Information Sciences 234 Nichols Hall, Kansas State University Manhattan, Kansas 66506 email: fsingh, sammetag@cis.ksu.edu October 24, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/multiphase.ps, 19951024
On the Construction of Multiphase Communicating Protocols* Gurdip Singh and Madhavi Sammeta Department of Computing and Information Sciences 234 Nichols Hall, Kansas State University Manhattan, Kansas 66506 email: fsingh, sammetag@cis.ksu.edu October 24, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/repl.ps, 19951031
Replication Protocol Structures for Fault-tolerant Remote Procedure Calls K. Ravindran && Shanthi Pichai Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi, shanthi@cis.ksu.edu S. T. Chanson Department of Computer Science University of British
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/perf.ps, 19951031
Performance Engineering of End-systems for High Bandwidth Multimedia Communications K. Ravindran && K. Bhat Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu 15th October 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/repl.ps, 19951031
Replication Protocol Structures for Fault-tolerant Remote Procedure Calls K. Ravindran && Shanthi Pichai Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi, shanthi@cis.ksu.edu S. T. Chanson Department of Computer Science University of British
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/perf.ps, 19951031
Performance Engineering of End-systems for High Bandwidth Multimedia Communications K. Ravindran && K. Bhat Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu 15th October 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec22.ps, 19951101
Dij;k = distance of i to j via neighbor k a b c d e 2 1 2 2 4 1 a c d a c d e 2 4 5 1 6 5 6 4 2 7 3 3 Distance Table for b Routing Table a a 2 c c 1 d d 2 e c 3 Figure 1: Bellman-Ford Algorithm Protocol at node i On receiving distance table from j Update column i of the distance table as follows: For
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/CRC.chapter.ps.Z, 19951101
Programming Language Semantics David A. Schmidt Department of Computing and Information Sciences Kansas State University October 24, 1995 A programming language possesses two fundamental features: syntax and semantics. Syntax refers to the appearance of the well-formed programs of the language, and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/CRC.chapter.ps.Z, 19951101
Programming Language Semantics David A. Schmidt Department of Computing and Information Sciences Kansas State University October 24, 1995 A programming language possesses two fundamental features: syntax and semantics. Syntax refers to the appearance of the well-formed programs of the language, and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec23.ps, 19951106
The following gives the computation of routes using the Bellman-Ford algorithm for the example discussed in the class. As indicated in the class, in the distance table, each row corresponds to a destination and each column corresponds to a neighbor. In the routing table, a row corresponds to a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr95-11.ps, 19951109
Lock Based Self-Stabilizing Distributed Mutual Exclusion Algorithms Masaaki Mizuno * Mikhail Nesterenko Hirotsugu Kakugawa Dept. of Comp. and Info. Sciences Dept. of Elect. Engineering Kansas State University Hiroshima University Manhattan, Kansas 66506 Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr95-11.ps, 19951109
Lock Based Self-Stabilizing Distributed Mutual Exclusion Algorithms Masaaki Mizuno * Mikhail Nesterenko Hirotsugu Kakugawa Dept. of Comp. and Info. Sciences Dept. of Elect. Engineering Kansas State University Hiroshima University Manhattan, Kansas 66506 Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr95-12.ps, 19951110
A Timestamp Based Transformation of Self-Stabilizing Programs for Distributed Computing Environments Masaaki Mizuno* Hirotsugu Kakugawa Dept. of Comp. and Info. Sciences Dept. of Elect. Engineering Kansas State University Hiroshima University Manhattan, KS 66506 Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr95-12.ps, 19951110
A Timestamp Based Transformation of Self-Stabilizing Programs for Distributed Computing Environments Masaaki Mizuno* Hirotsugu Kakugawa Dept. of Comp. and Info. Sciences Dept. of Elect. Engineering Kansas State University Hiroshima University Manhattan, KS 66506 Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/lec25.ps, 19951113
Techniques to deal with congestion 1. Buffer reservation - possible with virtual circuit communication - reserve buffers when establishing the circuit - prevents congestion 2. Packet discarding - no reservation - discard packets if buffers are full - how to allocate buffers to various lines allocate one
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/scp.ps.Z, 19951120
Stackability in the Simply-Typed Call-By-Value Lambda Calculus Anindya Banerjee yand David A. Schmidt z Department of Computing and Information Sciences Kansas State University x fbanerjee, schmidtg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/scp.ps.Z, 19951120
Stackability in the Simply-Typed Call-By-Value Lambda Calculus Anindya Banerjee yand David A. Schmidt z Department of Computing and Information Sciences Kansas State University x fbanerjee, schmidtg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Unger/tr95-6.ps, 19951122
Time Passive Property in Linear Past Temporal Logic Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-95-6 August, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Unger/tr95-6.ps, 19951122
Time Passive Property in Linear Past Temporal Logic Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-95-6 August, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Unger/tr95-13.ps, 19951127
String Constraints in Logic Programming Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-95-13 November 14, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Unger/tr95-13.ps, 19951127
String Constraints in Logic Programming Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-95-13 November 14, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/examples.ps, 19951211
1. Consider two stations A and B which are 100 miles apart and connected by a 100 Mbits/sec link. The round trip delay (approx) = 2 100 1600=(3 108) = 1ms In 1ms, 100 106 10 3 = 105 bits of data can be transmitted. If packet size is 1000 bits then, a window size of at least 105=1000 = 100 is need to
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/examples.ps, 19951211
1. Consider two stations A and B which are 100 miles apart and connected by a 100 Mbits/sec link. The round trip delay (approx) = 2 100 1600=(3 108) = 1ms In 1ms, 100 106 10 3 = 105 bits of data can be transmitted. If packet size is 1000 bits then, a window size of at least 105=1000 = 100 is need to
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Students/papers-int.ps.Z, 19951213
Point vs. Interval-based Query Languages for Temporal Databases (extended abstract) David Toman
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Students/papers-int.ps.Z, 19951213
Point vs. Interval-based Query Languages for Temporal Databases (extended abstract) David Toman
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/icse18.copyright.ps, 19951215
A Flexible Architecture for Building Data Flow Analyzers * Matthew B. Dwyer Lori A. Clarke Dept. of Computing and Info. Sciences Dept. of Computer Science Kansas State University University of Massachusetts Manhattan, KS 66506 Amherst, MA 01003
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/icse18.copyright.ps, 19951215
A Flexible Architecture for Building Data Flow Analyzers * Matthew B. Dwyer Lori A. Clarke Dept. of Computing and Info. Sciences Dept. of Computer Science Kansas State University University of Massachusetts Manhattan, KS 66506 Amherst, MA 01003
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Ravindran/mcast.ps, 19951229
Network Abstractions and Resource Allocation Models for Data Multicasting in Multi-service Networks K. Ravindran Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Ravindran/mcast.ps, 19951229
Network Abstractions and Resource Allocation Models for Data Multicasting in Multi-service Networks K. Ravindran Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA. E-mail: ravi@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howard/sorting.ps.Z, 19960118
Another Iteration on Darlington's A Synthesis of Several Sorting Algorithms" Brian Howard Kansas State University Draft: October 18, 1994 In A Synthesis of Several Sorting Algorithms" , Darlington showed how to use program transformation techniques to develop versions of six well-known sorting
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howard/inproret.ps.Z, 19960118
Inductive, Projective, and Retractive Types Brian T. Howard Institute for Research in Cognitive Science University of Pennsylvania bhoward@saul.cis.upenn.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howard/icfp.ps.Z, 19960118
Inductive, Coinductive, and Pointed Types Brian T. Howard Department of Computer and Information Sciences Kansas State University bhoward@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howard/icfp.ps.Z, 19960118
Inductive, Coinductive, and Pointed Types Brian T. Howard Department of Computer and Information Sciences Kansas State University bhoward@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howard/fcc.ps.Z, 19960118
Fixpoint Computations and Coiteration (Extended Abstract) Brian T. Howard Department of Computer and Information Sciences Kansas State University bhoward@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howard/inproret.ps.Z, 19960118
Inductive, Projective, and Retractive Types Brian T. Howard Institute for Research in Cognitive Science University of Pennsylvania bhoward@saul.cis.upenn.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howard/sudiss.ps.Z, 19960118
Fixed Points and Extensionality in Typed Functional Programming Languages Brian T. Howard Computer Science Department Stanford University October 19, 1992
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howard/lispfp90.ps.Z, 19960118
Operational and Axiomatic Semantics of PCF Brian T. Howard John C. Mitchelly Department of Computer Science Stanford University fbhoward,jcmg@cs.stanford.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howard/lispfp90.ps.Z, 19960118
Operational and Axiomatic Semantics of PCF Brian T. Howard John C. Mitchelly Department of Computer Science Stanford University fbhoward,jcmg@cs.stanford.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howard/fcc.ps.Z, 19960118
Fixpoint Computations and Coiteration (Extended Abstract) Brian T. Howard Department of Computer and Information Sciences Kansas State University bhoward@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howard/sudiss.ps.Z, 19960118
Fixed Points and Extensionality in Typed Functional Programming Languages Brian T. Howard Computer Science Department Stanford University October 19, 1992
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howard/sorting.ps.Z, 19960118
Another Iteration on Darlington's A Synthesis of Several Sorting Algorithms" Brian Howard Kansas State University Draft: October 18, 1994 In A Synthesis of Several Sorting Algorithms" , Darlington showed how to use program transformation techniques to develop versions of six well-known sorting
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Cover.ps, 19960123
PROGRAM SPECIFICATION VERIFICATION @ 1991 William Hankley Department of Computing & Information Sciences Kansas State University Manhattan, KS 66502
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap1.ps, 19960123
Chapter 1 Introduction Page 1 Specification and Verification 1991 1. Introduction The subjects of this book are formal specifications of programs and formal verification of specifications and programs. This chapter introduces these concepts and it explains how specification and verification are related
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Cover.ps, 19960123
PROGRAM SPECIFICATION VERIFICATION @ 1991 William Hankley Department of Computing & Information Sciences Kansas State University Manhattan, KS 66502
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/771syllabus.ps, 19960123
PROGRAMMING SCIENCE CIS 771 Spring 1996 Subtitle: Formal Specification of Programs and Components and Verification of Properties of Specifications Line: #32430, T/TH 2:05-3:20 pm, Jan. 23 - May 9, Durland 154 Instructor: Dr. William Hankley email: hankley@cis.ksu.edu www:
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/cover.ps, 19960123
PROGRAM SPECIFICATION VERIFICATION @ 1991 William Hankley Department of Computing & Information Sciences Kansas State University Manhattan, KS 66502
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap1.ps, 19960123
Chapter 1 Introduction Page 1 Specification and Verification 1991 1. Introduction The subjects of this book are formal specifications of programs and formal verification of specifications and programs. This chapter introduces these concepts and it explains how specification and verification are related
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/TOC.ps, 19960125
Table of Contents Page i Specification and Verification 1991 Table of Contents Page i Note: Page numbers are not consequtive; there are page jumps between chapters. 1. Introduction 1 1.1 About Specifications 1.2 About Verification 1.3 Relationship to Software Development 2. Non-Procedural Languages 20
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap2.ps, 19960125
Chapter 2 Non-Procedural Languages Page 20 Specification and Verification 1991 2. Non-Procedural Languages This chapter presents background concepts that will be useful in later chapers on developing formal specifications. This chapter presents introductions to three nonprocedural languages -- Prolog,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap2.ps, 19960125
Chapter 2 Non-Procedural Languages Page 20 Specification and Verification 1991 2. Non-Procedural Languages This chapter presents background concepts that will be useful in later chapers on developing formal specifications. This chapter presents introductions to three nonprocedural languages -- Prolog,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/TOC.ps, 19960125
Table of Contents Page i Specification and Verification 1991 Table of Contents Page i Note: Page numbers are not consequtive; there are page jumps between chapters. 1. Introduction 1 1.1 About Specifications 1.2 About Verification 1.3 Relationship to Software Development 2. Non-Procedural Languages 20
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/TOC.ps, 19960125
Table of Contents Page i Specification and Verification 1991 Table of Contents Page i Note: Page numbers are not consequtive; there are page jumps between chapters. 1. Introduction 1 1.1 About Specifications 1.2 About Verification 1.3 Relationship to Software Development 2. Non-Procedural Languages 20
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/chap2.ps, 19960125
Chapter 2 Non-Procedural Languages Page 20 Specification and Verification 1991 2. Non-Procedural Languages This chapter presents background concepts that will be useful in later chapers on developing formal specifications. This chapter presents introductions to three nonprocedural languages -- Prolog,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture1.ps.gz, 19960130
Verification and Validation CIS 841 (NTU SE 750-KS) Instructor: Matthew Dwyer Phone: (913) 532-6350 FAX: (913) 532-7353 Email: dwyer@cis.ksu.edu WWW: http://www.cis.ksu.edu/~dwyer Office: Nichols 324e Hours: T, TH 2:00-3:00 Prerequisites CIS 740 -- Graduate Software Engineering Should be familiar with :
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/lecture2.ps.gz, 19960130
Last Time ... We talked about class setup setting the context for our study This time finish up the introductory material begin the theoretical foundations Relations A RELATION, R, over a set, S = {s t } is a set of ordered n-tuples R = {r i }, where r i = (s i,1 , s i,2 , ... , s i,n A Binary relation
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture3.ps.gz, 19960130
Last Time ... We ... finished up the intro started reviewing mathematical background This time ... finish up the mathematical background a few basic definitions start talking about program models You should ... have read the Adrion et. al. article surveys basic concepts covered in this course defines a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture4.ps.gz, 19960201
Last Time ... We ...finish up the mathematical background a few basic definitions This time ... start talking about program models For next time ... Read the specification papers Think of some interesting partial program behaviors produce some example behaviors try to generalize Play around with regular
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Unger/tr96-1.ps, 19960202
Calendar Algebra Robert J. Zhang Elizabeth Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-96-1 January, 1996
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Unger/tr95-14.ps, 19960202
Introduction to Database Integrity Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-95-14 December, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Unger/tr96-1.ps, 19960202
Calendar Algebra Robert J. Zhang Elizabeth Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-96-1 January, 1996
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Unger/tr95-14.ps, 19960202
Introduction to Database Integrity Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-95-14 December, 1995
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture8.ps.gz, 19960215
Last Time ... I talked about Weakening Traces A Regular Expression Formalism This time I'll talk about More About Regular Expression Formalism Example Specifications Assignment 1 Writing Specifications Scope Syntax Semantics Style Scope of a Specification What does this specification talk about
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture7.ps.gz, 19960215
Last Time ... I talked about Specification formalisms Properties of specifications Trace specifications This time I'll talk about Weakening Traces A Regular Expression Formalism Assignment 1 Weakening Traces Traces capture program behavior by defining Legal sequences of calls defining correct Values of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture9.ps.gz, 19960219
Last Time ... I talked more about our regular expression formalism a number of example specifications Today more details about Assignment 1 start on the next part of the course The First Assignment Model Building Specification Writing Exploring Different Approaches The Application We have a program
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap3.ps, 19960220
Chapter 3 Base Data Types Page 60 Specification and Verification 1991 3. Base Data Types This chapter introduces data types that are used in the following chapters to compose specifications. These are called base types because they are used to compose specifications for other more complex structures.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap3.ps, 19960220
Chapter 3 Base Data Types Page 60 Specification and Verification 1991 3. Base Data Types This chapter introduces data types that are used in the following chapters to compose specifications. These are called base types because they are used to compose specifications for other more complex structures.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/chap3.ps, 19960220
Chapter 3 Base Data Types Page 60 Specification and Verification 1991 3. Base Data Types This chapter introduces data types that are used in the following chapters to compose specifications. These are called base types because they are used to compose specifications for other more complex structures.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture10.ps.gz, 19960221
Last Time ... I talked about Assignment 1 about Fagan-style inspections Today we'll look at inspection checklists weaknesses of inspections focusing inspections building our own inspections Heads Up In this lecture we're going to look at checklists It would be helpful for you to have them Appendix A of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture6.ps.gz, 19960221
Last Time ... We finished up our discussion of program models. Today I ll discuss ... Specifications Trace specifications Path expressions a few example specifications Specifications define intent provide a contract between producer and consumer user and requirements analyst designer and designer
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/assign1.ps, 19960224
CIS 841 Assignment 1 Spring 1996 Feb. 19, 1996 The first project requires you to apply concepts related to program models and software specification to a rather simple application. The Application The application is very simple; it reads a list of integers and prints out those values that lie below a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/assign1.ps, 19960224
CIS 841 Assignment 1 Spring 1996 Feb. 19, 1996 The first project requires you to apply concepts related to program models and software specification to a rather simple application. The Application The application is very simple; it reads a list of integers and prints out those values that lie below a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/text/errata.ps, 19960228
Errata for ``The Structure of Typed Programming Languages'' 27 February 1996 Page xiii, Line -12: ``Hemerik and Barendregt 1990'' should be ``Barendregt and Hemerik 1990''. Page xiii, Line -11: ``Tennent 1977'' should be ``Tennent 1977a''. Page 4, Figure 1.3: Several of the tree arcs should be shifted
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/text/errata.ps, 19960228
Errata for ``The Structure of Typed Programming Languages'' 27 February 1996 Page xiii, Line -12: ``Hemerik and Barendregt 1990'' should be ``Barendregt and Hemerik 1990''. Page xiii, Line -11: ``Tennent 1977'' should be ``Tennent 1977a''. Page 4, Figure 1.3: Several of the tree arcs should be shifted
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture13.ps.gz, 19960301
Last Time Talked about how to formulate a flow analysis uninitialized variable analysis This time finish talking about data flow frameworks discuss flow analysis for verifying QRE specifications Flow Analysis for Verification Recall that we had two different comparisons L(CFG) and L(Spec) are disjoint
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture13.lw.ps, 19960303
Last Time Talked about how to formulate a flow analysis uninitialized variable analysis This time finish talking about data flow frameworks discuss flow analysis for verifying QRE specifications Flow Analysis for Verification Recall that we had two different comparisons L(CFG) and L(Spec) are disjoint
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture12.lw.ps, 19960303
Capturing the effect of program statements How does a statement effect the information of interest e.g., for Avail an assignment to x := y+2 makes the expression y+2 available Transfer functions Functions are defined over the set of facts Transform the facts seen on input to a new set of facts available
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture11.lw.ps, 19960303
Last Time ... We talked about phased inspections checklists (we ll come back to this) This time we ll talk about automated static analysis flow analysis Static Analysis Ultimately, we want assurances about the behavior of a program when executed Recall, behaviors can be thought of as state sequences
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture14a.ps.gz, 19960307
Symbolic Evaluation (Symbolic Execution) Creates a functional representation of a path (executable component) For a path Pi D is the domain for path Pi C is the computation for path Pi Functional Representation of an Executable Component P : X fi Y P is composed of partial functions
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture15.ps.gz, 19960307
Inter-Procedural Analysis We use packages/subprograms to create abstractions data abstractions control abstractions Abstractions hide detailed execution behavior Good design minimizes cross-boundary information flow An accurate analysis of execution behavior MUST cut across abstraction boundaries Same
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture14b.ps.gz, 19960307
Last Time ... Looked at a ... symbolic execution more precise than flow analysis more expensive than flow analysis Today ... finish up global symbolic evaluation inter-procedural analyses Alternative Approaches to Symbolic Evaluation Dynamic Symbolic Execution Data dependent Global Symbolic Evaluation
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/tpn.ps, 19960307
A Compact Petri Net Representation and Its Implications for Analysis * KSU CIS TR 95-9 Matthew B. Dwyer Lori A. Clarke dwyer@cis.ksu.edu clarke@cs.umass.edu Dept. of Computing and Info. Sciences Dept. of Computer Science Kansas State University University of Massachusetts Manhattan, KS 66506 Amherst, MA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/tpn.ps, 19960307
A Compact Petri Net Representation and Its Implications for Analysis * KSU CIS TR 95-9 Matthew B. Dwyer Lori A. Clarke dwyer@cis.ksu.edu clarke@cs.umass.edu Dept. of Computing and Info. Sciences Dept. of Computer Science Kansas State University University of Massachusetts Manhattan, KS 66506 Amherst, MA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture16a.ps.gz, 19960313
1 Last Time ... We finished up static analysis symbolic evaluation inter-procedural analysis Today we start on the next part of the course dynamic analysis assertion checking As we talk about this think about how to classify symbolic evaluation Announcements Assignment 2 part A is online part B is hot
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture16b.ps.gz, 19960313
Assertions A dynamic testing capability self-checking software Insert specifications about the intent of a system During execution, monitor if the assertion is violated If violated then perform some action: display information to help find the source of the error 1 Exceptions versus Assertions
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture18b.ps, 19960320
Operand mutations Constant replacement e.g., x := x + 5; would replace 5 with each constant of the appropriate type that appears in the program Scalar variable replacement e.g., x := x + 5; would replace x with each scalar variable of the appropriate type that appears in the program Operand mutations
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture17.ps, 19960320
Last Time ... I talked about dynamic analyses about assertion checking Today we'll finish up assertion checking I'll outline our coverage of testing Approaches to Testing + Fault-based Testing + Coverage-based Testing + Specification-based Testing - Transaction/Thread/Use-case Testing Transaction
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture18a.ps, 19960320
Last Time ... finished up dynamic assertion methods APP is available via ftp I've installed it locally layed out our plan for covering testing This time ... discuss assignment #1 solutions discuss assignment #2 part B mutation testing Assignment #1 In general people did a pretty good job most people
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap5.ps, 19960402
Chapter 5 Predicates and Assertions Page 100 Specification and Verification 1991 5. Predicates and Assertions This chapter presents a semi-formal definition of predicates and assertions. Predicates are Boolean expressions. They are similar to the Boolean expressions used in programming languages, but
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap5.ps, 19960402
Chapter 5 Predicates and Assertions Page 100 Specification and Verification 1991 5. Predicates and Assertions This chapter presents a semi-formal definition of predicates and assertions. Predicates are Boolean expressions. They are similar to the Boolean expressions used in programming languages, but
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap6.ps, 19960402
Chapter 6 Specification of Package Modules Page 120 Specification and Verification 1991 6. Specification of Package Modules This chapter presents concepts and examples of model-based specifications of package modules using a syntax style based on that of Ada package specifications. A package is the Ada
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap4.ps, 19960402
Chapter 4 Formal Definitions Page 80 Specification and Verification 1991 4. Formal Definitions This chapter presents three techniques for formal definitions -- axiomatic, algebraic, and model-based. The purpose of this chapter is for you to develop some beginning skill in writing algebraic and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap4.ps, 19960402
Chapter 4 Formal Definitions Page 80 Specification and Verification 1991 4. Formal Definitions This chapter presents three techniques for formal definitions -- axiomatic, algebraic, and model-based. The purpose of this chapter is for you to develop some beginning skill in writing algebraic and
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap6.ps, 19960402
Chapter 6 Specification of Package Modules Page 120 Specification and Verification 1991 6. Specification of Package Modules This chapter presents concepts and examples of model-based specifications of package modules using a syntax style based on that of Ada package specifications. A package is the Ada
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/Chap6.ps, 19960402
Chapter 6 Specification of Package Modules Page 120 Specification and Verification 1991 6. Specification of Package Modules This chapter presents concepts and examples of model-based specifications of package modules using a syntax style based on that of Ada package specifications. A package is the Ada
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/lecture20.ps.gz, 19960405
Last Time ... Previously discussed mutation testing Today highlights of mutation testing PIE validity of testing assumptions Using Mutation Testing You've developed a program You've developed a set of test cases for the program All of the test cases pass There are two possible situations the program is
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/lomapsabs.ps.Z, 19960407
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/lecture21.ps.gz, 19960408
Last Time ... Finished up our discussion of mutation testing Talked about PIE and coupling effect Today, we ll start on two other forms of structural testing Structural Test Data Selection fault-based e.g., mutation testing coverage based domain based Domain Testing Values of input variables partition
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/boston.ps.Z, 19960411
Challenges to Programming Language Semantics David A. Schmidt Kansas State University 1 Complementary Semantics Definitions and Abstract Interpretation The development and initial successes of Scott-Strachey denotational semantics in the 1970s gave hope to those who desired a canonical definition format
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/boston.ps.Z, 19960411
Challenges to Programming Language Semantics David A. Schmidt Kansas State University 1 Complementary Semantics Definitions and Abstract Interpretation The development and initial successes of Scott-Strachey denotational semantics in the 1970s gave hope to those who desired a canonical definition format
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/lecture23.ps.gz, 19960415
Last Time ... data flow coverage Today inter-procedural data flow testing assignment 3 part A specification-based testing Is it Better Some Data for 14 mathematical programs random : 35 test cases, 93.7% bugs found branch : 3.8 test cases, 91.6% bugs found all-uses : 11.3 test cases, 96.3% bugs found
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture19.ps, 19960416
Operand mutations Constant replacement e.g., x := x + 5; would replace 5 with each constant of the appropriate type that appears in the program Scalar variable replacement e.g., x := x + 5; would replace x with each scalar variable of the appropriate type that appears in the program Operand mutations
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/Chap7.ps, 19960426
Chapter 7 Verification Page 135 Specification and Verification 1991 7. Verification This chapter opens a new direction of study. Verification is companion to specifications. Verification is a demonstration that two assertions are consistent (that is, they are in agreement). Three applications of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/771/Chap7.ps, 19960426
Chapter 7 Verification Page 135 Specification and Verification 1991 7. Verification This chapter opens a new direction of study. Verification is companion to specifications. Verification is a demonstration that two assertions are consistent (that is, they are in agreement). Three applications of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/771/Chap7.ps, 19960426
Chapter 7 Verification Page 135 Specification and Verification 1991 7. Verification This chapter opens a new direction of study. Verification is companion to specifications. Verification is a demonstration that two assertions are consistent (that is, they are in agreement). Three applications of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/inter-task.ps, 19960506
task T2 is begin accept a; s4; end T2; task T1 is begin s1; T1.a; s2; s3; end T1;
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/possible.ps, 19960506
task T1 is begin s1; T1.a; s2; s3; end T1; task T2 is begin accept a; s4; end T2; (-,a) (s1,-) (T2.a,-) (s1,a) (T2.a,a) (s2,s4) (s3,s4) (s2,-) (-,s4) (s3,-)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/asynch-task.ps, 19960506
task T2 is begin accept a; s4; end T2; task T1 is begin s1; T1.a; s2; s3; end T1;
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/asynch-task.ps, 19960506
task T2 is begin accept a; s4; end T2; task T1 is begin s1; T1.a; s2; s3; end T1;
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/possible.ps, 19960506
task T1 is begin s1; T1.a; s2; s3; end T1; task T2 is begin accept a; s4; end T2; (-,a) (s1,-) (T2.a,-) (s1,a) (T2.a,a) (s2,s4) (s3,s4) (s2,-) (-,s4) (s3,-)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/task-cfgs.ps, 19960506
task T1 is begin s1; T1.a; s2; s3; end T1; task T2 is begin accept a; s4; end T2;
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/cis841/task-cfgs.ps, 19960506
task T1 is begin s1; T1.a; s2; s3; end T1; task T2 is begin accept a; s4; end T2;
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/inter-task.ps, 19960506
task T2 is begin accept a; s4; end T2; task T1 is begin s1; T1.a; s2; s3; end T1;
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis841/lecture30.ps.gz, 19960510
Last Time ... we talked about ... static analysis of concurrent software coverage criteria for concurrent software Today recap of course material preparation for the final details about the final Learning Objectives Understand fundamental concepts What, why, how Understand variation in V&V techniques
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/GradInfo/PhD.manual.ps, 19960517
GUIDELINES FOR THE DEGREE OF DOCTOR OF PHILOSOPHY IN THE DEPARTMENT OF COMPUTING AND INFORMATION SCIENCES KANSAS STATE UNIVERSITY May 1996 GRADUATE STUDIES COMMITTEE Dr. Rodney Howell - Chair Dr. Masaaki Mizuno Dr. Allen Stoughton Dr. David Gustafson - 2 - 1. INTRODUCTION 1a. This document describes
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/GradInfo/PhD.manual.ps, 19960517
GUIDELINES FOR THE DEGREE OF DOCTOR OF PHILOSOPHY IN THE DEPARTMENT OF COMPUTING AND INFORMATION SCIENCES KANSAS STATE UNIVERSITY May 1996 GRADUATE STUDIES COMMITTEE Dr. Rodney Howell - Chair Dr. Masaaki Mizuno Dr. Allen Stoughton Dr. David Gustafson - 2 - 1. INTRODUCTION 1a. This document describes
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/aics.ps, 19960524
An Application-Independent Concurrency Skeleton in Ada-95 Matthew B. Dwyer Matthew J. Craig Eric Runquist Department of Computing and Information Sciences Kansas State University TR 96-7 May 24, 1996
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/aics.ps, 19960524
An Application-Independent Concurrency Skeleton in Ada-95 Matthew B. Dwyer Matthew J. Craig Eric Runquist Department of Computing and Information Sciences Kansas State University TR 96-7 May 24, 1996
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/GradInfo/application-form.ps, 19960710
Directions for Applying for Graduate Programs (July 1996) Name: ___________________________________________________________________________________ (Please print) Family Name First Name Initial Submit complete application materials to: Graduate Studies Department of Computing & Information Sciences 234
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/GradInfo/application-form.ps, 19960710
Directions for Applying for Graduate Programs (July 1996) Name: ___________________________________________________________________________________ (Please print) Family Name First Name Initial Submit complete application materials to: Graduate Studies Department of Computing & Information Sciences 234
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/pdcs96.ps, 19960711
A Complete Set of Satisfaction Rules for Property Detection in Distributed Computations Michel Hurfin Masaaki Mizuno y IRISA Dept. of Comp. and Info. Sciences Campus Universitaire de Beaulieu Kansas State University 35042 Rennes Cedex, France Manhattan, KS 66506 hurfin@irisa.fr masaaki@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/pdcs96.ps, 19960711
A Complete Set of Satisfaction Rules for Property Detection in Distributed Computations Michel Hurfin Masaaki Mizuno y IRISA Dept. of Comp. and Info. Sciences Campus Universitaire de Beaulieu Kansas State University 35042 Rennes Cedex, France Manhattan, KS 66506 hurfin@irisa.fr masaaki@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/k_coterie94.ps, 19960729
Nondominated K-Coteries for Multiple Mutual Exclusion Mitchell L. Neilsen Masaaki Mizuno * Computer Science Dept. Dept. of Comp. and Info. Science Oklahoma State University Kansas State University Stillwater, OK 74078 Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/k_coterie94.ps, 19960729
Nondominated K-Coteries for Multiple Mutual Exclusion Mitchell L. Neilsen Masaaki Mizuno * Computer Science Dept. Dept. of Comp. and Info. Science Oklahoma State University Kansas State University Stillwater, OK 74078 Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/flow87.ps, 19960806
INFORMATION FLOW CONTROL IN A DISTRIBUTED OBJECT-ORIENTED SYSTEM WITH STATICALLY BOUND OBJECT VARIABLES1 Masaaki Mizuno and Arthur E. Oldehoeft Department of Computer Science Iowa State University Ames, Iowa 50011 A. INTRODUCTION The modular approach to the design of computer systems has been the
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/mwrw94.ps, 19960806
An MWRW based Strict Two Phase Lock Scheduler Masaaki Mizuno James Z. Zhou Gurdip Singhy Dept. of Computing and Info. Sciences Kansas State University Manhattan, KS 66506. View serializability (VSR) is a correctness criterion in database systems. However, testing whether a history is VSR is an NP
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/opti95.ps, 19960806
An Optimistic Protocol for a Linearizable Distributed Shared Memory System Masaaki Mizuno Dept. of Comp. and Info. Sciences, Kansas State University, Manhattan, KS 66506, USA Mitchell L. Neilsen Computer Science Department, Oklahoma State University, Stillwater, OK 74078, USA Michel Raynaly IRISA,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/flow89.ps, 19960806
A LEAST FIXED POINT APPROACH TO INTER-PROCEDURAL INFORMATION FLOW CONTROL Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506 masaaki@ksuvax1.cis.ksu.edu 1. Introduction Information flow control regulates the flow of information between
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/logrel.ps.gz, 19960806
Mechanizing Logical Relations Allen Stoughtony Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA E-mail: allen@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/consensus91.ps, 19960806
Decentralized Consensus Protocols Mitchell L. Neilsen Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/porgi.ps.gz, 19960806
Porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional logic Allen Stoughtony Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA allen@cis.ksu.edu http://www.cis.ksu.edu/~allen/home.html
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/consensus91.ps, 19960806
Decentralized Consensus Protocols Mitchell L. Neilsen Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/conc_measure92.ps, 19960806
Synchronization and Concurrency Measures for Distributed Computations Michel Raynal Masaaki Mizuno Mitchell L. Neilsen IRISA Dept. of Computing and Info. Sciences Campus de Beaulieu Kansas State University 35042 Rennes-C edex, FRANCE Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/coterie_join92.ps, 19960806
Coterie Join Algorithm Mitchell L. Neilsen Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/analysis_coterie92.ps, 19960806
Measures of Node Importance for Quorum Structures Mitchell L. Neilsen Masaaki Mizuno Computer Science Department Dept. of Comp. and Info. Sci. Oklahoma State University Kansas State University Stillwater, Oklahoma 74078 Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/token_mx91.ps, 19960806
A Token Based Distributed Mutual Exclusion Algorithm based on Quorum Agreements Masaaki Mizuno* Mitchell L. Neilsen Raghavendra Rao Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/secure_quorum.ps, 19960806
A SECURE QUORUM PROTOCOL Masaaki Mizunoy Mitchell L. Neilsen Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506 In a distributed database system, several copies (replicas) of a data object may be maintained at different sites to improve fault tolerance
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/logrel.ps.gz, 19960806
Mechanizing Logical Relations Allen Stoughtony Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA E-mail: allen@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/flow87.ps, 19960806
INFORMATION FLOW CONTROL IN A DISTRIBUTED OBJECT-ORIENTED SYSTEM WITH STATICALLY BOUND OBJECT VARIABLES1 Masaaki Mizuno and Arthur E. Oldehoeft Department of Computer Science Iowa State University Ames, Iowa 50011 A. INTRODUCTION The modular approach to the design of computer systems has been the
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/mwrw94.ps, 19960806
An MWRW based Strict Two Phase Lock Scheduler Masaaki Mizuno James Z. Zhou Gurdip Singhy Dept. of Computing and Info. Sciences Kansas State University Manhattan, KS 66506. View serializability (VSR) is a correctness criterion in database systems. However, testing whether a history is VSR is an NP
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/coterie_join92.ps, 19960806
Coterie Join Algorithm Mitchell L. Neilsen Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/porgi.ps.gz, 19960806
Porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional logic Allen Stoughtony Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA allen@cis.ksu.edu http://www.cis.ksu.edu/~allen/home.html
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/analysis_coterie92.ps, 19960806
Measures of Node Importance for Quorum Structures Mitchell L. Neilsen Masaaki Mizuno Computer Science Department Dept. of Comp. and Info. Sci. Oklahoma State University Kansas State University Stillwater, Oklahoma 74078 Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/sc_theory95.ps, 19960806
Sequential Consistency in Distributed Systems Masaaki Mizuno1 Michel Raynal2 James Z. Zhou1 1 Dept. of Computing and Info. Sciences, Kansas State University, Manhattan, KS 66506. 2 IRISA, Campus de Beaulieu, 35042 Rennes Cedex, France
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/secure_quorum.ps, 19960806
A SECURE QUORUM PROTOCOL Masaaki Mizunoy Mitchell L. Neilsen Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506 In a distributed database system, several copies (replicas) of a data object may be maintained at different sites to improve fault tolerance
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/opti95.ps, 19960806
An Optimistic Protocol for a Linearizable Distributed Shared Memory System Masaaki Mizuno Dept. of Comp. and Info. Sciences, Kansas State University, Manhattan, KS 66506, USA Mitchell L. Neilsen Computer Science Department, Oklahoma State University, Stillwater, OK 74078, USA Michel Raynaly IRISA,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/conc_measure92.ps, 19960806
Synchronization and Concurrency Measures for Distributed Computations Michel Raynal Masaaki Mizuno Mitchell L. Neilsen IRISA Dept. of Computing and Info. Sciences Campus de Beaulieu Kansas State University 35042 Rennes-C edex, FRANCE Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/token_mx91.ps, 19960806
A Token Based Distributed Mutual Exclusion Algorithm based on Quorum Agreements Masaaki Mizuno* Mitchell L. Neilsen Raghavendra Rao Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/icdcs96.ps, 19960806
Lock Based Self-Stabilizing Distributed Mutual Exclusion Algorithms Masaaki Mizuno Mikhail Nesterenko Hirotsugu Kakugaway Dept. of Comp. and Info. Sciences Dept. of Elect. Engineering Kansas State University Hiroshima University Manhattan, Kansas 66506 Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/sc_theory95.ps, 19960806
Sequential Consistency in Distributed Systems Masaaki Mizuno1 Michel Raynal2 James Z. Zhou1 1 Dept. of Computing and Info. Sciences, Kansas State University, Manhattan, KS 66506. 2 IRISA, Campus de Beaulieu, 35042 Rennes Cedex, France
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/dag91.ps, 19960806
A Dag-Based Algorithm for Distributed Mutual Exclusion Mitchell L. Neilsen Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/icdcs96.ps, 19960806
Lock Based Self-Stabilizing Distributed Mutual Exclusion Algorithms Masaaki Mizuno Mikhail Nesterenko Hirotsugu Kakugaway Dept. of Comp. and Info. Sciences Dept. of Elect. Engineering Kansas State University Hiroshima University Manhattan, Kansas 66506 Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/flow89.ps, 19960806
A LEAST FIXED POINT APPROACH TO INTER-PROCEDURAL INFORMATION FLOW CONTROL Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506 masaaki@ksuvax1.cis.ksu.edu 1. Introduction Information flow control regulates the flow of information between
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/dag91.ps, 19960806
A Dag-Based Algorithm for Distributed Mutual Exclusion Mitchell L. Neilsen Masaaki Mizuno Department of Computing and Information Sciences Kansas State University Manhattan, Kansas 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/coordabs.ps, 19960808
High-Level Coordination Abstractions in Stock Languages CIS TR 96-9 Matthew B. Dwyer Matthew J. Craig Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, KS 66506 (913) 532-6350 dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/coordabs.ps, 19960808
High-Level Coordination Abstractions in Stock Languages CIS TR 96-9 Matthew B. Dwyer Matthew J. Craig Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, KS 66506 (913) 532-6350 dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/cis842/lecture1.ps.gz, 19960821
CIS 842 Specification and Verification of Reactive Systems Matthew B. Dwyer Office: 324e Nichols Hall Email: dwyer@cis.ksu.edu Web: http://www.cis.ksu.edu/ dwyer Phone: (913)532-6350 FAX: (913)532-7353 Hours: MW 2:30-3:30,Thu 2-3 Requirements You'll need WWW access to get to the class web pages You'll
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ln.ps, 19960904
Lecture Notes for Logical Foundations of Programming CIS 301 MICHAEL HUTH Department of Computing and Information Sciences Kansas State University Fall 1996 September 3, 1996 ii Contents 1 Propositional Logic 3 1.1 Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1.1 Declarative
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Unger/tr96-8.ps, 19960923
Event Specification and Detection Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-96-8 June, 1996
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Unger/tr96-8.ps, 19960923
Event Specification and Detection Robert J. Zhang Elizabeth A. Unger Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 {jzhang, beth}@cis.ksu.edu TR CS-96-8 June, 1996
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/FALL96/README.ps, 19961002
A SIMPLE FILE TRANSFER PROTOCOL This program transfers a text file from the Sender to the Receiver using UDP. In order to simulate a lossy channel, there is a Channel process which discards packets at random. The following diagram shows the processes in the Simple File Transfer Protocol. The Sender
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/leno1.ps, 19961006
Chapter 2 Predicate Logic 2.1 The Need for a Richer Logic In the first chapter we developed propositional logic by examining it from three different angles: its proof theory (the natural deduction calculus), its syntax (the tree-like nature of formulas) and its semantics (what these formulas actually
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/boston2.ps.Z, 19961007
On the Need for a Popular Formal Semantics David A. Schmidt Kansas State University Classical music faces a dilemma: as its practitioners specialize into new realms, the field's present-day popularity rests upon the tried-and-true war horses from centuries ago. Among the general populace, there is
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/boston2.ps.Z, 19961007
On the Need for a Popular Formal Semantics David A. Schmidt Kansas State University Classical music faces a dilemma: as its practitioners specialize into new realms, the field's present-day popularity rests upon the tried-and-true war horses from centuries ago. Among the general populace, there is
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/flpd.ps, 19961018
A FUZZY LOWER POWERDOMAIN MICHAEL HUTH Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA The power set of a domain D can be seen as the function space D ! 2 of all functions in the pointwise order. One computational version thereof is the lifted lower
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/flpd.ps, 19961018
A FUZZY LOWER POWERDOMAIN MICHAEL HUTH Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA The power set of a domain D can be seen as the function space D ! 2 of all functions in the pointwise order. One computational version thereof is the lifted lower
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/leno2.ps, 19961021
2.3. SEMANTICS OF PREDICATE LOGIC 75 is as follows. Let I be an interpretation satisfying 8x (P (x) ! Q(x)). We need to show that I satisfies (8x P (x)) ! (8x Q(x)) as well. Inspecting the definition of I j= 1 ! 2 we see that we are done if not every element of our model satisfies P . Otherwise, every
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/kripke/kripke.ps.gz, 19961022
Kripke: a Countermodel Checker for Intuitionistic Propositional Logic Christian Haack Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, Kansas 66506, U.S.A. haack@cis.ksu.edu October 22, 1996 The file kripke.sml" contains an ML-program that generates a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Stoughton/kripke/kripke.ps.gz, 19961022
Kripke: a Countermodel Checker for Intuitionistic Propositional Logic Christian Haack Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, Kansas 66506, U.S.A. haack@cis.ksu.edu October 22, 1996 The file kripke.sml" contains an ML-program that generates a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/lomaps96.ps.Z, 19961104
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/lomaps96.ps.Z, 19961104
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/boston3.ps.Z, 19961112
On the Need for a Popular Formal Semantics David A. Schmidt Kansas State University Computing and Information Sciences Department Manhattan, KS 66506 USA The technology transfer from semantics research to mainstream computing has been hampered by specialization of techniques at the expense of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/boston3.ps.Z, 19961112
On the Need for a Popular Formal Semantics David A. Schmidt Kansas State University Computing and Information Sciences Department Manhattan, KS 66506 USA The technology transfer from semantics research to mainstream computing has been hampered by specialization of techniques at the expense of
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Plexousakis/tr9617.ps, 19961223
Accommodating Integrity Constraints During Database Design * Dimitris Plexousakis Department of Computing and Information Sciences Kansas State University, Manhattan, KS 66506. E-mail: dimitris@cis.ksu.edu John Mylopoulos Department of Computer Science University of Toronto, Toronto, Ont. M5S 1A4,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Plexousakis/tr9617.ps, 19961223
Accommodating Integrity Constraints During Database Design * Dimitris Plexousakis Department of Computing and Information Sciences Kansas State University, Manhattan, KS 66506. E-mail: dimitris@cis.ksu.edu John Mylopoulos Department of Computer Science University of Toronto, Toronto, Ont. M5S 1A4,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/qspm.ps, 19970115
Quantitative Semantics and Possibility Measures Reinhold Heckmann and Michael Huth FB 14 { Informatik, Universit at des Saarlandes Geb. 45, Postfach 151150, D-66041 Saarbr ucken, Germany heckmann@cs.uni-sb.de and Department of Computing and Information Sciences Kansas State University, Manhattan,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/qspm.ps, 19970115
Quantitative Semantics and Possibility Measures Reinhold Heckmann and Michael Huth FB 14 { Informatik, Universit at des Saarlandes Geb. 45, Postfach 151150, D-66041 Saarbr ucken, Germany heckmann@cs.uni-sb.de and Department of Computing and Information Sciences Kansas State University, Manhattan,
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ex3.ps, 19970117
Exam #3, CIS 301 December 18, 1996 1. Let OE be the formula 8x8y9z (R(x; y) ! R(y; z)) where R is a predicate symbol of two arguments. (a) Let A = fa; b; c; dg and RI = f(b; c); (b; b); (b; a)g. Do we have I j= OE Justify your answer whatever it will be! (b) Let A0 = fa; b; cg and RI0 = f(b; c); (a; b);
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ex1.ps, 19970117
Exam #1, CIS 301 September 30, 1996 This is on open book exam. You may use any material you wish to use, except any electronic devices (especially those containing theorem proving software!). 1. Find proofs for the following sequents: (i) ` P ! (Q ! P ) (ii) :P ` P ! Q (iv) R; P ! (R ! Q) ` P ! (Q ^ R)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ex1.ps, 19970117
Exam #1, CIS 301 September 30, 1996 This is on open book exam. You may use any material you wish to use, except any electronic devices (especially those containing theorem proving software!). 1. Find proofs for the following sequents: (i) ` P ! (Q ! P ) (ii) :P ` P ! Q (iv) R; P ! (R ! Q) ` P ! (Q ^ R)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ex3.ps, 19970117
Exam #3, CIS 301 December 18, 1996 1. Let OE be the formula 8x8y9z (R(x; y) ! R(y; z)) where R is a predicate symbol of two arguments. (a) Let A = fa; b; c; dg and RI = f(b; c); (b; b); (b; a)g. Do we have I j= OE Justify your answer whatever it will be! (b) Let A0 = fa; b; cg and RI0 = f(b; c); (a; b);
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ex2.ps, 19970117
Exam #2, CIS 301 November 6, 1996 This is an open book exam. If you have questions about the phrasing of the problems below, please ask! I will try to clarify any ambiguities arising. Make sure that you begin working on a problem only after you have fully understood what exactly you are supposed to do.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ex2.ps, 19970117
Exam #2, CIS 301 November 6, 1996 This is an open book exam. If you have questions about the phrasing of the problems below, please ask! I will try to clarify any ambiguities arising. Make sure that you begin working on a problem only after you have fully understood what exactly you are supposed to do.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw1.ps, 19970129
Homework #1, CIS 301, Spring 1997 Instructor: MICHAEL HUTH Due Date: February 5, 1997; before class This assignment has 10 problems worth one point each (= total of 10 points). 1. Use :, !, ^ and _ to express the following declarative phrases in symbolic logic; in each case state what your respective
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/hw1.ps, 19970129
Homework #1, CIS 301, Spring 1997 Instructor: MICHAEL HUTH Due Date: February 5, 1997; before class This assignment has 10 problems worth one point each (= total of 10 points). 1. Use :, !, ^ and _ to express the following declarative phrases in symbolic logic; in each case state what your respective
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw2.ps, 19970207
Homework #2, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, Feb 12, 1997; before class Find proofs for the following sequents (each proof is worth two points): 1. P _ Q ` R ! ((P _ Q) ^ R) 2. (P ^ Q) _ (P ^ R) ` P ^ (Q _ R) 3. ` (P ! Q) ! ((R ! S) ! (P ^ R ! Q ^ S)); here you might
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw3.ps, 19970212
Homework #3, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, Feb 19, 1997; before class 1. (0:5 points each) Given the following formulas draw their corresponding parse tree: (a) Q (b) ((S _ (:P )) ! (:P )) (c) (S _ ((:P ) ! (:P ))) (d) (((S ! (R _ L)) _ ((:Q) ^ R)) ! ((:(P ! S)) !
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/pdpm.ps, 19970214
MFPS X111 (1997) pages A Powerdomain of Possibility Measures Michael Huth Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA E. N. T. C. S. Elsevier Science B. V.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/pdpm.ps, 19970214
MFPS X111 (1997) pages A Powerdomain of Possibility Measures Michael Huth Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA E. N. T. C. S. Elsevier Science B. V.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw4.ps, 19970215
Homework #4, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, Feb 26, 1997; before class Announcement: The revised line schedule states that our Final Exam will be on Friday, May 16, from 4:10 PM until 6:00 PM in N122 (our usual class room). Our First Exam (open book) will be on
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ex971.ps, 19970226
Exam #1, CIS 301, Spring 1997 Instructor: MICHAEL HUTH This is an open book exam. You have 50 minutes for solving these problems. 1. Use :, !, ^ and _ to express the following declarative phrases in propositional logic; in each case state what your respective propositional atoms P , Q, etc. mean: (a) If
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ex971.ps, 19970226
Exam #1, CIS 301, Spring 1997 Instructor: MICHAEL HUTH This is an open book exam. You have 50 minutes for solving these problems. 1. Use :, !, ^ and _ to express the following declarative phrases in propositional logic; in each case state what your respective propositional atoms P , Q, etc. mean: (a) If
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/wdag96.ps, 19970305
A Timestamp Based Transformation of Self-Stabilizing Programs for Distributed Computing Environments Masaaki Mizuno1 and Hirotsugu Kakugawa2 1 Dept. of Comp. and Info. Sci. Kansas State University, Manhattan, KS 66506 2 Dept. of Elect. Engineering, Hiroshima University, Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/wdag96.ps, 19970305
A Timestamp Based Transformation of Self-Stabilizing Programs for Distributed Computing Environments Masaaki Mizuno1 and Hirotsugu Kakugawa2 1 Dept. of Comp. and Info. Sci. Kansas State University, Manhattan, KS 66506 2 Dept. of Elect. Engineering, Hiroshima University, Higashi-Hiroshima, Japan
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw5.ps, 19970310
Homework #5, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, March 19, 1997; before class Announcement: There will be no class on Wednesday, March 12, and on Friday, March 14. 1. Let m; h; b; a be constants. Further, let F; M;H; S; B be predicate symbols, each with two arguments.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Students/HoweMethod.ps, 19970312
A formal generalization of Howe's method Sergey V. Kotov Report TR-CS-97-3 Kansas State University Department of Computing and Information Sciences Nichols Hall kotov@cis.ksu.edu March 10, 1997 This work is supported by NSF Grant CCR-9302962 1
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Students/HoweMethod.ps, 19970312
A formal generalization of Howe's method Sergey V. Kotov Report TR-CS-97-3 Kansas State University Department of Computing and Information Sciences Nichols Hall kotov@cis.ksu.edu March 10, 1997 This work is supported by NSF Grant CCR-9302962 1
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/qamc.ps, 19970320
Quantitative Analysis and Model Checking Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu Marta Kwiatkowska School of Computer Science University of Birmingham, Edgbaston, B15 2TT, United Kingdom mzk@cs.bham.ac.uk
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/lics97.ps, 19970320
Quantitative Analysis and Model Checking Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu Marta Kwiatkowska School of Computer Science University of Birmingham, Edgbaston, B15 2TT, United Kingdom mzk@cs.bham.ac.uk
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/lics97.ps, 19970320
Quantitative Analysis and Model Checking Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu Marta Kwiatkowska School of Computer Science University of Birmingham, Edgbaston, B15 2TT, United Kingdom mzk@cs.bham.ac.uk
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/afps.ps, 19970320
On the Approximation of Denotational Mu-Semantics Michael Huth Department of Computing and Information Sciences Kansas State University March 19, 1997
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/qamc.ps, 19970320
Quantitative Analysis and Model Checking Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu Marta Kwiatkowska School of Computer Science University of Birmingham, Edgbaston, B15 2TT, United Kingdom mzk@cs.bham.ac.uk
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/afps.ps, 19970320
On the Approximation of Denotational Mu-Semantics Michael Huth Department of Computing and Information Sciences Kansas State University March 19, 1997
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Hankley/Clark.ps, 19970401
April 1, 1997 page 1 A Theory of Types for Natural Language Processing
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Hankley/Clark.ps, 19970401
April 1, 1997 page 1 A Theory of Types for Natural Language Processing
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw7.ps, 19970402
Homework #7, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, April 9, 1997; before class Let zero and one be constants, + and two function symbols with two arguments. Additionally, we consider a predicate symbols P with one argument and predicate symbols <, and = with two arguments.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/hw6.ps, 19970402
Homework #6, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, April 2, 1997; before class Announcement: Have a nice Spring Break! 1. Consider the parsetree of the predicate logic formula OE in the Figure on the back. (a) Specify the free and bound occurrences of variables in OE. (b)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/hw7.ps, 19970402
Homework #7, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, April 9, 1997; before class Let zero and one be constants, + and two function symbols with two arguments. Additionally, we consider a predicate symbols P with one argument and predicate symbols <, and = with two arguments.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw6.ps, 19970402
Homework #6, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Wednesday, April 2, 1997; before class Announcement: Have a nice Spring Break! 1. Consider the parsetree of the predicate logic formula OE in the Figure on the back. (a) Specify the free and bound occurrences of variables in OE. (b)
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/fpags.ps, 19970410
A Framework for Parallel Adaptive Grid Simulations * KSU CIS TR 97-5 Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, KS 66506 (913) 532-6350 dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr96-12.ps, 19970410
A Protocol for Weak Virtual Synchrony Yiwei Chiao Masaaki Mizuno Hemang Nadkarni Dept. of Computing and Info. Sciences Kansas State University Manhattan, KS 66506.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr96-12.ps, 19970410
A Protocol for Weak Virtual Synchrony Yiwei Chiao Masaaki Mizuno Hemang Nadkarni Dept. of Computing and Info. Sciences Kansas State University Manhattan, KS 66506.
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/fpags.ps, 19970410
A Framework for Parallel Adaptive Grid Simulations * KSU CIS TR 97-5 Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, KS 66506 (913) 532-6350 dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw8.ps, 19970414
Homework #8, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Monday, April 21, 1997; before class 1. (2 points each) Prove the following sequents in predicate logic, where P and Q are predicates with one argument: (a) 8x (P (x) ^ Q(x)) ` 8x (P (x) ! Q(x)) (b) 9x (:P (x) ^ :Q(x)) ` 9x (:(P (x) ^
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/hw8.ps, 19970414
Homework #8, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Monday, April 21, 1997; before class 1. (2 points each) Prove the following sequents in predicate logic, where P and Q are predicates with one argument: (a) 8x (P (x) ^ Q(x)) ` 8x (P (x) ! Q(x)) (b) 9x (:P (x) ^ :Q(x)) ` 9x (:(P (x) ^
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/hw9.ps, 19970428
Homework #9, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Monday, April 28, 1997; before class We let Atoms = fP; Q; R; S; Tg be the set of propositional atoms for all systems of this set of exercises. 1. (0.5 points each) Please specify which formulas below are valid CTL formulas and draw a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ann.ps, 19970428
Final Announcements for CIS 301, Spring 1997 Instructor: Michael Huth 1. The deadline for HW#9 has been extended to Friday, May 3, before class. 2. The figure for HW#9 does not tell you which state is s0; this should be the top state with L(s0) = fR; Tg. To streamline the grading process let us say that
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ann.ps, 19970428
Final Announcements for CIS 301, Spring 1997 Instructor: Michael Huth 1. The deadline for HW#9 has been extended to Friday, May 3, before class. 2. The figure for HW#9 does not tell you which state is s0; this should be the top state with L(s0) = fR; Tg. To streamline the grading process let us say that
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/hw9.ps, 19970428
Homework #9, CIS 301, Spring 1997 Instructor: Michael Huth Due Date: Monday, April 28, 1997; before class We let Atoms = fP; Q; R; S; Tg be the set of propositional atoms for all systems of this set of exercises. 1. (0.5 points each) Please specify which formulas below are valid CTL formulas and draw a
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ex972.ps, 19970429
Exam #2, CIS 301, Spring 1997 Instructor: MICHAEL HUTH April 29, 1997 1. Let ffl be a constant symbol. Let head, reverse, and tail be function symbols with one argument; let be a function symbol with two arguments. Further, let = and <= be predicate symbols with two arguments. We interpret these symbols
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ex972.ps, 19970429
Exam #2, CIS 301, Spring 1997 Instructor: MICHAEL HUTH April 29, 1997 1. Let ffl be a constant symbol. Let head, reverse, and tail be function symbols with one argument; let be a function symbol with two arguments. Further, let = and <= be predicate symbols with two arguments. We interpret these symbols
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/ooca.ps, 19970606
Object-Oriented Coordination Abstractions for Parallel Software * Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 Abstract Abstraction is a fundamental concept in software engineering. In this paper, we describe how
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/ooca.ps, 19970606
Object-Oriented Coordination Abstractions for Parallel Software * Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506 Abstract Abstraction is a fundamental concept in software engineering. In this paper, we describe how
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/mcgui.ps, 19970609
Model Checking Graphical User Interfaces Using Abstractions* Matthew B. Dwyer, Vicki Carr, Laura Hines Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/mcgui.ps, 19970609
Model Checking Graphical User Interfaces Using Abstractions* Matthew B. Dwyer, Vicki Carr, Laura Hines Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/wss97.ps, 19970613
Development of Self-Stabilizing Distributed Algorithms using Transformation: Case Studies Hirotsugu Kakugawa 1 Masaaki Mizuno2 Mikhail Nesterenko2 1 Research Institute for Information Science and Education, Hiroshima University, Higashi-Hiroshima, Japan. E-mail: kakugawa@se.hiroshima-u.ac.jp 2
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/wss97.ps, 19970613
Development of Self-Stabilizing Distributed Algorithms using Transformation: Case Studies Hirotsugu Kakugawa 1 Masaaki Mizuno2 Mikhail Nesterenko2 1 Research Institute for Information Science and Education, Hiroshima University, Higashi-Hiroshima, Japan. E-mail: kakugawa@se.hiroshima-u.ac.jp 2
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/wjse97-poster.ps, 19970620
A Framework for Parallel Adaptive Grid Simulations (POSTER) * Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/wjse97-poster.ps, 19970620
A Framework for Parallel Adaptive Grid Simulations (POSTER) * Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Zamfir-Bleyberg/nlksu.ps, 19970626
SENSE TYPED >=-CALCULUS FOR NATURAL LANGUAGE PROCESING Maria Zamfir Bleyberg Clark Sexton Bill Hankley Computing and Information Sciences Department Kansas State University Manhattan, KS, 66506 fmaria,sexton,hankleyg@cis.ksu.edu June 26, 1997
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Zamfir-Bleyberg/nlksu.ps, 19970626
SENSE TYPED >=-CALCULUS FOR NATURAL LANGUAGE PROCESING Maria Zamfir Bleyberg Clark Sexton Bill Hankley Computing and Information Sciences Department Kansas State University Manhattan, KS, 66506 fmaria,sexton,hankleyg@cis.ksu.edu June 26, 1997
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/ta.ps, 19970717
Quantitative Semantics, Topology, and Possibility Measures Reinhold Heckmann FB 14 { Informatik, Universit at des Saarlandes, Postfach 151150, D-66041 Saarbr ucken, Germany Michael Huth Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/ta.ps, 19970717
Quantitative Semantics, Topology, and Possibility Measures Reinhold Heckmann FB 14 { Informatik, Universit at des Saarlandes, Postfach 151150, D-66041 Saarbr ucken, Germany Michael Huth Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/csl.ps, 19970723
A Duality Theory for Quantitative Semantics Reinhold Heckmann FB 14 Informatik, Universit at des Saarlandes Geb. 45, Postfach 151150, D-66041 Saarbr ucken, Germany heckmann@cs.uni-sb.de Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/csl.ps, 19970723
A Duality Theory for Quantitative Semantics Reinhold Heckmann FB 14 Informatik, Universit at des Saarlandes Geb. 45, Postfach 151150, D-66041 Saarbr ucken, Germany heckmann@cs.uni-sb.de Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/cpe97.ps, 19970725
A Framework for Parallel Adaptive Grid Simulations * Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, KS 66506 (913) 532-6350 dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/cpe97.ps, 19970725
A Framework for Parallel Adaptive Grid Simulations * Matthew B. Dwyer and Virgil Wallentine Department of Computing and Information Sciences Kansas State University 234 Nichols Hall Manhattan, KS 66506 (913) 532-6350 dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/aapf.ps, 19970829
Automated Analysis of Software Frameworks (Position Paper) Matthew B. Dwyer Dept. of Computing and Information Science Kansas State University 234 Nichols Hall Manhattan, KS 66506 USA Tel: (913) 532-6350 Fax: (913) 532-7353 Email: dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/aapf.ps, 19970829
Automated Analysis of Software Frameworks (Position Paper) Matthew B. Dwyer Dept. of Computing and Information Science Kansas State University 234 Nichols Hall Manhattan, KS 66506 USA Tel: (913) 532-6350 Fax: (913) 532-7353 Email: dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/spatterns.ps, 19970905
Property Specification Patterns for Finite-State Verification Matthew B. Dwyer Kansas State Universityy George S. Avrunin University of Massachusettsz James C. Corbett University of Hawaiix
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/driving.ps.Z, 19970906
Partial Evaluation of Higher-Order Natural-Semantics Derivations Husain I. Ibraheem and David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/driving.ps.Z, 19970906
Partial Evaluation of Higher-Order Natural-Semantics Derivations Husain I. Ibraheem and David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/modular.ps, 19970914
Modular Flow Analysis for Concurrent Software Matthew B. Dwyer Department of Computing and Information Sciences Kansas State University dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/modflow.ps, 19970914
Modular Flow Analysis for Concurrent Software Matthew B. Dwyer Department of Computing and Information Sciences Kansas State University dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/modflow.ps, 19970914
Modular Flow Analysis for Concurrent Software Matthew B. Dwyer Department of Computing and Information Sciences Kansas State University dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/modular.ps, 19970914
Modular Flow Analysis for Concurrent Software Matthew B. Dwyer Department of Computing and Information Sciences Kansas State University dwyer@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Singh/FALL97/README.ps, 19970918
A SIMPLE FILE TRANSFER PROTOCOL This program transfers a text file from the Sender to the Receiver using UDP. In order to simulate a lossy channel, there is a Channel process which discards packets at random. The following diagram shows the processes in the Simple File Transfer Protocol. The Sender
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Singh/FALL97/README.ps, 19970918
A SIMPLE FILE TRANSFER PROTOCOL This program transfers a text file from the Sender to the Receiver using UDP. In order to simulate a lossy channel, there is a Channel process which discards packets at random. The following diagram shows the processes in the Simple File Transfer Protocol. The Sender
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/filter.ps.Z, 19970919
Limiting State Explosion with Filter-Based Refinement Matthew B. Dwyer and David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr97-14.ps, 19970924
A Transformation of Self-Stabilizing Serial Model Programs for Asynchronous Parallel Computing Environments Masaaki Mizuno Mikhail Nesterenko Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA fmasaaki,mikhailg@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/pdcs97.ps, 19971002
A Protocol for Weak Virtual Synchrony Yiwei Chiao Masaaki Mizuno Hemang Nadkarni Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Dwyer/papers/pefsv.ps, 19971002
Using Partial Evaluation to Enable Verification of Concurrent Software Matthew Dwyer John Hatcliffy Muhammad Nandaz
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/pefsv.ps, 19971002
Using Partial Evaluation to Enable Verification of Concurrent Software Matthew Dwyer John Hatcliffy Muhammad Nandaz
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/pdcs97.ps, 19971002
A Protocol for Weak Virtual Synchrony Yiwei Chiao Masaaki Mizuno Hemang Nadkarni Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/pctl.ps, 19971009
Comparing CTL and PCTL on Labeled Markov Chains Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu Marta Kwiatkowska School of Computer Science University of Birmingham, Edgbaston, B15 2TT, United Kingdom mzk@cs.bham.ac.uk
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/pctl.ps, 19971009
Comparing CTL and PCTL on Labeled Markov Chains Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu Marta Kwiatkowska School of Computer Science University of Birmingham, Edgbaston, B15 2TT, United Kingdom mzk@cs.bham.ac.uk
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/dfa.ps.Z, 19971021
Data Flow Analysis is Model Checking of Abstract Interpretations David A. Schmidt Computing and Information Sciences Department Kansas State University0
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/dfa.ps.Z, 19971021
Data Flow Analysis is Model Checking of Abstract Interpretations David A. Schmidt Computing and Information Sciences Department Kansas State University0
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Zamfir-Bleyberg/mamdb.ps, 19971030
A CATEGORICAL VIEW OF DATABASES Maria Zamfir Bleyberg Computing and Information Sciences Department Kansas State University, Manhattan, KS 66506-2302, USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Zamfir-Bleyberg/mamdb.ps, 19971030
A CATEGORICAL VIEW OF DATABASES Maria Zamfir Bleyberg Computing and Information Sciences Department Kansas State University, Manhattan, KS 66506-2302, USA
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Huth/idmm.ps, 19971121
The Interval Domain: A Matchmaker for aCTL and aPCTL Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Huth/idmm.ps, 19971121
The Interval Domain: A Matchmaker for aCTL and aPCTL Michael Huth Department of Computing and Information Sciences Kansas State University, Manhattan, KS66506, USA huth@cis.ksu.edu
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Dwyer/papers/spatterns.ps, 19971123
Property Specification Patterns for Finite-State Verification Matthew B. Dwyer Kansas State University Department of Computing and Information Sciences 234 Nichols Hall Manhattan, KS 66506-2302 dwyer@cis.ksu.edu George S. Avrunin University of Massachusetts Department of Mathematics and Statistics Box
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Howell/papers/ssbv.ps.gz, 19980109
Finite-State Self-Stabilizing Protocols in Message-Passing Systems Rodney R. Howell Mikhail Nesterenko Masaaki Mizuno Dept. of Computing and Information Sciences Kansas State University Manhattan, KS 66506 January 9, 1998
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Howell/papers/ssbv.ps.gz, 19980109
Finite-State Self-Stabilizing Protocols in Message-Passing Systems Rodney R. Howell Mikhail Nesterenko Masaaki Mizuno Dept. of Computing and Information Sciences Kansas State University Manhattan, KS 66506 January 9, 1998
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Mizuno/tr98-1.ps, 19980114
Finite-State Self-Stabilizing Protocols in Message-Passing Systems Rodney R. Howell Mikhail Nesterenko Masaaki Mizuno Dept. of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr98-1.ps, 19980114
Finite-State Self-Stabilizing Protocols in Message-Passing Systems Rodney R. Howell Mikhail Nesterenko Masaaki Mizuno Dept. of Computing and Information Sciences Kansas State University Manhattan, KS 66506
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Schmidt/papers/aiosh.ps.Z, 19980122
Trace-Based Abstract Interpretation of Operational Semantics David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/papers/aiosh.ps.Z, 19980122
Trace-Based Abstract Interpretation of Operational Semantics David A. Schmidt Kansas State University
open this document and view contentsftp://ftp.cis.ksu.edu/pub/techreports/Mizuno/tr97-14.ps, 19980128
A Transformation of Self-Stabilizing Serial Model Programs for Asynchronous Parallel Computing Environments Masaaki Mizuno Mikhail Nesterenko Department of Computing and Information Sciences Kansas State University Manhattan, KS 66506, USA fmasaaki,mikhailg@cis.ksu.edu