NEWSLETTER No. 104, September 2013

- From the AAR President, Larry Wos…
- Maria Paola Bonacina follows Franz Baader as President of CADE
- Conferences
- FLoC 2014, Federated Logic Conference, Call for Workshop Proposals
- LPAR-19, Logic for Programming, Artificial Intelligence and Reasoning
- FMCAD 2013, Formal Methods in Computer-Aided Design
- LATA 2014, Language and Automata Theory and Applications
- FM 2014, International Symposium on Formal Methods
- NFM 2014, NASA Formal Methods Symposium

- Job Opportunities
- Results of CADE Trustee Elections

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.

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.

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.

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:

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

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, 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.

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

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.

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)

*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 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Brigitte Pientka, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
no supp. |

Peter Baumgartner | 33 | 34 | 21 | 17 | 11 | 7 |

Maria Paola Bonacina | 25 | 36 | 20 | 15 | 7 | 20 |

Christopher Lynch | 14 | 13 | 26 | 25 | 23 | 22 |

Larry Paulson | 36 | 17 | 18 | 26 | 14 | 12 |

Carsten Schuermann | 15 | 20 | 25 | 18 | 27 | 18 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Christopher Lynch, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
no supp. |

Peter Baumgartner | 38 | 36 | 28 | 14 | 7 |

Maria Paola Bonacina | 33 | 33 | 23 | 14 | 20 |

Larry Paulson | 36 | 24 | 29 | 22 | 12 |

Carsten Schuermann | 16 | 26 | 27 | 36 | 18 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
no supp. |

Peter Baumgartner | 42 | 52 | 22 | 7 |

Maria Paola Bonacina | 38 | 39 | 26 | 20 |

Larry Paulson | 43 | 23 | 45 | 12 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Maria Paola Bonacina, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
no supp. |

Peter Baumgartner | 71 | 45 | 7 |

Larry Paulson | 52 | 59 | 12 |

Now, Peter Baumgartner reaches at least 62 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Peter Baumgartner and get the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
no supp. |

Maria Paola Bonacina | 38 | 32 | 13 | 9 | 11 | 20 |

Christopher Lynch | 17 | 19 | 19 | 25 | 21 | 22 |

Larry Paulson | 39 | 21 | 20 | 20 | 11 | 12 |

Brigitte Pientka | 14 | 28 | 28 | 22 | 12 | 19 |

Carsten Schuermann | 14 | 18 | 29 | 18 | 26 | 18 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
no supp. |

Maria Paola Bonacina | 42 | 35 | 14 | 12 | 20 |

Christopher Lynch | 19 | 22 | 34 | 26 | 22 |

Larry Paulson | 43 | 24 | 26 | 18 | 12 |

Brigitte Pientka | 18 | 33 | 26 | 27 | 19 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Brigitte Pientka, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
no supp. |

Maria Paola Bonacina | 48 | 42 | 13 | 20 |

Christopher Lynch | 22 | 37 | 42 | 22 |

Larry Paulson | 51 | 27 | 33 | 12 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Christopher Lynch, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
no supp. |

Maria Paola Bonacina | 63 | 40 | 20 |

Larry Paulson | 57 | 54 | 12 |

Now, Maria Paola Bonacina reaches at least 62 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Maria Paola Bonacina and get the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
no supp. |

Christopher Lynch | 33 | 15 | 24 | 29 | 22 |

Larry Paulson | 49 | 26 | 23 | 13 | 12 |

Brigitte Pientka | 22 | 40 | 28 | 14 | 19 |

Carsten Schuermann | 18 | 32 | 26 | 29 | 18 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
no supp. |

Christopher Lynch | 36 | 28 | 37 | 22 |

Larry Paulson | 55 | 36 | 20 | 12 |

Brigitte Pientka | 29 | 44 | 31 | 19 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Brigitte Pientka, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
no supp. |

Christopher Lynch | 46 | 55 | 22 |

Larry Paulson | 72 | 39 | 12 |

Now, Larry Paulson reaches at least 62 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Larry Paulson and get the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
no supp. |

Christopher Lynch | 43 | 21 | 37 | 22 |

Brigitte Pientka | 44 | 42 | 18 | 19 |

Carsten Schuermann | 31 | 39 | 35 | 18 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Carsten Schuermann, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
no supp. |

Christopher Lynch | 54 | 47 | 22 |

Brigitte Pientka | 58 | 46 | 19 |

No candidate reaches at least 62 first preference votes.

By redistributing the votes of Christopher Lynch, one gets the following table:

Candidate |
1st pref. |
no supp. |

Brigitte Pientka | 104 | 19 |

Now, Brigitte Pientka reaches at least 62 first preference votes, and is elected.

To summarize, the 4 candidates elected are Peter Baumgartner, Maria Paola Bonacina, Larry Paulson, and Brigitte Pientka.

After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:

- Peter Baumgartner (elected 2013)
- Maria Paola Bonacina (elected 2013, president)
- Martin Giese (secretary)
- Bernhard Gramlich (elected 2012)
- Deepak Kapur (IJCAR 2014 program co-chair)
- Neil Murray (treasurer)
- Larry Paulson (reelected 2013)
- Brigitte Pientka (reelected 2013)
- Renate Schmidt (reelected 2012, vice-president)
- Viorica Sofronie-Stokkermans (elected 2011)
- Geoff Sutcliffe (elected 2011)
- Christoph Weidenbach (reelected 2012)

On behalf of the AAR and CADE Inc., I thank Franz Baader for three years of service as member and president of the CADE Board of Trustees. We are also grateful to Amy Felty, who has been a member of the Board for six years.

I further thank all candidates for running in the election, and all members who voted.

Congratulations to Peter Baumgartner, Maria Paola Bonacina, Larry Paulson, and Brigitte Pientka on being elected!