ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER No. 104, September 2013

From the AAR President, Larry Wos…
Maria Paola Bonacina follows Franz Baader as President of CADE
Conferences
Job Opportunities
- Post-doc Position in Trento, Italy
Results of CADE Trustee Elections

From the AAR President, Larry Wos…

Occasionally in mathematics and in logic, the goal is not only to find a proof but also to find a proof with some constraint.

For example, you might be asked to find a proof from a set of axioms all of which are independent, as in group theory when the axioms of right identity and right inverse are omitted. For a second example, you might be asked, as I was by Branden Fitelson, to find for a particular theorem, a proof that avoided various lemmas that are usually present in the literature. For a third example, pertinent to this column, you are asked first to find a proof under no constraints, and then under the constraint that certain terms are avoided. The terms to be avoided are so-called double-negation terms, terms of the form n(n(t)) for some term t, where the function n denotes negation. The area in focus is many-valued, or infinite-valued, sentential calculus. The inference rule is condensed detachment.

I now give a set of three lists – usable, sos, and passive – all pertinent to William McCune's program OTTER. Condensed detachment is found in list(usable), the axioms to be used are found in list(sos), and the target theorems are found, negated, in list(passive).

The key theorem to concentrate on is 44a.

You are asked first to find a proof of that theorem under no constraints, and then – more challenging indeed – under the constraint that no double-negation term is used.

   list(usable).
   -P(i(x,y)) | -P(x) | P(y).
   end_of_list.
   
   list(sos).
   P(i(x,i(y,x))).                   % A1
   P(i(i(x,y),i(i(y,z),i(x,z)))).    % A2
   P(i(i(i(x,y),y),i(i(y,x),x))).    % A3
   P(i(i(n(x),n(y)),i(y,x))).        % A4
   end_of_list.
   
   list(passive).
   -P(i(i(a,b),i(n(b),n(a)))) | $ANS(mv_lemma_a6).
   -P(i(i(n(a),b),i(n(b),a))) | $ANS(mv_lemma_a7).
   -P(i(i(a,n(b)),i(b,n(a)))) | $ANS(mv_lemma_a8).
   -P(i(i(a,n(i(i(n(b),n(c)),n(c)))),n(i(i(n(i(a,b)),n(i(a,c))),n(i(a,c)))))) | $ANS(step_dist_44a).
   end_of_list.

Maria Paola Bonacina follows Franz Baader as President of CADE

Franz Baader's term as CADE trustee expired after the trustee elections 2013, and with that ended his office as president. The new Board of Trustees has elected Maria Paola Bonacina as new president of CADE.

On the behalf of CADE and AAR, I congratulate Maria Paola Bonacina on this honor and opportunity to serve CADE and the field of automated reasoning.

Also on behalf of the AAR and CADE, I would like to thank Franz Baader for his service and commitment as president of CADE during the past three years.

Conferences

FLoC 2014, Federated Logic Conference, Call for Workshop Proposals

The Sixth Federated Logic Conference (FLoC 2014) will be part of the Vienna Summer of Logic (VSL), the largest logic event in history, with over 2000 expected participants. FLoC 2014 will host eight conferences and many workshops. Each workshop will be affiliated with one of the eight conferences.

26th International Conference on Computer Aided Verification (CAV)
Workshop Chair: Martina Seidl
27th IEEE Computer Security Foundations Symposium (CSF)
Workshop Chair: Luca Vigano
30th International Conference on Logic Programming (ICLP)
Workshop Chair: Haifeng Guo
7th International Joint Conference on Automated Reasoning (IJCAR)
Workshop Chair: Matthias Horbach
5th Conference on Interactive Theorem Proving (ITP)
Workshop Chair: David Pichardie
29th ACM/IEEE Symposium on Logic in Computer Science (LICS) joined with the 23rd EACSL Annual Conference on Computer Science Logic (CSL)
Workshop Chair: Georg Moser
25th International Conference on Rewriting Techniques and Applications (RTA) joined with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA)
Workshop Chair: Aleksy Schubert
17th International Conference on Theory and Applications of Satisfiability Testing (SAT)
Workshop Chair: Ines Lynce

Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense. Each workshop proposal must indicate one hosting conference among the participating conferences.

It is suggested that prospective workshop organizers contact the relevant conference Workshop Chair before submitting a proposal. Proposals should be submitted electronically to EasyChair.

The deadline for workshop proposals is 30 September 2013.

Questions regarding workshop proposals should be sent to the workshop chairs of conferences that are supposed to host the workshop (see above). General questions should be sent to floc14cfw@easychair.org. For full details, please refer to the FLoC Workshop Guide.

LPAR-19, Logic for Programming Artificial Intelligence and Reasoning

The 19th edition of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19) will be held in Stellenbosch, South Africa, 14–19 December 2013. LPAR-19 includes five associated workshops:

IWIL-10 - The 10th International Workshop on the Implementation of Logics, Submission deadline: October 14, 2013

APS-7 - The 7th International Workshop on Analytic Proof Systems, Submission deadline: October 14, 2013

ALCS - The 1st International Workshop on Algebraic Logic in Computer Science, Submission deadline: passed

LRCM - The 1st Workshop on Logics and Reasoning for Conceptual Models, Submission deadline: October 14, 2013

ALFA-2 - The 2nd Workshop on Automata, Logic, Formal languages, and Algebra, Submission deadline: September 30

Submissions are still being accepted for most workshops. For further details, please refer to the workshop web pages.

FMCAD 2013, Formal Methods in Computer-Aided Design

FMCAD 2013 will be held in Portland, Oregon, USA on 20–23 October 2013. The conference will be co-located with MEMOCODE 2013, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, and DIFTS 2013, the International Workshop on Design and Implementation of Formal Tools and Systems. DIFTS will be held on October 19. MEMOCODE will take place from October 18 to 19, followed by a joint FMCAD/MEMOCODE tutorial day on October 20. FMCAD will continue from
October 21 to 23, 2013.

FMCAD 2013 is the thirteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.

Early registration will be open until 30 September 2013. Please refer to the conference webs site for details.

LATA 2014, Language and Automata Theory and Applications

LATA 2014, the 8th Intl. Conf. on Language and Automata Theory and Applications will be held in Madrid, Spain on 10–14 March 2014.Topics of either theoretical or applied interest include connections between automata and logic, term rewriting, and others that may be of interest to the AAR community.

The paper submission deadline is 14 October 2013. Accepted papers will be published in a Springer LNCS volume.

Please go to the conference web site for details.

FM 2014, International Symposium on Formal Methods

FM 2014, the 19th International Symposium on Formal Methods will take place in Singapore on 14–16 May 2014. This series of symposia is organized by
Formal Methods Europe, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development.

Topics of interest include theory and tools for specification, verification, model checking, refinement, etc.

Accepted papers will be published in Springer's LNCS series. Abstracts are due on 7 November 2013, and full papers on 14 November.

For details, please refer to the Symposium web page

NFM 2014, NASA Formal Methods Symposium

The sixth NASA Formal Methods Symposium will take place at the NASA Johnson Space Center at Houston, Texas, USA, from 29 April to 1 May 2014. NFM is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. Submissions on cross-cutting approaches are encouraged, marrying formal verification techniques with advances in safety-critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages carrying throughout system development.

Accepted papers will appear as a Springer LNCS volume. Abstracts should be submitted until 14 November 2013, with full papers of 15 pages, or short papers of 6 pages until 21 November. For full details, refer to the symposium web site.

Job Opportunities

Post-doc Position in Trento, Italy

One post-doc position in Information and Communication Technologies on the research project “Advanced SMT Techniques for Word-level Formal Verification – (WOLF)” is available at the University of Trento, Italy, under the joint supervision of Alessandro Cimatti, FBK, Trento, and Roberto Sebastiani, DISI, University of Trento.

The research activity will be carried out jointly within the Embedded Systems (ES) Research Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler (FBK), Trento, and the Software Engineering & Formal Methods (SE&FM) Research Program, at Department of Information Engineering and Computer Science (DISI) of University of Trento.

The research activity will aim at investigating and developing novel techniques, methodologies and support tools for Satisfiability Modulo Theories (SMT) for the formal verification of systems. This work will be part of the "Advanced SMT Techniques for Word-level Formal Verification –(WOLF)" project, a three-year research project supported by SRC/GRC, in collaboration with major HW companies.

The ultimate goal of the WOLF project is to provide a comprehensive SMT package to support effective formal verification of systems ranging from RTL circuits all the way up to high-level hardware description languages (e.g. SystemC) and software. The package will be implemented on top of the MathSAT SMT platform, and provided as an API.

The ideal candidate should have an PhD in computer science or related discipline, and combine solid theoretical background and excellent software development skills (in particular C/C++).

A solid background knowledge and/or previous experience on one of the following topics (in order of preference) is required: Satisfiability Modulo Theory (SMT), Propositional Satisfiability (SAT), Model Checking, Automated Reasoning. Previous experience in the following areas will also be considered favourably: Constraint Solving and Optimization, Embedded Systems Design Languages (e.g. Verilog, VHDL).

The candidate should be able to work in a collaborative environment, with a strong committment to reaching research excellence and achieving assigned objectives.

Early availability will be considered with much favour.

Interested candidates should inquire for further information and/or apply by sending email to wolf-recruit (at) disi.unitn.it

Applications should contain a statement of interest, with a Curriculum Vitae, and the names of reference persons. PDF format is strongly encouraged. It should also indicate an estimated starting date.

Emails will be automatically processed and should have 'PHD ON WOLF PROJECT' as subject.

Contact Persons: Prof. ROBERTO SEBASTIANI (rseba[at]disi[dot]unitn[dot]it), Dr. ALESSANDRO CIMATTI (cimatti [at] fbk [dot] eu)

Results of CADE Trustee Elections

Martin Giese
(Secretary of AAR and CADE)
E-mail: martingi (at) ifi.uio.no

An election was held from 24 July to 20 August to fill four positions on the board of trustees of Cade, Inc. Peter Baumgartner, Maria Paola Bonacina, Christopher Lynch, Larry Paulson, Brigitte Pientka, and Carsten Schuermann were nominated.

Ballots were sent by electronic mail to all members of AAR on 24 July, for a total of 1038 ballots. 123 valid ballots were returned, which translates to a participation level of 11.8% (as compared to 13,0% in 2012, 16.2% in 2011, 13.3% in 2010, 18.3% in 2009, 18% in 2008, and 16.4% in 2007).

Therefore, in each iteration of the single transferrable vote algorithm described in the CADE Bylaws, a candidate is elected iff she or he gets at least 62 1st preference votes. Otherwise, the votes of the candidate with the least 1st preference votes are redistributed.

The following table reports the initial distribution of preferences among the candidates:

Candidate	1st pref.	2nd pref.	3rd pref.	4th pref.	5th pref.	6th pref.	no supp.
Peter Baumgartner	33	27	20	14	14	8	7
Maria Paola Bonacina	25	31	16	14	10	7	20
Christopher Lynch	13	11	21	16	22	18	22
Larry Paulson	32	18	16	17	17	11	12
Brigitte Pientka	8	20	25	21	18	12	19
Carsten Schuermann	12	13	19	23	13	25	18