Peter Schachte's Publications

• Peter Schachte and Harald Søndergaard. Boolean approximation revisited. In Ian Miguel and Wheeler Ruml, editors, Abstraction, Reformulation and Approximation: Proceedings of SARA 2007, volume 4612 of Lecture Notes in Artificial Intelligence, pages 329–343. Springer, 2007.
  Abstract: Most work to date on Boolean approximation assumes that Boolean functions are represented by formulas in conjunctive normal form. That assumption is appropriate for the classical applications of Boolean approximation but potentially limits wider use. We revisit, in a lattice-theoretic setting, so-called envelopes and cores in propositional logic, identifying them with upper and lower closure operators, respectively. This leads to recursive representation-independent characterisations of Boolean approximation for a large class of classes. We show that Boolean development can be applied in a representation-independent setting to develop approximation algorithms for a broad range of Boolean classes, including Horn and Krom functions.
• Amy Beth Corman, Peter Schachte, and Vanessa Teague. A secure group agreement (SGA) protocol for peer-to-peer applications. In AINAW '07: Proceedings of the 21st International Conference on Advanced Information Networking and Applications Workshops, pages 24–29, Washington, DC, USA, May 2007. IEEE Computer Society.
  Abstract: The lack of a trusted central authority poses a unique security challenge to peer-to-peer networks. It must be assumed that some fraction of all peers in a network are corrupt and may collude to try to derive an advantage. Nonetheless, in some circumstances it is necessary to select a subset of the peer-to-peer network in such a way that all members of the selected group can be confident that most group members are honest. We propose a secure protocol for the selection of a subset of peers from the network without a trusted authority. Our protocol ensures, with any desired probability, that the percentage of corrupt members in the subset is no greater than a selected limit (up to the total percentage of corrupt peers). We then discuss the use of this protocol in the context of a peer-to-peer game.
• Khalid Al-Jasser, Peter Schachte, and Ed Kazmierczak. Suitability of object and aspect oriented languages for software maintenance. In Proceedings of the 2007 Australian Software Engineering Conference, pages 117–128, April 2007.
  Abstract: Program maintenance is an important and frequently a difficult part of the software life cycle. One reason for its difficulty is the presence of crosscutting concerns: aspects of a program that cannot be confined to a single program component. Crosscutting concerns defy the standard wisdom of program design that individual components should be highly cohesive (they should address only one concern) and loosely coupled (they should not share concerns with other components). We consider several approaches to a simple maintenance task in both object-oriented and aspect-oriented languages, analyzing how well they maintain high cohesion and low coupling. We conclude that none of these approaches is entirely satisfactory, and present a few changes to aspect oriented programming language design that would better support maintenance in the face of crosscutting concerns.
• Brian Herlihy, Peter Schachte, and Harald Søndergaard. Un-Kleene Boolean equation solving. International Journal of Foundations of Computer Science, 18(2):227–250, April 2007.
  Abstract: We present a new method for finding closed forms of recursive Boolean function definitions. Traditionally, these closed forms are found by Kleene iteration: iterative approximation until a fixed point is reached. Conceptually, our new method replaces each k-ary function by 2^k Boolean constants defined by mutual recursion. The introduction of an exponential number of constants is mitigated by the simplicity of their definitions and by the use of a novel variant of ROBDDs to avoid repeated computation. Experiments suggest that this approach is significantly faster than Kleene iteration for examples that require many Kleene iteration steps.
• Amy Corman, Peter Schachte, and Vanessa Teague. Quip: A protocol for securing content in peer-to-peer publish/subscribe overlay networks. In Gillian Dobbie, editor, Thirtieth Australasian Computer Science Conference (ACSC2007), volume 62 of CRPIT, pages 35–40, Ballarat Australia, 2007. ACS.
  Abstract: Publish/subscribe networks provide an interface for publishers to perform many-to-many communication to subscribers without the inefficiencies of broadcasting. Each subscriber submits a description of the sort of content they are interested in, then the publish/subscribe system delivers any appropriate messages as they are published. Although publish/ subscribe networks offer advantages over traditional web-based content delivery, they also introduce security issues. The two security problems that we solve are: ensuring that subscribers can authenticate the messages they receive from publishers, and ensuring that publishers can control who receives their content. We propose QUIP, a protocol which adds efficient authentication and encryption mechanisms to existing publish/subscribe overlay networks. The idea is to combine an efficient traitor-tracing scheme (by Tzeng and Tzeng (2001)) with a secure key management protocol. This allows publishers to restrict their messages to authorised subscribers and to add and remove subscribers without affecting the keys held by the other subscribers.
• Amy Beth Corman, Scott Douglas, Peter Schachte, and Vanessa Teague. A secure event agreement (SEA) protocol for peer-to-peer games. In The First International Conference on Availability, Reliability and Security (AReS), pages 34–41, 2006.
  Abstract: Secure updates in a peer-to-peer game where all of the players are untrusted offers a unique challenge. We analyse the NEO protocol [5] which was designed to accomplish the exchange of update information among players in a fair and authenticated manner. We show that of the five forms of cheating it was designed to prevent, it prevents only three. We then propose an improved protocol which we call Secure Event Agreement (SEA) which prevents all five types of cheating as well as meeting some additional security criteria. We also show that the performance of SEA is at worst equal to NEO and in some cases better.
• Michael Codish, Vitaly Lagoon, Peter Schachte, and Peter J. Stuckey. Size-change termination analysis in k-bits. In Peter Sestoft, editor, Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, volume 3924 of Lecture Notes in Computer Science, pages 230–245. Springer, 2006.
• Brian Herlihy, Peter Schachte, and Harald Søndergaard. Boolean equation solving as graph traversal. In Joachim Gudmundsson and Barry Jay, editors, Theory of Computing 2006, volume 51 of Conferences in Research and Practice in Information Technology, pages 123–132, 2006.
• Peter Schachte and Harald Søndergaard. Closure operators for ROBDDs. In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 1–16. Springer, Berlin, 2006.
  Abstract: Program analysis commonly makes use of Boolean functions to express information about run-time states. Many important classes of Boolean functions used this way, such as the monotone functions and the Boolean Horn functions, have simple semantic characterisations. They also have well-known syntactic characterisations in terms of Boolean formulae, say, in conjunctive normal form. Here we are concerned with characterisations using binary decision diagrams. Over the last decade, ROBDDs have become popular as representations of Boolean functions, mainly for their algorithmic properties. Assuming ROBDDs as representation, we address the following problems: Given a function ψ and a class of functions Δ, how to find the strongest ϕ ∈ Δ entailed by ψ (when such a ϕ is known to exist)? How to find the weakest ϕ ∈ Δ that entails ψ? How to determine that a function ψ belongs to a class Δ? Answers are important, not only for several program analyses, but for other areas of computer science, where Boolean approximation is used. We give, for many commonly used classes Δ of Boolean functions, algorithms to approximate functions represented as ROBDDs, in the sense described above. The algorithms implement upper closure operators, familiar from abstract interpretation. They immediately lead to algorithms for deciding class membership.
• Peter Schachte. Precise goal-independent abstract interpretation of constraint logic programs. Theoretical Computer Science, 293:557–577, 2003.
  Abstract: We present a goal-independent abstract interpretation framework for pure constraint logic programs, and prove the sufficiency of a set of conditions for abstract domains to ensure that the analysis will never lose precision. Along the way, we formally define pure constraint logic programming systems, give a formal semantics that is independent of the actual constraint domain and the details of the proof algorithm, and formally define the maximally precise abstraction of a pure constraint logic program.
• Peter Schachte. Sequence quantification. In Veronica Dahl and Philip Wadler, editors, Practical Aspects of Declarative Languages, volume 2562 of Lecture Notes in Computer Science, pages 128–144. Springer, Berlin, 2003.
  Abstract: Several earlier papers have shown that bounded quantification is an expressive and comfortable addition to logic programming languages. One shortcoming of bounded quantification, however, is that it does not allow easy and efficient relation of corresponding elements of aggregations being quantified over. Bounded quantification also does not allow easy quantification over part of an aggregation, nor does it make it easy to accumulate a result over an aggregation. We generalize the concept of bounded quantification to quantification over any finite sequence, as we can use a rich family of operations on sequences to create a language facility that avoids the weaknesses mentioned above. We also propose a concrete syntax for sequence quantification in Prolog programs, which we have implemented as a source to source transformation.
• Peter Schachte. Precise goal-independent abstract interpretation of constraint logic programs. In Colin Fidge, editor, Electronic Notes in Theoretical Computer Science, volume 42. Elsevier Science Publishers, 2001.
  Abstract: We present a goal-indpendent abstract interpretation framework for pure constraint logic programs, and prove the sufficiency of a set of conditions for abstract domains to ensure that the analysis will never lose precision. Along the way, we formally define pure constraint logic programming systems, give a formal sementics that is independent of the actual constraint domain, and formally define the maximally precise abstraction of a pure constraint logic program.
• Roberto Bagnara and Peter Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In A. M. Haeberer, editor, Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST'98)”, volume 1548 of Lecture Notes in Computer Science, pages 471–485, Amazonia, Brazil, 1999. Springer, Berlin.
  Abstract: The subject of groundness analysis for (constraint) logic programs has been widely studied, and interesting domains have been proposed. Pos has been recognized as the most suitable domain for capturing the kind of dependencies arising in groundness analysis, and Reduced Ordered Binary Decision Diagrams (ROBDDs) are generally accepted to be the most efficient representation for Pos. Unfortunately, the size of an ROBDDs is, in the worst case, exponential in the number of variables it depends upon. Earlier work has shown that a hybrid representation that separates the definite information from the dependency information is considerably more efficient than keeping the two together. The aim of the present paper is to push this idea further, also separating out certain dependency information, in particular all pairs of variables that are always either both ground or neither ground. We find that this new hybrid representation is a significant improvement over previous work.
• Tania Armstrong, Kim Marriott, Peter Schachte, and Harald Søndergaard. Two classes of Boolean functions for dependency analysis. Science of Computer Programming, 31(1):3–45, May 1998.
  Abstract: Many static analyses for declarative programming/database languages use Boolean functions to express dependencies among variables or argument positions. Examples include groundness analysis, arguably the most important analysis for logic programs, finiteness analysis and functional dependency analysis for databases. We identify two classes of Boolean functions that have been used: positive and definite functions, and we systematically investigate these classes and their efficient implementation for dependency analyses. On the theoretical side we provide syntactic characterizations and study the expressiveness and algebraic properties of the classes. In particular, we show that both are closed under existential quantification. On the practical side we investigate various representations for the classes based on reduced ordered binary decision diagrams (ROBDDs), disjunctive normal form, conjunctive normal form, Blake canonical form, dual Blake canonical form, and a form specific to definite functions. We compare the resulting implementations of groundness analyzers based on the representations for precision and efficiency.
• Roberto Bagnara and Peter Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In J. L. Freire-Nistal, M. Falaschi, and M. Vilares-Ferro, editors, Proceedings of the 1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE '98), pages 227–239, July20–23 1998.
  Abstract: The subject of groundness analysis for (constraint) logic programs has been widely studied, and interesting domains have been proposed. Pos has been recognized as the most suitable domain for capturing the kind of dependencies arising in groundness analysis, and Reduced Ordered Binary Decision Diagrams (ROBDDs) are generally accepted to be the most efficient representation for Pos. Unfortunately, the size of an ROBDDs is, in the worst case, exponential in the number of variables it depends upon. Earlier work [] has shown that a hybrid representation that separates the definite information from the dependency information is considerably more efficient than keeping the two together. The aim of the present paper is to push this idea further, also separating out certain dependency information, in particular all pairs of variables that are always either both ground or neither ground. We find that this new hybrid representation is a significant improvement over previous work.
• Peter Schachte. Global variables in logic programming. In Lee Naish, editor, Logic Programming: Proceedings of the Fourteenth International Conference on Logic Programming., pages 3–17, Cambridge, USA, July 1997. MIT Press.
  Abstract: We show that adding global variables to logic programming can solve some common problems of reliability and programmer productivity in large logic programs. By presenting a formal semantics for logic programs with global variables, we show that this addition retains a clean semantics. This addition has the consequences that conjunction is neither commutative nor absorptive, but we show that the practical loss is small. We also describe an implementation of Prolog with global variables as a translator to ordinary Prolog which preserves the efficiency of the Prolog program, while statically detecting some programming errors, and avoiding others altogether.
• Peter Schachte. Efficient ROBDD operations for program analysis. In Kotagiri Ramamohanarao, editor, ACSC'96: Proceedings of the 19^th Australasian Computer Science Conference, pages 347–356. Australian Computer Science Communications, 1996.
  Abstract: Reduced Ordered Binary Decision Diagrams (ROBDDs), also known as Bryant graphs, are a representation for Boolean functions supporting many efficient operations. Because of this, they have often been used to implement the positive Boolean functions for program analysis. Some ROBDD operations heavily used in program analysis, however, are still rather expensive. The undertaking of the present paper is to develop some more efficient algorithms for a few key ROBDD operations used in program analysis.
• Peter Schachte and Georges Saab. Efficient object-oriented programming in Prolog. In Christoph Beierle and Lutz Plümer, editors, Logic Programming: Formal Methods and Practical Applications, number 11 in Studies in Computer Science and Artificial Intelligence, chapter 7, pages 205–243. Elsevier Science B.V./North-Holland, Amsterdam, 1995.
  Abstract: We discuss classes, a package for efficient object-oriented programming in Prolog. Successive versions are described, along with a discussion of the problems encountered when using the initial version to build application products, and the solutions devised to correct these problems. We also discuss implementation techniques, and how we achieve high performance. Two examples which use the package are included. Comparisons are made with related work.
• Tania Armstrong, Kim Marriott, Peter Schachte, and Harald Søndergaard. Boolean functions for dependency analysis: Algebraic properties and efficient representation. In B. Le Charlier, editor, Static Analysis: Proceedings of the First International Symposium, volume 864 of Lecture Notes in Computer Science, pages 266–280. Springer-Verlag, Berlin, September 1994.
  Abstract: Many analyses for logic programming languages use Boolean functions to express dependencies between variables or argument positions. Examples include groundness analysis, arguably the most important analysis for logic programs, finiteness analysis and functional dependency analysis. We identify two classes of Boolean functions that have been used: positive and definite functions, and we systematically investigate these classes and their efficient implementation for dependency analyses. We provide syntactic characterizations and study their algebraic properties. In particular, we show that both classes are closed under existential quantification. We investigate representations for these classes based on: reduced ordered binary decision diagrams (ROBDDs), disjunctive normal form, conjunctive normal form, Blake canonical form, dual Blake canonical form, and a form specific to definite functions. We give an empirical comparison of these different representations for groundness analysis.
• Peter Schachte and Georges Saab. Efficient object-oriented programming in Prolog. In Leon Sterling, editor, Proceedings of the Second International Conference on Practical Application of Prolog, pages 471–496, London, England, April 1994. Royal Society of Arts.
  Abstract: We discuss classes, a package for efficient object-oriented programming in Prolog. Successive versions are described, along with a discussion of the problems encountered when using the initial version to build application products, and the solutions devised to correct these problems. Two examples which use the package are included.

This document was translated from L^AT_EX by H^EV^EA.