
Zhanping Chen; Student Member; Kaushik Roy; Senior Member; TanLi Chou
Power dissipation in CMOS circuits is heavily dependent on the signal properties of the primary inputs. Due to uncertainties in specification of such properties, the average power should be specified between a maximum and a minimum possible value. Due to the complex nature of the problem, it is practically impossible to use traditional power estimation techniques to determine such bounds. In this paper, we present a novel approach to accurately estimate the maximum and minimum bounds for average power using a technique which calculates the sensitivities of average power dissipation to uncertainties in specification of primary input signal properties. The...

Paola Bruscoli; Francesca Levi; Giorgio Levi; Maria Chiara Meo
In this paper we define a new compilative version of constructive negation (intensional negation) in CLP and we prove its (nonground) correctness and completeness wrt the 3valued completion. We show that intensional negation is essentially equivalent to constructive negation and that it is indeed more efficient, as one would expect from the fact that it is a compilative technique, with the transformation and the associated normalization process being performed once and for all on the source program. We define several formal nonground semantics, based either on the derivation rule or on the least fixpoint of an immediate consequence operator. All...

Christopher T. Haynes; Richard M. Salter
In the presence of firstclass continuations, shallow maintenance of dynamic bindings requires more than the traditional stackbased techniques. This paper provides correctness criteria for such dynamic environments, along with contrasting implementations. A store semantics provides the framework for our correctness criteria and presentation of deep and shallowbinding implementations. The latter implementation is a new statespace algorithm, which is proved correct. A variation of the algorithm implements Scheme's dynamicwind operation. Finally, a technique for maintaining dynamic state called semishallow binding is presented. This compromise between deep and shallowbinding appears suitable for parallel systems. Applications include fluid binding of lexical variables and...

Scott Richard Oksanen; David Chenho Kung; Jyhjong Lin
: A technique is presented for verifying realtime system specifications. A visual conceptual modeling language called ECM is used as a realtime specification language. Specifications are translated into augmented Petri nets with timing and temporal logic constraints. A reachability tree of legal system states is generated from the timing constraints in the Petri net. Past temporal logic constraints are verified using the reachability tree as a record of past states. Future temporal logic constraints are verified dynamically during construction of the reachability tree. 1 Introduction As the size and complexity of software systems grows, so does the potential for errors....

Steve Reeves; Steve Reeves; Steve Reeves
In this paper we propose the design of a tool that will allow the construction of a formal, textual description of a software system even if it has a graphical userinterface as a component. An important aspect of this design is that it can be used for two purposesthe teaching of predicate calculus and the formal specification of graphical userinterfaces. The design has been suggested by considering a system that has already been very successful for teaching predicate logic, namely Tarski's World. 1. Introduction There are now many, welldocumented uses of formal specification in the program development processDiller, 1994; Dromey,...

Giorgio Levi; Davide Ramundo
The paper formally shows that the Ssemantics is adequate for reasoning about the soundness and completeness of real Prolog metainterpreters, based on the nonground representation of objectlevel variables. The paper extends some recent results by De Schreye and Martens, by proving the "equivalence" between the object program and its version metainterpreted by vanilla for any positive logic program. The same construction is applied to obtain a soundness and completeness result for an enhanced metainterpreter defining various inheritance mechanisms on structured logic programs. We then consider the specialization of metainterpreters by means of partial deduction techniques, both in the case of...

Dmitry Y. Zinoviev; Yury A. Polyakov
An integrated multipurpose setup for the automated testing of superconductor devices and circuits has been designed, implemented, and installed in the RSFQ Laboratory of the State University of New York at Stony Brook. The extendable and modular design of the setup allows a wide variety of lowfrequency superconductor experiments to be carried out including those that require immediate interaction between the setup and the researcher. I. Motivation The recent rapid progress in the field of superconductor electronics, particularly of Rapid Single Flux Quantum (RSFQ) logic and memory devices [1], has required adequate testing equipment that would flexibly accommodate the needs...

Peter Buneman; Leonid Libkin; Dan Suciu; Val Tannen; Limsoon Wong
. The syntax of comprehensions is very close to the syntax of a number of practical database query languages and is, we believe, a better starting point than firstorder logic for the development of database languages. We give an informal account of a language based on comprehension syntax that deals uniformly with a variety of collection types; it also includes pattern matching, variant types and function definition. We show, again informally, how comprehension syntax is a natural fragment of structural recursion, a much more powerful programming paradigm for collection types. We also show that a very small "abstract syntax language"...

B. M. Lawal; D. R. Gilbert; A. A. Letichevsky
This paper describes the design of a web based scheduler program and its implementation in the constraint logic programming language clp(FD). We give a formal description of this implementation using the interaction semantics of action languages recently developed by the authors. The clp code employs a port of the PiLLoW library and was compiled via C to executable code (using technology based on wamcc for Prolog) to be run as a CGI script. The implementation is based on the course modules description currently being used in the School of Informatics at City University. It integrates constraints concerning module pre and...

V. Michele Abrusci; Paul Ruet
INTRODUCTION Unrestricted exchange rules of Girard's linear logic [8] force the commutativity of the multiplicative connectives\Omega (times, conjunction) and & (par, disjunction) , and henceforth the commutativity of all logic. This a priori commutativity is not always desirable  it is quite problematic in applications like linguistics or computer science , and actually the desire of a noncommutative logic goes back to the very beginning of LL [9]. Previous works on noncommutativity deal essentially with noncommutative fragments of LL, obtained by removing the exchange rule at all. At that point, a simple remark on the status of exchange in the...

Paul RUET; Paul Ruet; Paul Ruet
This paper presents a sequent calculus for Belnap's fourvalued logic, and proves its soundness and completeness with respect to model theory. The proofs are adaptations of Gallier's proofs for classical logic. It is also shown that the extensions of the classical connectives : and to the fourvalued case do not form a complete set, and a new connective is introduced to obtain the completeness of the connectives. 1 INTRODUCTION The interest of threevalued logic for computer science has been motivated by research on the semantics of negation in logic programming, from the modeltheoretical [4, 11, 12] and the prooftheoretical viewpoints...

Uri Abraham
In the well known timestamp algorithm each writing process reads all the registers of the other processes, and then sets a higher timestamp (natural number) to itself. In the `skewed algorithm' only one writing process in each pair reads the other. Categories and Subjects Descriptors: D.2.4 [Software Engineering]: Programs Verificationcorrectness proofs; F.3.1 [Logic and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs. 1 Preface Messages are often timestamped. In a fax, the timestamp includes the date and exact time of the day, and in a book only the publication year, but in all cases this information guides the...

Denis Bechet; Philippe de Groote; Projet Calligramme
. We state and prove Roorda's interpolation theorem in the framework of proofnet theory. This allows us to transform any proofnet into some other proofnet that matches some given (phonological or prosodic) bracketing. 1 Introduction Almost a decade ago, Girard invented linear logic together with the notion of proofnet [7]. Girard's proofnets have been subsequently adapted to the Lambek calculus by Roorda [16] and, since then, many authors have advocated the notion of proofnet as the right parsing structure in the framework of categorial grammars [11, 13, 14, 16]. Nevertheless, if one wants to take this proposal seriously, one must...

Zinovy Diskin; Zinovy Diskin
. The goal of the paper is to develop a graphical formalism for specifying queries and views within the sketch data model (SkeDM) introduced in [17]. Sketches are directed multigraphs in which some diagrams are labeled with special markers. These markers denote predicates and operations over diagrams of sets and functions. Given a signature of operations (query language), any sketch (database schema) can be extended with derived items denoting data that can be retrieved from the database. Views to a schema S are then sketch morphisms v : SV ! S 0 from some sketch (view schema) SV into an...

B. Le Charlier; C. Leclère; S. Rossi; A. Cortesi
. Program verification is a crucial issue in the field of program development, compilation and debugging. In this paper, we present an analyser for Prolog which aims at verifying whether the execution of a program behaves according to a given specification (behavioural assumptions) . The analyser is based on the methodology of abstract interpretation. A novel notion of abstract sequence is introduced, that includes an overapproximatimation of successful inputs (this is useful to detect mutual exclusion of clauses), and expresses size relation information between successful inputs and the corresponding outputs, together with cardinality information in terms of input argument sizes....

Oliver Matz
. We show that every formula of the existential fragment of monadic secondorder logic over picture models (i.e., finite, twodimensional, coloured grids) is equivalent to one with only one existential monadic quantifier. The corresponding claim is true for the class of word models ([Tho82]) but not for the class of graphs ([Ott95]). The class of picture models is of particular interest because it has been used to show the strictness of the different (and more popular) hierarchy of quantifier alternation. 1 Introduction We study monadic secondorder logic (MSO) over finite structures. For a given class of structures, one can consider...

Hassan AïtKaci; Hassan Atkaci; Rueilmalmaison Cedex; Patrick Lincoln; Patrick Lincoln
Experimenting with formalisms for Natural Language Processing involves costly programming overhead in conventional computing idioms, even as "advanced" as Lisp or Prolog. LIFE (Logic, Inheritance, Functions, and Equations) is a programming language which incorporates an elegant type system which supports a powerful facility for structured type inheritance. Also, LIFE reconciles styles from Functional Programming and Logic Programming by implicitly delegating control to an automatic suspension mechanism. This allows interleaving interpretation of relational and functional expressions which specify abstract structural dependencies on objects. Together, these features provide a convenient and versatile power of abstraction for very highlevel expression of constrained data...

Christopher Landauer
In this note, we report on some work in progress on using rewriting logics for discrete event simulation. The idea is to combine the proofs in the logic with the observations in the simulations to gain a better understanding of the interaction intricacies that seem to occur in complex simulations. In particular, we use communication protocols as our application domain, since they have all the interaction and unpredictability that makes formal specifications difficult. 1 Problem: Formal Methods in Simulation The historical barriers to the use of formal methods in designing and developing communication protocols derive from their different attitudes: verification...

Jan Chomicki; David Toman
The paper proposes a general architecture for implementing temporal integrity constraints by compiling them into a set of active DBMS rules. The modularity of the design allows easy adaptation to different environments. Both differences in the specification languages and in the target rule systems can be easily accommodated. The advantages of this architecture are demonstrated on a particular temporal constraint compiler. This compiler allows automatic translation of integrity constraints formulated in Past Temporal Logic into rules of an active DBMS (in the current version of the compiler two active DBMS are supported: Starburst and INGRES). During the compilation the set...

An An
Introduction To Artificial Life Moshe Sipper Logic Systems Laboratory Swiss Federal Institute of Technology INEcublens CH 1015, Lausanne, Switzerland Can a machine reproduce? Can software be evolved? How are sophisticated robots built to function in a human environment? Can an ecological system be created within a computer? How do flocks of birds fly? These are some of the issues confronted by researchers in Artificial Life (ALife), a young field on the rise that has been gaining acceptance over the past few years. Can a machine reproduce? This question was posed by mathematician John von Neumann in the early 1950s and...