NEWSLETTER No. 77, September 2007

From the AAR President
Announcement of CADE Elections
Proposals for Sites for CADE-22 in 2009 Solicited
Call for Participation

From the AAR President, Larry Wos... I am delighted by the number of people interested in becoming CADE trustees. I find their statements most impressive, with their recurring themes of exploring new ideas, encouraging young researchers, seeking new funding, investigating novel applications, and sponsoring awards.

Would it not be marvelous to see the same excitement filling our subsequent issues of this newsletter as well as the Journal of Automated Reasoning! Program verification is mentioned as a challenging area: have you had any successes? I rely on others for implementations: have you implemented any new techniques that will give me more power, for example, to attack my favorite topic in finding shorter proofs? I look forward to hearing from you soon!

Christoph Benzmueller nominated by Geoff Sutcliffe and Larry Paulson
Maria Paola Bonacina Bonacina nominated by Reiner Haehnle and Uli Furbach Furbach
br afelty Amy Felty Felty Felty nominated by Dale Miller and Brigitte Pientka
Robert Nieuwenhuis nominated by Andrei Voronkov and Ashish Tiwari
Brigitte Pientka Pientka nominated by Aaron Stump and Maria Paola Bonacina Bonacina
br vxs Volker Sorge Sorge Sorge nominated by Alan Bundy and Simon Colton Colton
Geoff Sutcliffe Sutcliffe Geoff nominated by Wolfgang Ahrendt and Koen Claessen Koen
Koen voronkov Andrei Voronkov Andrei Voronkov nominated by Konstantin Verchinine and David Toman David

Toman

Toman Statement by Christoph Benzmüller BenzmÃ

Automated deduction is a prestigious subfield of AI and there are numerous examples of mutual fertilization between the automated deduction area and other subfields of AI. Over the past decades automated deduction has become a mature discipline, and our systems have considerably gained in strength. Further impetus is possible by tightening links, for example, by a stronger exploitation of techniques from other AI areas and a tighter integration of our theorem provers with computer algebra techniques and decision procedures. Moreover, we need to explore novel applications, adapt our systems to their specific needs and provide better user interfaces for expert as well as nonexpert users. My own research in the past decade has been driven by such a wide range of interests and activities. Among others these include

• the interactive proof assistant and knowledge based proof planner OMEGA,
• the agent-based OANTS framework supporting a flexible integration of reasoning systems, and and
LI
• application of these systems toward natural language-based based automated proof tutoring in an e-learning scenario. scenario
LI

Statement by Maria Paola Bonacina

Being asked to write a statement for re-election as CADE trustee, I thought I would share a few thoughts about our field, referring to my web page for accomplishments in research, teaching, and service.

We live at a time when it is widely acknowledged that computer technology is everywhere. On the other hand, the intellectual implications of the computing revolution are still not fully understood. Nevertheless, there is a growing awareness of how deeply computer science is changing the entire scientific enterprise, enterpriseincluding the humanities (e.g., Computer Science: Reflections on the Field, Reflections from the Field, Oct. 2004, http://www7.nationalacademies.org/cstb/pub_fcs.html; Towards 2020 Science, Mar. 2006, http://research.microsoft.com/towards2020science; Jeannette M. Wing, Computational Thinking, CACM 49(3):33-35, Mar. 2006, http://www.cs.cmu.edu/~wing/). The scientific paradigm of mathematical theories and physical experiments is increasingly intertwined with the computational paradigm of models, procedures, languages to express them, and computer experiments, and mathematics itself is becoming computational.

Then I keep asking myself: what is the role of automated reasoning in this exciting and challenging landscape? I think that if computer science becomes the "queen and servant" of all sciences, on a par with mathematics, automated reasoning should become the "queen and servant" of all fields of computer science. Automated reasoning should be for computer science the leap forward that quantum computing promises to be for electronics. A scientific endeavor alternates in its history phases of inward-looking, specialistic growth, with phases of open, universalistic development. Automated reasoning has been through a fruitful phase of the first kind and is ready to open up and reassert itself at the center of computer science, in the origin's spirit (to the question "Can machines think?" Alan Turing answered Yes, because the computing of a Turing machine is a kind of thinking). Our mission is to inject reasoning into all computer applications that are sufficiently complex to warrant it, without forgetting that a highest challenge of automated reasoning is reasoning about software and therefore about computing itself. To this end, we need a variety of engines, to be hidden inside applications, to make them more powerful and more beautiful, or to be integrated into reasoning environments that are easy, comfortable and pleasant to play with. Our field is young and full of marvelous challenges: it is with this mixture of reflection and excitement that I am ready to serve again the community as CADE trustee.

Statement by Amy Felty

It is an exciting time to be working in automated reasoning. Techniques and tools are maturing, and the number of applications of of the research and technology in this area is growing rapidly. There is a lot of diversity in our field, which helps make for interesting and fruitful conferences, both CADE and IJCAR. The IJCAR initiative has been quite successful, and I strongly support its continuation. I also strongly support CADE's role in supporting student participation, particularly through the Bledsoe Travel Award. Another strong point of CADE/IJCAR is the associated workshops, which provide the opportunity to bring people together to discuss and learn about specialized areas.

I have participated in CADE at many levels for many years. My first paper appeared in 1988 and my most recent in 2005. I have also published in associated workshops including this year's LFMTP (Logical Frameworks and Metalanguages: Theory and Practice). In 1996, I was the Conference Chair of CADE when it participated in the first FLoC. I believe that FLoC is an excellent way to bring together even more people in related but diverse areas, and I fully support CADE/IJCAR's participation in future FLoC conferences. During the past three years (until May 2007), I have served as Secretary of CADE and Secretary-Treasurer of AAR (Association for Automated Reasoning), during a time of growth for AAR membership. I would like to continue my work with CADE as a trustee and work toward even more visibility and growth.

Statement by Robert Nieuwenhuis

Some conferences focus on a particular class of techniques and any applications of these, e.g., the conference on Rewriting Techniques and Applications (RTA), and other conferences focus on a particular kind of applications, using any kind of techniques, e.g., the conference on Computer-Aided Verification (CAV). CADE, the major forum for discussing all aspects of automated reasoning research, falls under both categories: it includes typical techniques, such as resolution, decision procedures, constraints, SAT, paramodulation, or tableaux, as well as typical applications, such as hardware and software development and verification, databases, mathematical reasoning or linguistics, to name just a few.

Based on my experience as a PC-chair and PC-member of this and other conferences, I believe that it is crucial but not at all easy for a conference like CADE to maintain this leading role in both aspects, as a prestigious, broad, interesting, and attractive event, well known also in the large variety of potential application communities.

Therefore, as a CADE trustee the viewpoint I would bring into discussion and defend is: (i) maintain equally high scientific standards when assessing the applicability and the theoretical quality of submitted work, and (ii) always have one single joint conference (inside FLoC or not) integrating at least CADE, Tableaux and FTP, that is always clearly visible under the same name (I would slightly prefer CADE over IJCAR), combined only with informal satellite workshops for discussing ongoing work.

Statement by Brigitte Pientka

In my view, CADE is the major venue for all aspects of automated reasoning research, and I regard it as the driving force to promote our field. While we should continue our emphasis on theoretical work and system building, I believe we should also reach out and welcome applications of our work in areas such as computer algebra, constraint solving, knowledge representation, mechanization of programming languages, and reasoning about programs. To foster synergy with other related areas, I would like to initiate discussions about collocating CADE with conferences on related areas. Joint events such as IJCAR and collocating with FLOC are also important ways to promote the visibility of our area and demonstrate the impact of our results to the general computer science community at large.

My own research interest is in the theory and practice of logical frameworks. This includes: designing and investigating type theories and logics, building efficient verification and programming tools, and demonstrating their effectiveness using realistic applications. Since 2001, I have regularly published at CADE/IJCAR, ICLP, and, most recently, TPHOLs. In 2003, I received the best paper award at ICLP'03 for my work on higher-order term indexing, and I was invited to give a tutorial at ICLP'06 about my work.

Over the past few years, I have been actively involved in promoting our field, and I recently proposed to organize CADE in Montreal in 2009. Over the previous years I was publicity chair for CADE 2005, PC member (PPDP'04, MFPS'05, ICLP'06, LPAR'07), organizer (2006, 2007) and program chair (2006) of the "Workshop for Logical Frameworks and Meta-theory: Theory and Practice," and area editor (theorem proving) for the Association of Logic Programming Newsletter (since 2005). As a CADE trustee, I intend to continue working toward ensuring that automated reasoning receives the attention it deserves.

Volker Sorge

My main research area is the application of automated reasoning in pure mathematics, in particular in algebraic domains. I have worked extensively on the integration of automated reasoning with other computational and AI methods, such as computer algebra and machine learning. I have organized several workshops at CADE, and regularly publish in CADE, IJCAR, and the Journal of Automated Reasoning. In my role as a Calculemus trustee, I was one of the people responsible for bringing Calculemus into IJCAR 2004. I am therefore very happy that Alan Bundy has nominated me as a CADE trustee.

I believe that CADE is the leading and most influential automated reasoning conference today and that it is particularly pathbreaking in terms of the theoretical results presented. However, in my opinion, the key word "Automated" is often underrepresented in CADE, and I am particularly concerned that there are relatively few papers on implementations and applications at CADE. I strongly believe that CADE has an obligation to preserve the knowledge of advances in implementation techniques and applicability as it is otherwise at risk of being lost. I believe, therefore, that the most critical challenge to the community is to address this current need without damaging CADE's leading position in theory of automated reasoning. I therefore particularly support the IJCAR initiative as it not only exposes the CADE community to techniques outside the core field but also has a broader remit for applications and implementations.

Statement by Geoff Sutcliffe

I believe that the advancement and application of automated reasoning depends on recognizing and supporting the synergetic interaction of theoretical progress, high performance implementation (techniques), and application requirements. I strongly support research and development that leads to effective implemented systems. I expect CADE to remain the major forum for the presentation of new research in all aspects of automated deduction. As such CADE must reflect the depth, breadth, and interaction of all aspects of automated reasoning, to allow a broad automated reasoning community to use CADE as the preferred conference for the presentation of research results. I support CADE's efforts to provide financial assistance that enables young and poor researchers to attend the conference. I endorse CADE's leading role in IJCAR and continued participation in FLoC. I have recently taken on responsibility for publicity for CADE as an organization -- I already am the owner of the cadeinc.org, cadeconference.org, and ijcar.org domains, which are now the entry points to the respective web pages.

I started my academic career at Edith Cowan University in 1986, taught at James Cook University from 1992 to 2001, and am now an associate professor at the University of Miami. I am probably best known in the automated reasoning community for the TPTP Problem Library, the CADE ATP System Competitions (CASC), and the "Empirically Successful" workshop series. Additionally, my "ARTists" research group is active in several aspects of automated reasoning. I have been attending CADE since CADE-10 in 1990 and have hosted CADE twice -- in Australia in 1997 and in Miami in 2003. I have been on the CADE program committee five times.

Statement by Andrei Voronkov

I contributed to research in automated deduction on many levels: by publishing 15 papers at CADE and IJCAR, implementing the theorem prover Vampire, editing the Handbook of Automated Reasoning, organizing many events in the area (LPAR, Dagstuhl Deduction workshops, Workshops on Implementation of Logic, other conferences and workshops), representing IJCAR on the FLoC steering committee, being vice president of CADE Inc. and CADE program chair, and working on applications in industry, including Intel and Microsoft. I attended every CADE/IJCAR since 1992.

There is no doubt that CADE (as constituent of IJCAR, part of FLoC, or by itself) has been and will continue to be the major conference in automated reasoning. In the past some people regarded CADE as either very theoretical or very narrow but in the last years the scope of CADE has changed to the better in every respect.

I have always thought that CADE should attract more papers in the newly developing areas and applications. To this end, in 2002 I nearly doubled the size of the CADE program committee and invited many people from other areas to it. In the same spirit, in 2003 when involved in organizing regular Dagstuhl Deduction workshops, I proposed to rename them in "Deduction and ..." and invited people from other areas.

Now CADE attracts papers on a wide spectrum of topics. Yet I believe it should try to receive more high-quality papers from noncore areas. Indeed, best papers in applications of deduction in verification, constraints, semantic Web, SAT, and program analysis rarely appear at CADE.

We should also try to attract young researchers to the area. To this end, we should start organizing (at least one) annual summer/winter school in automated reasoning involving also lecturers in areas where deduction is or can be used.

There is another aspect in which the work of CADE Inc. should, in my opinion, be improved: financial. CADE has an excellent Woody Bledsoe award program for sponsoring students attending CADE. Nonetheless, I think it is not enough. We should more aggressively seek major funding in the area that would allow us to sponsor events and awards in the area and reduce CADE conference fees.

TPTP v3.3.0 is now available on the Web. The TPTP-v3.3.0.tar.gz file contains the library, including utilities and basic documentation. Full documentation is online.

The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user and be kept informed of such developments, please email Geoff Sutcliffe.

What's New in TPTP v3.3.0

• 920 new FOF problems, in the domains GEO LCL SEU SWV.

• Better header handling in tptp2X

• In SyntaxBNF
  • Removed the lemma_conjecture role
  • Added assumption_record, assumption role, and assumption intro_type
  • Generalized the BNF for defined terms - been commented out so far
  • Added real numbers in scientific notation

The 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2007) will take place in Austin, Texas, on November 11-14, 2007. Early registration will open mid-September; refer to the Web for more information and updates.

FMCAD 2007 is the seventh in a series of conferences on the theory and application of formal methods in hardware and system design and verification. In 2005, the bi-annual FMCAD and sister conference CHARME decided to merge to form an annual conference with a unified community. The resulting unified FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for formally reasoning about computing systems, as well as open challenges therein. FMCAD2007 will include a full day of tutorials and will be collocated with the ACL2 Workshop.

Diagrams 2008

The 5th International Conference on the Theory and Application of Diagrams (Diagrams 2008) will take place in Germany on September 19-21, 2008.

Diagrams is the only conference that provides a united forum for all areas that are concerned with the study of diagrams: for example, architecture, artificial intelligence, cartography, cognitive science, computer science, education, graphic design, history of science, human-computer interaction, linguistics, logic, mathematics, philosophy, psychology, and software modeling.

Diagrams will run in conjunction with the IEEE Symposium on Visual Languages and Human-Centric Computing and the ACM Symposium on Software Visualization as part of Visual Week.

Topics of particular interest to AAR members include the following:

• computational models of reasoning with, and interpretation of, diagrams
• diagram understanding by humans or machines
• reasoning with diagrams
• theoretical aspects of diagrams including, for example, classification and formalization

For further information, see the Web site.

TAP 2008

The second international conference on Tests and Proofs (TAP) will be held on April 9-11, 2008, in Prato (near Florence), Italy. TAP is devoted to the convergence of proofs and tests. It combines ideas from both sides for the advancement of software quality.

To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a program is to run it with the expectation of discovering bugs. The two techniques seem contradictory: if you have proved your program, it's fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope to prove its correctness. Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools. And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity, but in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer.

How does deduction help testing? How does testing help deduction? How can the combination of testing and deduction increase the reach of both? These and topics such as the following are welcome:

• Generation of test data, oracles, or preambles by deductive techniques such as theorem proving, model checking, symbolic execution, constraint logic programming, and so forht forht
LI
• Generation of specifications by deduction deduction
LI
• Verification techniques combining proofs and tests tests
LI
• Program proving with the aid of testing techniques techniques
LI
• Transfer of concepts from testing to proving (e.g., coverage criteria) criteria
LI
• Automatic bug finding finding
LI
• Formal frameworks frameworks
LI
• Tool descriptions and experience reports reports
LI
• Case studies studies
LI

The abstracts are due November 2, 2007; the papers are due November 9, 2007. Submissions should describe previously unpublished work (completed or in progress), including descriptions of research, tools, and applications. Papers must be formatted following the Springer LNCS guidelines and be at most 15 pages long. Submission of papers is via The proceedings are planned to be published within Springer's LNCS series and will be available at the conference.

For further information, please see the Web site, or send email to tap2008@uni-koblenz.de.

The newly formed group Laboratory for Automated Reasoning and Analysis has open Ph.D. positions in the area of automated reasoning and verification. To apply, please contact Viktor Kuncak.

Title of Thesis: Modular Data Structure Verification
Author: Viktor Kuncak
Institution: Massachusetts Institute of Technology
Thesis Supervisor: Martin C. Rinard
Current Web page: http://lara.epfl.ch/~kuncak/papers/Kuncak07DecisionProceduresModularDataStructureVerification.html
Abstract: This dissertation describes an approach for automatically verifying data structures, focusing on techniques for automatically proving formulas that arise in such verification. I have implemented this approach with my colleagues in a verification system called Jahob. Jahob verifies properties of Java programs with dynamically allocated data structures.

Developers write Jahob specifications in classical higher-order logic (HOL); Jahob reduces the verification problem to deciding the validity of HOL formulas. I present a new method for proving HOL formulas by combining automated reasoning techniques. My method consists of (1) splitting formulas into individual HOL conjuncts, (2) soundly approximating each HOL conjunct with a formula in a more tractable fragment, and (3) proving the resulting approximation using a decision procedure or a theorem prover. I present three concrete logics; for each logic I show how to use it to approximate HOL formulas, and how to decide the validity of formulas in this logic.

First, I present an approximation of HOL based on a translation to first-order logic, which enables the use of existing resolution-based theorem provers. Second, I present an approximation of HOL based on field constraint analysis, a new technique that enables decision procedures for special classes of graphs (such as monadic second-order logic over trees) to be applied to arbitrary graphs.

Third, I present an approximation using Boolean Algebra with Presburger Arithmetic (BAPA), a logic that combines reasoning about sets of elements with reasoning about cardinalities of sets. BAPA can express relationships between sizes of data structures and invariants that correlate data structure size with integer variables. I present the first implementation of a BAPA decision procedure, and establish the exact complexity bounds for BAPA and quantifier-free BAPA.

Together, these techniques enabled Jahob to modularly and automatically verify data structure implementations based on singly and doubly-linked lists, trees with parent pointers, priority queues, and hash tables. In particular, Jahob was able to prove that data structure implementations satisfy their specifications, maintain key data structure invariants expressed in a rich logical notation, and never produce run-time errors such as null dereferences or out of bounds accesses.

Title of Thesis: Combined Decision Procedures for Constraint Satisfiability
Author: Enrica Nicolini
Institution: Universita' degli Studi di Milano (Italy)
Date of Defense: Jan. 4, 2007
Current Web page: A pdf file is available from the Web.
Abstract: This thesis is devoted to the study of the decidability of fragments of different logical languages and the transfer of the decidability to their combination. Our work first shows that the universal fragment of the theory of arrays with dimension is decidable, and then it concentrates on combination problems. If we consider the union of two first-order theories over disjoint signatures, we prove that the constraint satisfiability problem (c.s.p.) for the combination of two theories whose c.s.p. is decidable is in general undecidable, but nevertheless it is possible to weaken the standard additional hypothesis of stably infiniteness in order to regain the decidability.

As far as the combination of two theories over non-disjoint signature is concerned, we introduce the notion of noetherianity that, together with the already-known requirement of 'T_0 compatibility,' is sufficient for transferring the decidability of the c.s.p. We also generalize the Nelson-Oppen combination schema by plugging it into a higher-order framework. The main advantage of this choice is the opportunity to consider in a uniform way a large variety of logical fragments, deriving thus new decidability results. As an example, we analyze monodic modal/temporal fragments as combinations of extensional first-order fragments and standard translations of one variable modal/temporal fragments, finally obtaining rather general decidability transfer results.