AARNEWS - January 2002



No. 54, January 2002


From the AAR President

New Books

  • Automated Theorem Proving in Software Engineering
  • Handbook of Automated Reasoning
  • Modeling and Verification of Parallel Systems Software
    Call for Papers

  • CADE Workshops
  • Workshop on Complexity in Automated Deduction
  • Advances in Modal Logic
  • 4th Workshop on Hybrid Logics
  • SAT2002
  • WRS 2002
  • TPHOLs 2002
  • Automated Deduction in Geometry

  • Proof-Carrying Code: Special Issue of JAR

    From the AAR President, Larry Wos...

    Welcome to the first palindrome year of the millennium! I trust this will mean not that we go backwards and forwards but that we neatly integrate developments--in theory, implementation, and applications--leading to startling new successes. Among the challenging areas of research in automated reasoning is program verification--particularly of parallel programs; Olga Shumsky Matlin has contributed an interesting article on this topic. Also in this issue are announcements for numerous conferences for the year 2002. It promises to be an exciting year, and I hope that you will contribute some of your research results to the AAR Newsletter and to its companion the Journal of Automated Reasoning.

    New Books

    Automated Theorem Proving in Software Engineering

    Johann M. Schumann has published a new book entitled Automated Theorem Proving in Software Engineering. Using case studies on verification of communication and security protocols and logic-based component reuse, the book demonstrates that state-of-the-art automated theorem provers can handle important tasks automatically during the development of high-quality software. It also provides numerous techniques for increasing practical usability of the automated theorem prover for successful applications.

    Foreword by Donald Loveland
    Springer Verlag, 2001, ISBN 3-540-67989-8
    XIV+228 pp.
    Web site

    Handbook of Automated Reasoning

    The Handbook of Automated Reasoning, edited by J. Alan Robinson and Andrei Voronkov. presents an overview of the fundamental ideas, techniques, and methods in automated reasoning and its applications. The material covers both theory and implementation. In addition to traditional topics, the book covers material that bridges the gap between automated reasoning and related areas. Examples include model checking, nonmonotonic reasoning, numerical constraints, description logics, and implementation of declarative programming languages.

    Volume I

    The Early History of Automated Deduction - Martin Davis, pp. 3-15
    Resolution Theorem Proving - Leo Bachmair and Harald Ganzinger, pp. 19-99
    Tableaux and Related Methods - Reiner Hähnle, pp. 100-178
    The Inverse Method - Anatoli Degtyarev and Andrei Voronkov, pp. 179-272
    Normal Form Transformations - Matthias Baaz, Uwe Egly, and Alexander Leitsch, pp. 273-333
    Computing Small Clause Normal Forms - Andreas Nonnengart and Christoph Weidenbach, pp. 335-367
    Paramodulation-Based Theorem Proving - Robert Nieuwenhuis and Albert Rubio, pp. 371-443
    Unification Theory - Franz Baader and Wayne Snyder, pp. 445-532
    Rewriting - Nachum Dershowitz and David A. Plaisted, pp. 535-610
    Equality Reasoning in Sequent-Based Calculi - Anatoli Degtyarev and Andrei Voronkov, pp. 611-706
    Automated Reasoning in Geometry - Shang-Ching Chou and Xiao-Shan Gao, pp. 707-749
    Solving Numerical Constraints - Alexander Bockmayr and Volker Weispfenning, pp. 751-842
    The Automation of Proof by Mathematical Induction - Alan Bundy, pp. 845-911
    Inductionless Induction - Hubert Comon, pp. 913-962

    Volume II
    Classical Type Theory - Peter B. Andrews, pp. 965-1007
    Higher-Order Unification and Matching - Gilles Dowek, pp. 1009-1062
    Logical Frameworks - Frank Pfenning, pp. 1063-1147
    Proof-Assistants Using Dependent Type Systems - Henk Barendregt and Herman Geuvers, pp. 1149-1238
    Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations - Jürgen Dix, Ulrich Furbach, and Ilkka Niemelä, pp. 1241-1354
    Automated Deduction for Many-Valued Logics - Matthias Baaz, Christian G. Fermüller, and Gernot Salzer, pp. 1355-1402
    Encoding Two-Valued Nonclassical Logics in Classical Logic - Hans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, and Dov M. Gabbay, pp. 1403-1486
    Connections in Nonclassical Logics - Arild Waaler, pp. 1487-1578
    Reasoning in Expressive Description Logics - Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Daniele Nardi, pp. 1581-1634
    Model Checking - Edmund M. Clarke and Bernd-Holger Schlingloff, pp. 1635-1790
    Resolution Decision Procedures - Christian G. Fermüller, Alexander Leitsch, Ullrich Hustadt, and Tanel Tammet, pp. 1791-1849
    Term Indexing - I. V. Ramakrishnan, R. Sekar, and Andrei Voronkov, pp. 1853-1964
    Combining Superposition, Sorts and Splitting - Christoph Weidenbach, pp. 1965-2013
    Model Elimination and Connection Tableau Procedures - Reinhold Letz and Gernot Stenz, pp. 2015-2114

    6 1/2 x 9 1/2, 2150 pp.
    Elsevier Science and
    MIT Press, 2001
    two-volume set cloth ISBN 0-262-18223-8
    Vol. 1, 981 pp., ISBN 0-262-18221-1
    Vol. 2, 1169 pp., ISBN 0-262-18222-X

    For further information, please see the Web page.

    Modeling and Verification of Parallel Systems Software

    Olga Shumsky Matlin
    Argonne National Laboratory

    1. Introduction

    Reasoning about parallel programs is surprisingly difficult. Even small parallel programs are difficult to write correctly, and an incorrect parallel program is equally difficult to debug. This characterization has been borne out in experiences with writing the Multi-Purpose Daemon (MPD): despite MPD's small size and apparent simplicity, errors have impeded progress toward correct code. Such a situation led to exploration of program verification techniques.

    MPD [1] is a process manager for parallel programs and is itself a parallel program. Its function is to start the processes of a parallel job, manage input and output, deal with faults, provide services to the application, and cause jobs to terminate cleanly. MPD is the sort of process manager needed to run applications that use the standard MPI [3] library for parallelism, although it is not MPI-specific.

    Our attempt to use formal verification techniques to ensure correctness of MPD algorithms employs the model checker SPIN [4], which supports design and verification of asynchronous distributed communicating systems. Models of such systems are recorded in a special high-level verification language PROMELA, which can also be used to state some correctness properties of the models. Additional correctness properties are specified by using linear temporal logic (LTL). The verification engine of SPIN is based on on-the-fly reachability analysis with several optimizations and heuristics. The system also includes a simulation environment and a graphical user interface.

    2. Modeling Components of the MPD System

    The MPD system consists of several types of processes (called daemon, manager, console, and client) that communicate over Unix sockets and pipes. Daemons and managers are connected in a ring. A typical setup of the MPD system is shown in Figure 1.

    Figure 1. Daemons with console process, managers, and clients

    MPD algorithms execute on daemons and managers. Daemons and managers execute in essentially infinite loop: they receive messages on their connections and perform actions depending on the type of the received message. The actions are relatively simple and typically involve sending another message. Thus, daemons and managers are viewed and modeled in three layers. On the first layer is the main loop that allows to select a message from one of the attached communication connections. The middle layer is the collection of algorithms that are executed in response to each defined message type. The bottom layer is the mechanism that allows messages to travel from one process to another. The real MPD system relies on Unix sockets for communication between the processes, and the operating system provides all the necessary services.

    The MPD algorithms that we would like to verify thus reside in the middle layer of the three-tiered model. To proceed with verification, we must model not only the algorithms of interest but also the interprocess communication of the bottom level; that is, we have to create a Promela model of Unix sockets. Success of verification attempts depends on the efficiency of the underlying model, and so creation of an efficient Promela model of sockets was important. Several Promela models of socket handling functions were tried. Finally, we created a reusable general-purpose library of Unix socket functions. The library contains implementations of the socket functions connect, accept, read, write, close, and select. These functions provide the interface between the interprocess communication layer of the three-tiered model and the middle layer where the algorithms reside. A different implementation of the socket library can be used, if desired, without making any changes to the model of the algorithms.

    3. Verification of MPD Algorithms

    We considered algorithms that reside on different levels of the MPD system. Two related daemon-level algorithms were modeled: an algorithm for simultaneously inserting new members into a ring of daemons and an algorithm for a recovery of the ring after a single nondeterministic daemon failure. Each of the two algorithms was verified against two correctness properties. The first property (state) is a static check that the information contained in the underlying data structures indeed represents a properly connected ring. The second property (trace) is that a special purpose ring traversal algorithm completes after having visited each member of the ring. We also modeled a manager-level algorithm to provide a synchronization service to the client application processes. A correctness property, stating that no client is allowed to proceed past the synchronization point until all clients have reached the synchronization point, was proved for the algorithm with SPIN's aid.

    As shown in Table 1, verification succeeded on models of only a small size, especially compared with the real MPD system that can involve hundreds if not thousands of processes. However, since even the most difficult errors can be discovered on models comprising only a few processes, the verification engine of SPIN enables us to verify the algorithms on models that are sufficiently large for our purposes.

    Table 1: Table 1. Summary of verification attempts
      Correctness Maximum
    Algorithm Property Model Size
    Ring insert state 4
    Ring insert trace 4
    Ring recovery state 12
    Ring recovery trace 9
    Synchronization   14

    4. Future Plans

    Currently we use SPIN to explore and verify individual MPD algorithms. However, many things take place in parallel in a running MPD system. Daemons enter and leave the ring, as do managers, different client processes request different services from the managers, and several instances of the same algorithm may be executing simultaneously. Correct interaction of these algorithms is also important. We hope to be able to reason formally about MPD models that consist of several related and interdependent algorithms.

    A long-term goal of this project is to model and verify MPD algorithms and then translate them into C or another programming language, while preserving the verified properties. Ideally, translation should be automated. In order to allow this to happen, the Promela model must not be overly abstract. We compared the C implementation of the barrier algorithm with its specification in Promela. The comparison suggests that the automated translation is feasible.

    The Promela implementation of the the Unix socket library, models of the verified MPD algorithms and a technical report [2] with a more detailed description of the project are available at on the Web site.


    This project is a joint work with E. Lusk and W. McCune. This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Advanced Scientific Computing Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.


    1. R. Butler, W. Gropp, and E. Lusk. ``Components and interfaces of a process management system for parallel programs.'' Parallel Computing, 27:1417-1429, 2001.

    2. O. S. Matlin, E. Lusk, W. McCune. ``SPINning Parallel Systems Software.'' Preprint ANL/MCS-P921-1201. Argonne National Laboratory, 2001.

    3. Message Passing Interface Forum. ``MPI2: A message passing interface standard.'' International Journal of High Performance Computing Applications,12(1-2):1-299, 1998.

    4. Spin Home Page. http://netlib.bell-labs.com/netlib/spin.

    Call for Papers

    CADE Workshops

    Workshop on Complexity in Automated Deduction

    A workshop on "Complexity in Automated Deduction" will take place in conjunction with CADE-18 on July 25-26, 2002, in Copenhagen, Denmark. The workshop will bring together researchers interested in problems at the interface between automated deduction and computational complexity. If you are interested in giving a contributed talk, please send an abstract, preferably as a PostScript attachment, to Miki.Hermann@loria.fr no later than Friday, May 17, 2002.


    The 5th International Workshop on Strategies in Automated Deduction (STRATEGIES 2002) will be held in conjunction with CADE at FLoC in Copenhagen, Denmark, on July 26, 2002.

    Strategies are almost ubiquitous in automated deduction and reasoning systems, because the rules at the heart of such systems are nondeterministic and need to be complemented by strategies, or search plans, responsible for controlling them. The role that search plans play in making the resulting procedures capable of solving efficiently interesting problems is no less than that played by the inference systems themselves, since typical deduction paradigms (e.g., generation of consequences, subgoal-reduction, generation of instances, case analysis, enumeration) generate very large or infinite spaces of choices.

    These considerations apply to both fully automated systems (theorem provers, model builders, rewriting engines, decision procedures) and interactive ones (proof assistants and verification systems) and affect them at all levels, from abstract definition to design and implementation. The combination of automated components (e.g., theorem provers and decision procedures) as well as their integration within interactive systems to generate the reasoning environments of the future poses new control problems and puts the study of strategies at the forefront.

    The workshop on Strategies in Automated Deduction is the primary forum for the communication of new results on control strategies and search plans in automated theorem proving, automated model building, decision procedures, interactive proof assistants, proof planners, and logical frameworks and in first-order (including propositional and purely equational as special cases),, modal (e.g., temporal) and higher-order logics. Sample topics include the following:


  • Models of search spaces and languages or mathematical formalisms to define search plans and prove their properties
  • Analysis of the search space (e.g., regularities, symmetries, classification, stratification)
  • Strategy analysis (e.g., formal approaches for the machine-independent evaluation and comparison of deduction strategies)
  • Definition, design, implementation and application:

  • Metalevel features (e.g., preprocessing, compilation, lemmatization, caching, usage of semantics or domain knowledge)
  • Strategies in (existing) systems (e.g., implementation of the proof search model, flexibility and programmability of strategies, role of the user)
  • Applications and case studies in which strategies play a major role
  • Specialization and integration:

  • Strategies devoted to specific theories including inductive theories, arithmetic, decidable theories, and combinations thereof
  • Control issues and strategies in the integration of systems
  • Authors are invited to submit an extended abstract of up to 10 pages. Researchers interested in attending the workshop without giving a talk are invited to send a position paper of 1--2 pages. All submissions should be sent to the Program Chairs (strategies02@cs.uiowa.edu) in Postscript before April 22, 2002. Accepted contributions will be included in the workshop proceedings, which will be available at the workshop and on the Web.

    Based on the submissions, the Program Chairs will consider the possibility of a postworkshop publication (e.g., a special issue of a journal or a volume in a series of electronic proceedings), where authors may submit full versions of the workshop papers. This may involve another call for papers and refereeing process.

    Attendance is by invitation only but late requests for participation will be considered.

    For further information, please see the STRATEGIES 2002 Web site and the CADE 2002 Web site.

    Advances in Modal Logic

    Advances in Modal Logic will be held September 30 - October 2, 2002, in Toulouse, France. AiML 2002 is part of an initiative aimed at presenting an up-to-date picture of the state of the art in modal logic and its many applications. Topics of interest include the following: complexity and decidability of modal and temporal logics, deontic logic, description logics, dynamic logic, epistemic logic, modal logic and game theory, modal logic and grammar formalisms, modal realism and antirealism, modal and temporal logic programming and theorem proving, model theory and proof theory of modal and temporal logic, representation of time in natural language semantics, nonmonotonic modal logics, provability logic, and common-sense temporal reasoning. During the workshop there also will be a special session on modal logics of space.

    Authors are invited to submit a detailed abstract of a full paper of at most 10 pages (a4paper, 11pt) by e-mail to one of the program chairs (Nobu-Yuki Suzuki, smnsuzu@ipc.shizuoka.ac.jp, or Frank Wolter, wolter@informatik.uni-leipzig.de) using `AiML Submission' as the subject line. Submissions must be received no later than May 15, 2002. Note that at least one author of each accepted paper is required to register for and attend the conference to present the paper. Preliminary versions of the full papers should be made available at the workshop; the proceedings volumes will be submitted to CSLI Publications.

    Information about AiML-2002 can be obtained at the Web site.

    4th Workshop on Hybrid Logics

    A workshop on "Hybrid Logics" will take place at LICS 2002, on July 25, 2002, in Copenhagen, Denmark. Hybrid logic is a branch of modal logic in which it is possible to directly refer to worlds, times, states, or whatever the elements of the (Kripke) model are meant to represent. Although they date back to the late 1960s and have been sporadically investigated ever since, it is only in the 1990s that work on them really got into its stride. The workshop is relevant to a wide range of people, including those interested in description logic, feature logic, applied modal logics, temporal logic, and labeled deduction. Moreover, the workshop is devoted to exploring ideas Prior first introduced 30 years ago: it will be an ideal opportunity to see how his ideas have been developed in the intervening period. Contributions in the form of an extended abstract (up to 10 A4 size pages) should be sent in PostScript format to carlos@science.uva.nl before April 26, 2002. Please note that all workshop contributors are required by the LICS organizers to register for FLoC 2002. Visit the Web site for further information.


    The 5th International Symposium on the Theory and Applications of Satisfiability Testing will take place on May 6-9, 2001, in Cincinnati, Ohio, USA. Several aspects of satisfiability testing will be explored including propositional proof systems, search techniques, relationship between BDDs and search, applications such as in formal verification, probabilistic analysis of SAT algorithms and SAT properties, upper bounds on SAT algorithm performance, specific solvers, empirical results, and quantified Boolean formulas. Extended abstracts are due February 6, 2002.

    There will also be a mini-workshop on QBF.

    In conjunction with the symposium, there will be an SAT Solver Competition (BDD packages welcome). SAT solvers and benchmarks are due March 6, 2002. See the symposium home page for further details.

    WRS 2002

    The second international workshop on "Reduction Strategies in Rewriting and Programming" will be held in conjunction with RTA 2002 in Copenhagen, Denmark, on July 21, 2002.

    Reduction strategies bridge the gap between unrestricted general rewriting (computation) and (more deterministic) rewriting with particular strategies (programming). Moreover, reduction strategies provide a natural way to go from operational principles (e.g., graph and term rewriting, narrowing, lambda-calculus) and semantics (e.g., normalization, computation of values, infinitary normalization, head-normalization) to implementations of programming languages. Therefore, progress in this area is likely to be of interest not only to the rewriting community, but also to neighboring fields like functional programming, functional-logic programming, and termination proofs of algorithms.

    The workshop seeks to provide a forum for the presentation of recent developments and new research directions (max. 10 pages) as well as discussion of surveys on existing knowledge in this area (no page limit). Topics of interest include theoretical foundations for reduction strategies; strategies in different frameworks (e.g., term rewriting, lambda calculi, constraint solving) and their application in programming; properties of reduction strategies and computation under strategies (e.g., completeness, computability, decidability); interrelations, combinations, and applications of reduction under different strategies; program analysis and other semantics-based optimization techniques dealing with reduction strategies; rewrite systems, tools, and implementations with programmable strategies as an essential concept; specification of reduction strategies in (real) languages; and data structures and implementation techniques for reduction strategies.

    Submissions should be sent in PostScript format to the following e-mail address wrs02@dsic.upv.es before April 15, 2002. Accepted papers will be included in the workshop proceedings that will be available at the workshop, and electronically on the web. A special issue of the Journal of Symbolic Computation on will be designated for revised and extended versions of selected contributions from both WRS 2001 (Utrecht, May 2001) and WRS 2002.

    For further information, please see the Web site.

    TPHOLs 2002

    The 2002 International Conference on Theorem Proving in Higher Order Logics will be held August 20-23, 2002, in Hampton, Virginia, USA. It is being organized jointly by NASA Langley Research Center, ICASE, and Concordia University.

    The program committee welcomes submissions on all aspects of theorem proving in higher-order logics and on related topics in theorem proving and verification. Topics of interest include the following:

    Submissions are invited in two categories: (A) full research paper, and (B) work in progress report. Submissions under category A are due February 22, 2002; they will be fully refereed, and accepted papers will be published as a volume of Springer-Verlag's Lecture Notes in Computer Science series. Submissions under category B are due May 17, 2002; they will not be formally refereed, but their content and relevance will be reviewed. Those submissions accepted will be published in a NASA technical report. Unless otherwise requested, submissions rejected under category A will also be considered for inclusion under category B. Papers should be no more than 16 pages. Details are available from the Web page.


    The fourth international workshop on ``Automated Deduction in Geometry'' will be held in Hagenberg, Austria, on September 4-6, 2002. The ADG workshop provides a forum to exchange ideas and views, to present research results, and to demonstrate software tools.

    Specific topics for ADG 2002 include the following:

    Potential participants of ADG 2002 are invited to submit an extended abstract (3 or more pages) or a full paper by June 3, 2002. Electronic submissions are preferred, and should be sent to the chairman Franz.Winkler@risc.uni-linz.ac.at. Authors of the extended abstracts and full papers accepted for presentation at the workshop will be invited to submit their full or revised papers for publication in the proceedings of ADG 2002 after the workshop. It is expected that the accepted papers will be published as a volume in the LNAI series by Springer-Verlag.

    For further details, please see the Web site.

    Proof-Carrying Code:
    Special Issue of the Journal of Automated Reasoning

    Amy Felty has issued a call for papers for a special issue of the Journal of Aumated Reasoning on proof-carrying code and related approaches that use formal reasoning to enhance safety and reliability of software. Topics of interest include original results and study of tools and methods for proof generation, proof checking, and their integration with code generation/compilation. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. The deadline for submissions is February 22, 2002.

    For further information, please see the Web site.

    prepared by Gail W. Pieper January 2002