Not too long ago, in the AAR newsletter I asked you to focus on classical propositional logic. The area of logic is often termed two-valued sentential (or classical propositional) calculus and features names such as C. A. Meredith and J. Lukasiewicz. In this column I advance (in a sense) from this calculus to modal logic. And I will, as you may well expect, offer you numerous challenges relating to modal logic.
I begin with S5, one of five systems of modal logic introduced in the early 1900s by C. I. Lewis and C. H. Langford. One obtains S5 from classical propositional calculus by starting with a basis for that calculus. I have chosen a lesser-known basis offered by Lukasiewicz (and sometimes incorrectly credited to Church by me and perhaps by others).
% Following are the members of the so-called Church system.
P(i(x,i(y,x))).
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
P(i(i(n(x),n(y)),i(y,x))).
To obtain an axiomatization of S5, one adjoins the following three formulas to a basis for classical propositional calculus.
% The following three when added to a basis for two-valued gives S5.
P(i(l(i(x,y)),i(l(x),l(y)))).
P(i(l(x),x)).
P(i(n(l(x)),l(n(l(x))))).
Yes, a function now comes into play that was not present in the earlier column on propositional calculus, namely, the function l. Therefore, an inference rule is needed in addition to that for condensed detachment; both will be used with hyperresolution.
% The following clause is used with hyperresolution for condensed detachment.
-P(i(x,y)) | -P(x) | P(y).
% The following clause captures with hyperresolution necessitation.
-P(x) | P(l(x)).
For the first challenge, you are asked to prove that S5 implies S4, a second modal logic introduced by Lewis and Langford. To do so, you are asked to prove the following, given in negated form, with reliance on both condensed detachment and necessitation and the previously cited basis for classical propositional logic.
% Following purported difficult to prove negates the S4 axiom not in the S5 basis.
-P(i(l(a),l(l(a)))) | $ANS(step_s4).
For a second challenge, you are asked to prove S4; but now instead of the so-called Church basis you are given the familiar Lukasiewicz basis, the following.
% The following three are Luka, 1 2 3.
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(n(x),x),x)).
P(i(x,i(n(x),y))).
I believe you will find this second challenge more difficult to meet than the first.
But, I conjecture, you would like challenges focusing on various bases, alternative axiom systems. Therefore, I turn to C5, the strict implicational fragment of S5. For the study of C5 you need not use necessitation; indeed, condensed detachment suffices for drawing conclusions. Early in this century, I had the good fortune of collaborating with B. Fitelson, K. Harris, and Z. Ernst. As you learn later in this column, those three colleagues, in addition to laying the groundwork for finding single axioms, asked some thought-provoking questions. Ernst, in particular, produced some interesting bases for C5. I now offer three bases, the latter two from Ernst.
% Meredith's single axiom for C5
P(i(i(i(i(i(x,x),y),z),i(u,v)),i(i(v,y),i(w,i(u,y))))).
% Following is Zac Ernst's first new single axiom, Ernst1.
P(i(i(i(i(i(x,x),y),z),i(w,y)),i(i(y,v),i(u,i(w,v))))).
% Following is Zac Ernst's second new single axiom, Ernst2.
P(i(i(i(i(i(x,x),y),z),i(w,y)),i(i(v,w),i(u,i(v,y))))).
A familiar way to prove that some formula (or set of formulas) is a basis is by proving a known basis from the conjectured basis. Since each of these single axioms has length 21—ignoring predicate symbol, parentheses, and commas—you might wonder about the existence of a so-called smaller basis. Ernst provided a new basis, the following, that is such a basis.
% Zac's new 2-basis
P(i(i(x,y),i(i(i(i(y,z),w),z),i(x,z)))).
P(i(x,x)).
Now you are ready for a third challenge. You are asked to prove, from each basis, the other bases.
Two more intriguing challenges, a fourth and fifth, are now offered to complete this column. For these two challenges, I (in effect) return to an earlier column, a column in which circles of pure proofs were featured. If you have three axioms systems each consisting of a single member, a circle of pure proofs for this set of axiom systems would consist of a proof of B from A in which C is not allowed to participate, a proof of C from B in which A is not allowed to participate, and a proof of A from C in which B is not allowed to participate. I have already supplied three axioms systems, for C5, each consisting of a single formula. I now challenge you to find a circle of pure proofs for Ernst1, Ernst2, and Meredith—in that order. My glance at the research I conducted many years ago on this problem—presented to me by Fitelson, Harris, and Ernst—suggests that the desired proofs are by no means trivial.
For a sixth challenge, one I never attempted to meet, you are asked to again find a circle of pure proofs for the cited three single axioms, but in the other order, namely, Ernst1, Meredith, and Ernst2.
Modal logic, if I follow my plan, will again be featured in a later column.
An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:
The terms of Peter Baumgartner, Maria Paola Bonacina, Larry Paulson, and Brigitte Pientka expire. There are thus four positions of elected trustees to fill.
The following candidates were nominated and their statements are below:
My research focuses on the generation of proofs and countermodels for higher-order logic. I am currently the main developer of the Nitpick and Sledgehammer tools for Isabelle/HOL and collaborate with developers of superposition provers and SMT solvers to enrich their systems with features motivated by interactive verification.
I have served on the PC of main deduction conferences, including CADE, FroCoS, and IJCAR, and have chaired ITP (Interactive Theorem Proving) and TAP (Tests and Proof). CADE/IJCAR has been a mandatory stop for me since 2009, either to present papers, to represent Isabelle at CASC, or just to meet colleagues; if I missed the 2012 edition, it was only so that I could attend my Ph.D. defense. I am co-organizing the Dagstuhl Deduction seminars for 2015 and 2017 and am editing the AAR newsletter. As a CADE trustee, I would pursue the following main objectives.
1. We must promote diversity. CADE must remain open to all deductive methods. The selection of program chairs and program committee is crucial here. In a good year, CADE features a healthy balance of theory and practice, of proof calculi, empirical evaluations, and practical applications. We should make sure that all years are good years.
We must also promote co-locations in various combinations. A CADE/ITP co-location, with shared sessions and social events, would permit more interactions between the two communities that develop and use tools they both call theorem provers. Many applications would seem to need the flexibility and trustworthiness of proof assistants in conjunction with the raw reasoning power of automatic provers.
Finally, we must work harder to avoid that CADE/IJCAR slowly becomes a European affair, starting with the location of conference. We should start thinking about 2019 already, to ensure that the sequence "Vienna, Berlin, Coimbra, Gothenburg, Oxford" will get extended with a city outside Europe.
2. We must promote high scientific quality. The rebuttal phase, initiated at CADE-25 and repeated next year, is a sensible measure to raise the quality of reviews and decisions. Despite the additional burden on PC members and authors, I would argue in favor of making this a permanent feature of CADE/IJCAR.
Conference publications can suffer from the page limit and deadlines, leading to papers that are not precise or detailed enough to be reproducible. Thankfully, every year, a selection of the papers are invited in a special issue of J. Automated Reasoning. We should continue this tradition but also encourage the authors of the remaining papers to transform their underlying technical reports into journal or arXiv submissions.
3. We must increase the conference's impact and prestige. Automated reasoning is a very exciting field to work in. But even though deduction is becoming increasingly relevant, our community is hardly growing. We must improve the conference's profile, without losing the strong community feeling that is sorely missing at many top-tier conferences.
When applying for a permanent position or even for funding, the profile of the conferences we publish at matter a lot. According to the widely used CORE index, CADE is A ("excellent conference") whereas IJCAR gets the top score, A* ("flagship conference"). This is paradoxical, given that CADE's standards are not lower than IJCAR's. The current situation, with three conferences on odd years (with ranks A, A, and unranked) and only one conference on even years (with rank A*), is suboptimal, both in terms of publication opportunities and of profiling. This is a delicate topic, but as a CADE trustee I would argue in favor of reforms that benefit the community as a whole.
I believe that in the future the automated reasoning community should make a big effort to keep a strong balance between logic foundations on one side and implementations and applications on the other side. All traditional and relatively novel areas (saturation-based theorem proving, SAT/SMT technology, verification and computer algebra applications) should be equally encouraged and represented in our main conferences.
The core of my research in recent years has been on two important challenges in automated deduction: 1) how to validate that the complex techniques developed by the community produce correct results; and 2) how to exploit the power of big clusters. Although my work focused mainly on SAT and QBF solving, these challenges are also important for first-order logic and beyond. My first paper on validation of SAT techniques was accepted at IJCAR 2012. I have been participating in the CADE and IJCAR conferences since 2012 and I was a CADE PC member in 2015.
The CADE conferences have been very welcoming to papers from related communities, such as SAT, SMT, and QBF. As trustee, I would be very supportive of this position. Although most CADE attendees come from Europe, I consider it important that participation from researchers in North America is stimulated. Organizing CADE regularly in the US or Canada should therefore be continued. Maybe CADE could come back to Austin.
The researchers in the larger CADE community have created very powerful tools from Lingeling to Vampire to Z3. These tools have been successful in industry as well. I would be supportive of attracting paper submissions that describe how these tools made a difference in solving relevant problems. Such papers could have a broad impact and help further promote automated deduction.
My research focuses on the combination of automated reasoning with symbolic computation for the purpose of automating program analysis. Since 2010, I became the co-developer of the first-order theorem prover Vampire and worked on extending Vampire with support for interpolation, consequence finding, program analysis, and reasoning about theories. Hence, my interest covers both theoretical and practical aspects of automated reasoning. My research on automated reasoning and symbolic computation is mainly supported by an ERC Starting Grant 2014 and a Wallenberg Academy Fellowship 2014.
My involvement in the organization of CADE is still at the very early stage, but I have been active with giving a Vampire tutorial at CADE 2011 and establishing the yearly Vampire workshops starting with IJCAR 2014. I am also involved in the organization of CADE 2017 in Gothenburg and participated in the organization of FLoC 2014 as FLoC proceedings chair.
As a CADE trustee, I would be committed to raise the participation of early-stage researchers, in particular master and PhD students, at CADE. For that, I think it is very important to keep low the CADE conference fees but still allow students to attend social events, dinners and receptions where they get the chance to talk with more senior researcher in the field. Continuing the tradition of Woody Bledsoe student travel grants is important! In addition, I would initiate and regularly organize mentoring workshops at CADE/IJCAR for master and PhD students, giving them career advice and encouraging students to pursue research in automated reasoning.
CADE should further maintain the balance between theoretical work, applications, and tools. In addition, I think it is very important to also include case studies on various applications of automated reasoning in the CADE program, allowing active participation of young researchers from the beginning of their career. I very much support the organization and maintenance of the CASC System Competition. I would be committed to strengthen the relation between CASC and SMT-COMP, given that reasoning about theories and quantifiers is a common hot topic in both competitions.
Automated reasoning techniques and tools are increasingly used in related areas, such as symbolic computation, software verification, security, and machine learning. I would therefore pay special attention to strengthening the connection to top conferences in related areas, such as ISSAC, CAV, POPL, to only name a few.
My research is devoted to the question how cyber-physical systems (CPSs) can be made safer by developing proof principles and theorem provers for CPSs that combine computer control aspects with physical motion. These questions play an important role in ensuring the safety of advanced applications in aviation, automotive, and robotics.
CADE and its sister conferences IJCAR, FroCoS, and TABLEAUX should continue to serve as effective forums for promoting the advancement and exchange of ideas on all theoretical, practical, and applied aspects of automated reasoning. I believe they should also embrace the opportunities for synergies and interchange with related research communities as part of FLoC. CADE et al. have a tradition of providing a friendly attitude welcoming students and should build on this success, including educational initiatives like the Automated Reasoning school.
My primary mission as a CADE trustee will be to champion activities that broaden the scope and reach of automated reasoning techniques, while simultaneously arguing for the pursuit of ambitious challenge problems. I believe proofs matter, not just for the intrinsic value that they provide for anyone in our automated deduction community, but also for extrinsic reasons that the world is better off with such proofs. Significant results are often made possible by decades of core foundational research and practical reasoning advances that should continue to be pursued at CADE. Yet, they also need the right application challenges as technology drivers, whether that is the proof of the Kepler conjecture, the Feith-Thompson theorem, the analysis of a delicate software program, or of an aircraft control system.
As I have also elaborated in my invited contribution at IJCAR 2016, I am convinced that deduction has more to offer to the world. Which is why I consider it my duty to support and promote ambitious initiatives that motivate deep foundational and practical advances of proof technology, and affect true challenges that really matter.
My main research areas are automated and interactive theorem proving, program verification, and SMT solving. I have been member of the CADE/IJCAR community since I attended my first conference related to deduction, IJCAR 2004 in Cork, and always enjoyed the friendly and open atmosphere at CADE and IJCAR. Over the years, I have participated at most of the CADE/IJCAR conferences, published papers at several of them, entered the CASC competition in every year since 2012, and (co)organised affiliated events: the SAT/SMT/AR Summer School in 2016, and two workshops (LfSA in 2010, and SMT in 2014). I am also elected member of the steering committee of the SMT workshop (2014–2016), and I have served on the PC of various related conferences and workshops.
As a conference and community, CADE/IJCAR has developed well over the last years and managed to attract a stable number of submissions and attendees; but I believe that there are several challenges that the community has to keep in mind to stay relevant. One of them is to continue providing a forum for all forms of deduction; there is an ongoing diversification of theorem proving technology, which can quickly lead to new paradigms/techniques/communities that might not necessarily consider CADE/IJCAR as first affiliation. One example of the past years was the development of SMT, now increasingly being unified with first-order theorem proving (but still with publications more often at verification conferences than at CADE/IJCAR). A second example is the growing number of automated theorem provers for separation logic, and similar "new" logics inspired by applications. CADE/IJCAR has to reach out to such emerging fields to avoid getting sidelined, and to remain an attractive forum for a variety of deduction techniques.
A related challenge is to keep the conferences well-connected with applications of computer-aided deduction, and to aim at broadening the scope of reasoning and deduction by inviting or welcoming contributions from new domains. CADE/IJCAR have always been venues for both theoretical and practical papers, but concrete applications motivating the research can be as important. This obviously includes verification, formalised mathematics, etc., areas where reasoning has been successful in the past; but also new domains that might result from the resurgence of AI in the past years (in academia and industry), among others. It is a responsibility of CADE/IJCAR to propagate the use of deduction and automated reasoning wherever it can be useful, and to motivate or initiate research that closes the gap between existing techniques and potential application domains.
CADE is a special conference and community for me. Since 1999 I have been participating in CADE and IJCAR on a near annual basis. What distinguishes the conferences from other conferences in my experience is the high quality of research, the fair and constructive reviews, the open-mindedness and sense of community, the celebration of the past through the Herbrand award and the newly established Skolem award, not to forget the vibrant programme of workshops, system demos, tutorials and prover competitions.
Because of my previous membership of the Board of Trustees I appreciate the crucial role that the Board plays in constituting and ensuring the continued success of all these activities, as well as the leadership and representation it provides for the area of automated deduction.
If elected I will assist the Board in these very important missions and all its activities. To make CADE even more special I believe:
My background: My research is inter-disciplinary ranging from algebra, knowledge representation and ontology engineering to modal logic and multi-agent systems, but my main research is the automation of reasoning with a focus on developing decision procedures. My current research is focused on non-standard forms of reasoning including forgetting/uniform interpolation, model generation and automated prover generation. I am an implementer of several AR systems and have contributed to the first-order theorem prover SPASS.
I have been involved in CADE/IJCAR as an author, a presenter, a reviewer, a workshop organiser (ESCoR and PAAR), a PC member, a PC Chair (CADE-22) and have served on the Board of Trustees from 2008 to 2015. I have (co-)chaired and (co-)organised ~11 other international conferences and workshops and have (co-)edited ~17 books, conference/workshop proceedings, and special journal issues. I serve on the editorial board of the Journal of Applied Non-Classical Logic and am on the steering/organisation committee of FroCoS, TABLEAUX and ARW (UK).
My research centers on techniques for efficient theorem proving, in particularly for first-order logic with equality. Most of my research is embodied in the theorem prover E (which will eventually beat Vampire in CASC again). I have attended nearly all CADE and IJCAR conferences in the last 20 years, and have co-created both the "Empirically Successful" workshop series (many instances of which co-located with CADE/IJCAR) and the ongoing IJCAR workshop series on Practical Aspects of Automated Reasoning. After an 8 year hiatus working on developing and deploying Air Traffic Control/Air Traffic Management systems, I returned to academia full-time with a permanent position as professor of computer science at DHBW Stuttgart in 2014.
We are currently seeing the convergence of several fields of automated deduction, from propositional logic, SMT solvers, fully automatic theorem provers for first- and higher-order logic, and proof assistants, resulting in systems and processes that are actually applied to large and complex problems. Examples include the Flyspeck proof of the Kepler conjecture, the verification of the seL4 microkernel, and the CompCert verified compiler. In addition, there is renewed interaction between deduction and the wider fields of artificial intelligence and machine learning. With the increasing ubiquity of computers interacting directly with our lives, from secure communication to autonomous driving, the need for reliable systems also increases dramatically. CADE is in a unique position to participate in and help control the direction of these developments. To achieve this, we should very much try to grow the CADE community and attract younger researchers. While meetings at hotels can be an option, holding conferences at university locations makes it easier for young researchers with limited funding to attend.
CADE should strive to maintain a balance profile—with enough diversity to allow the field to develop and enough focus to allow real and effective communication between attendees. I also welcome the trend to accepting more practical and application-oriented papers at CADE. Implementations help to highlight both strengths and weaknesses of theoretical results, and very much help us to identify new and relevant areas of work.
Personal: My first CADE was in 1984 when I started studying computer science at Kaiserslautern. Since then I have regularly contributed to CADE/IJCAR as a conference participant, author, PC member, trustee (2009–2015), IJCAR coChair and sponsor (CASC computers). I worked in industry for six years, from 1999 to 2005, before returning to the Max Planck Institute for Informatics and founding the automation of logic group. End of 2011 I started the company L4B that sells theorem proving technology to industry.
Nominee Statement: CADE is the major conference on the automation of deduction. I will commit myself to keeping CADE the place for people working on the automation of deduction including the variety of logics, methods, and all stages of the pipeline from basic research to applications. It is this great many-sidedness that makes CADE unique on the conference landscape.
We see now that more and more of our technologies find their way from academia to industry as well as to other fields of science, in particular through systems. Therefore, deduction system engineering has become another valid research area for CADE. I will commit myself to support a culture where applied engineering research, research based on experiments, and basic research results without any direction to applications are all welcome at CADE. I also think that there is room of improvement for our "marketing." We have already done so by the (re)introduction of a best paper award, but there is more we can do. In particular, to support the career of young researchers that are in competition with researchers from related communities.
The 10th International Web Rule Symposium (RuleML 2016) was held at Stony Brook University, Stony Brook, New York 11794, USA, June 6-9, 2016. A total number of 68 papers were submitted from which 18 full papers, 2 short papers, 3 industry papers, 7 challenge papers and 3 Doctoral Consortium papers were selected. Moreover, 2 keynote and 2 tutorial papers were invited. Most regular papers were presented in one of these tracks: Smart Contracts, Blockchain, and Rules, Constraint Handling Rules, Event Driven Architectures and Active Database Systems, Legal Rules and Reasoning, Rule- and Ontology-Based Data Access and Transformation, Rule Induction and Learning.
Following up on previous years, RuleML also hosted the 6th RuleML Doctoral Consortium and the 10th International Rule Challenge, which this year was dedicated to applications of rule-based reasoning, such as: Rules in Retail, Rules in Tourism, Rules in Transportation, Rules in Geography, Rules in Location-Based Search, Rules in Insurance Regulation, Rules in Medicine, and Rules in Ecosystem Research.
This year's symposium featured four invited keynote and tutorial talks: Richard Waldinger, of SRI International (keynote): Natural Language Access to Data: It Needs Reasoning, Bruce Silver, of Bruce Silver Associates (keynote): DMN as a Decision Modeling Language, Neng-Fa Zhou, of City University of New York (tutorial): Programming in Picat, and Michael Kifer, Theresa Swift and Benjamin Grosof, of Coherent Knowledge Systems (tutorial): Practical Knowledge Representation and Reasoning in Ergo.
As a novelty this year, there was a highly successful co-location between RuleML 2016 and DecisionCAMP 2016, facilitated by Jacob Feldman and colleagues. A total number of 132 participants attended both conferences and the affiliated sub-events. The co-location was a great opportunity for the rule-based community and the industrial decision-modeling community to mingle at one of the several joint events such as: the joint reception and conference dinner at the Hilton Garden Hotel on, respectively, Tuesday July 6 and Thursday July 8; the joint keynote by Bruce Silver; the joint tutorial by Neng-Fa Zhou; and the RuleML industry session on Friday, July 9.
The RuleML 2016 Best Paper Awards were given to: Iliano Cervesato, Edmund Soon Lee Lam and Ali Elgazar for their paper "Choreographic Compilation of Decentralized Comprehension Patterns", and Ho-Pun Lam, Mustafa Hashmi and Brendan Scofield for their paper "Enabling Reasoning with LegalRuleML".
The 10th International Rule Challenge Awards went to: Ingmar Dasseville, Laurent Janssens, Gerda Janssens, Jan Vanthienen and Marc Denecker, for their paper "Combining DMN and the Knowledge Base Paradigm for Flexible Decision Enactment", and Jacob Feldman for his paper "What-If Analyzer for DMN-based Decision Models".
As in previous years, RuleML 2016 was also a place for presentations and face-to-face meetings about rule technology standardizations, which this year covered RuleML 1.02 (System of Families of Languages and Knowledge-Interoperation Hub) and DMN 1.1 (OMG DMN RTF).
Links:
We would like to thank our sponsors, whose contributions allowed us to cover the costs of student participants and invited/keynote speakers. We would also like to thank all the people who have contributed to the success of this year's special RuleML 2016 and co-located events, including the organization chairs, PC members, authors, speakers, and participants.
The RuleML community will join forces in 2017 with the RR (Web Reasoning and Rule Systems) community for the joint conference: RuleML+RR 2017: International Joint Conference on Rules and Reasoning, under the leadership of Fariba Sadri and Roman Kontchakov.
See you all next year at RuleML+RR 2017 in London, UK.
The 2nd Global Conference on Artificial Intelligence (GCAI 2016) will be held at the Freie Universität Berlin from 29th September to 2nd October, 2016. The conference addresses all aspects of artificial intelligence. There will be 29 papers presented, tutorials on automated theorem proving in classical and non-classical logic, and three invited speakers:
HVC 2016 invites authors to present their work in a poster session during the conference. The poster session is intended to give researchers the opportunity to present promising initial results, interesting work-in-progress or any idea worthwhile sharing with the HVC community. The session will be interactive, allowing authors to get feedback about their work and further exchange ideas with researchers and practitioners participating in HVC.
The lovely city of Haifa resides on a mountain overlooking the Mediterranean Sea, and is home to Jews, Muslims, and Christians. Haifa is also the world center of the Baha'i faith, and the wondrous Baha'i gardens are a must-see attraction. The conference will be held at IBM Research – Haifa, situated at the top of the Carmel mountains.
Extended abstracts should be sent by email by 30 September 2016. Submissions can be up to 2 PDF pages in length. Submissions should follow a standard LNCS paper template, either in Latexor Word.
Submissions will be reviewed and evaluated by the program committee. If accepted, the author will be required to prepare a 70 x 100 cm poster to present in the HVC poster session. The program committee will issue a number of grants to support students who present their work. All poster submissions from outside Israel will be considered for these grants.
Although this event focuses on students' work, we welcome submissions by other researchers and practitioners, to accommodate exposure of early results that are not yet ready for full paper publication. See the conference web site for details.
For more than two decades, the RAMiCS conferences series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond.
We invite submissions in the general field of algebraic structures relevant to computer science and on applications of such algebras. Topics of the conference include, but are not limited to the following:
Invited speakers:
The abstract submission deadline is 25 November 2016. See the conference web site for details.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.
New developments and emerging applications like autonomous software for Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced separation assurance algorithms for aircraft, and the need for system-wide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. Similar challenges need to be addressed during development and deployment of on-board software for spacecraft ranging from small and inexpensive CubeSat systems to manned spacecraft like Orion, as well as for ground systems.
The focus of the symposium will be on formal techniques and other approaches for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.
Topics of interest include but are not limited to: Model checking; Theorem proving; SAT and SMT solving; Symbolic execution; Static analysis; Model-based development; Runtime verification; Software and system testing; Safety assurance; Fault tolerance; Compositional verification; Security and intrusion detection; Design for verification and correct-by-design techniques; Techniques for scaling formal methods; Formal methods for multi-core, GPU-based implementations; Applications of formal methods in the development of autonomous systems, safety-critical artificial intelligence systems, cyber-physical, embedded, and hybrid systems, and fault-detection, diagnostics, and prognostics systems; Use of formal methods in assurance cases, human-machine interaction analysis, requirements generation, specification, and validation, and automated testing and verification.
The abstract submission deadline is 28 November 2016. Registration is required but is free of charge. There are two categories of submissions: regular papers describing fully developed work and complete results (maximum 15 pages); short papers on tools, experience reports, or work in progress with preliminary results (maximum 6 pages). Papers will appear in a volume of Springer's Lecture Notes in Computer Science (LNCS), and must use LNCS style formatting. Authors of selected best papers may be invited to submit an extended version to a special issue of the J. Automated Reasoning. See the conference web site for details.
A. P. Ershov Informatics Conference (the PSI Conference Series, the 11th edition) is the premier international forum in Russia for research and applications in Computer Science (CS) and Software Engineering (SE). PSI is held regularly since 1991. The conference brings together academic and industrial researchers, developers and users to discuss the most recent topics in the field. PSI provides an ideal venue for setting up research collaborations between the growing Russian CS/SE researcher community and its international counterparts. The conference is held to honour the late academician Andrei Ershov (1931–1988) and his outstanding contributions towards advancing informatics.
PSI is governed by International Steering and Programme Committees. The PSI Proceedings are published by Springer in the Lecture Notes in Computer Science series (LNCS). The abstract submission deadline is 13 January 2017. There are three categories of submissions: regular papers describing fully developed work and complete results (15 pages / 30 minute talks); short papers reporting on interesting work in progress and/or preliminary results (9 pages / 15 minute talks); system and experimental papers describing implementation or evaluation of experimental systems and containing a link to a working system (7 pages / 10 minute presentations).
Three satellite workshops will be held in conjunction with PSI 2017:
Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The programme of the conference TACL 2017 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the eighth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL).
Contributed talks can be on with any topic involving the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: algebraic structures in CS; algebraic logic; coalgebra; categorical methods in logic; domain theory; lattice theory; lattices with operators; many-valued and fuzzy logics; modal logics; non-classical logics; ordered topological spaces; ordered algebraic structures; pointfree topology; proofs and types; residuated structures; semantics; stone-type dualities; substructural logics; topological semantics of modal logic.
The conference will be held at the campus of the Faculty of Arts, Charles University in Prague from 26 to 30 June 2017. The summer school will be held at the campus of the Faculty of Science, Palacký University Olomouc from 20 to 24 June 2017. (The two cities are two hours train trip apart.) See the conference web site for more information.
The Defence Science and Technology Group, Edinburgh Australia, are looking to fill an "S&T6 Computer Theory and Programming Specialist" position.
Candidates must have proven ability to undertake novel research and development in the areas of dynamic and static computer program analysis, or proven ability to undertake novel research and development in formal methods with advanced understanding of compiler construction and aptitude and skills to apply this to program analysis.
There are nontrivial (e.g., citizenship) eligibility conditions for employment within Defence, including the requirement to successfully undergo the security clearance vetting process.
For more details—in particular, about how to apply—please see the job advert.
A postdoctoral position is available in the Systems Software Research Group at Virginia Tech on a project involving formally verifying experimental software systems. The project's goals include verifying components of experimental Linux kernels (e.g., Popcorn Linux), compiler backends and run-times (e.g., HydraVM), and transactional memory concurrency libraries (e.g., Hyflow), which are being developed by the group and transitioned into production contexts of sponsors.
Recent computer science/engineering PhD graduates with formal methods background (e.g., Isabelle/HOL) are sought. The position is for three years minimum, with strong possibilities for additional years. For the right candidate, a research faculty position may also be possible. Contact Prof. Binoy Ravindran with a CV or for any questions.
The Automation of Logic group, led by Dr Christoph Weidenbach, is searching for a researcher to work with us on the next generation of automated reasoning procedures. We are interested in new ways for combining classical logics with theories in theory and practice.
The position is for up to five years. We will support the successful applicant to build his/her own subgroup and to get the right for PhD supervision at Saarland University. We expect a background in automated reasoning, preferrably including programming experience.To apply for this post, please send your personal record (including CV, publication list, research statement) by email to Jennifer Müller. The deadline for the application is 31 October 2016.
A Researcher position is available in the Embedded Systems Research Unit (ES) at Bruno Kessler Foundation (FBK), Center for Information Technology. FBK is a private research institution based in Trento (Italy) and operating in different scientific fields and disciplines. As such, it has the role of keeping the Autonomous Province of Trento within the mainstream of international research. FBK is made up of seven research centres.
The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation (FBK-irst), Trento, Italy consists of about 25 people, including researchers, post-docs, PhD students, and programmers. The Unit carries out research, tool development and technology transfer in the field of design and verification of embedded systems.
The ES Unit has an opening for a PostDoc position in the framework of CITADEL ("Critical Infrastructure Protection using Adaptive MILS"), an H2020 European project started on June 1, 2016. The successful candidate will be employed for a period of at least two years (with a trial period of 6 months). He/She will carry out research activities in the field of formal methods applied to the design and implementation of adaptive systems with critical safety and security requirements. In particular, the activities will focus on:
Preferred: In depth previous experience in at least one of the following areas: Symbolic Model Checking, Temporal Logics and Property Specification Languages, Satisfiability Modulo Theory, Formal Specification and Analysis of Architectures, Contracts and Interface Theories, Architecture Description Languages, Software Model Checking, or Model-Based Safety Analysis (e.g., automatic generation of fault trees).
Type of contract: Fixed Term Contract
Gross annual salary: about 38K Euro
Working hours: full time
Benefits: flexi-time, company subsidized cafeteria or meal vouchers,
internal car park, welcome office support for visa formalities,
accommodation, social security, etc., reductions on bank account
opening fees, public transportation, sport, language course fees
Start date: November 2016
Workplace: Povo (TN)
Application deadline: 1 October 2016.
Candidates are required to submit their applications by filling in an online form. Please make sure that your application includes the following attachments (pdf format): Detailed CV; Cover Letter (explaining your motivation for this specific position); 3 professional references (e-mails and/or phone numbers). Please read the Guidelines for Selection before completing your application. For further information or technical issues regarding the application, please contact the Human Resources Service.
Candidates who pass the preliminary curricula screening will be contacted shortly afterwards for an interview. Non selected applicants will be notified of their exclusion at the end of the selection process. Please note that FBK may contact shortlisted candidates within a period of 12 months, for the selection processes of similar vacancies. For reasons of professional transparency, the name of the successful candidate will be published on the FBK website following acceptance of the position.