SIGLOG Monthly 186
October  1, 2016

*******************************************************************
* Past issues of the newsletter are available at
 http://lics.siglog.org/newsletters/
* Instructions for submitting an announcement to the newsletter
 can be found at
 http://lics.siglog.org/newsletters/inst.html
*******************************************************************

TABLE OF CONTENTS
* NEWS
  ANNOUNCEMENT OF THE 2016 CHURCH AWARD
  ACM SIGLOG Announcement
  LICS 2017 CALL FOR WORKSHOP PROPOSALS
  ETAPS 2017 JOINT CALL FOR PAPERS
  IN MEMORIAM: BORIS (BOAZ) TRAKHTENBROT (1921-2016)
  2016 CAV AWARD ANNOUNCEMENT
* DEADLINES
  Forthcoming Deadlines
* CALLS
  EDITOR-IN-CHIEF ACM TRANSACTIONS ON COMPUTATION THEORY - Call for Nominations
  TIME 2016 - Call for Participation
  TAMC 2017 - Call for Papers
  SETTA 2016 - Call for Participation
  NFM 2017 - Call for Papers
  ITEQS 2017 - Call for Papers
  PODS 2017 - Call for Papers (2nd submission cycle)
  SAC 2017 - Call for Papers
  CAV 2017 - Call for Papers
  FSCD 2017 - Call for Workshop Proposals
* JOB ANNOUNCEMENTS
  PHD POSITION AT THE RWTH AACHEN
  POST-DOCTORAL POSITION IN PROOF THEORY, VIENNA UNIVERSITY OF TECHNOLOGY
  3-YEAR POSTDOC POSITION AT HASSELT UNIVERSITY


THE 2016 ALONZO CHURCH AWARD
FOR OUTSTANDING CONTRIBUTIONS TO LOGIC AND COMPUTATION
  http://siglog.hosting.acm.org/wp-content/uploads/2016/05/church16.pdf
* The 2016 Alonzo Church Award for Outstanding Contributions to Logic
  and Computation is given to Rajeev Alur and David Dill for their
  invention of timed automata, a decidable model of real-time systems,
  which combines a novel, elegant, deep theory with widespread
  practical impact.
  Rajeev Alur and David Dill: A theory of timed automata.
  Theoretical Computer Science 126(2):183-235, 1994.
  * Alur and Dill will receive the award at the 31st Annual ACM/IEEE
  Symposium on Logic in Computer Science (LICS), which will be held on
  July 5-8, 2016, at Columbia University, New York City, USA.
* The Award was established in 2015 by the ACM Special Interest Group
  for Logic and Computation (SIGLOG), the European Association for
  Theoretical Computer Science (EATCS), the European Association for
  Computer Science Logic (EACSL), and the Kurt Goedel Society
  (KGS). It recognises an outstanding contribution represented by a
  paper or small group of papers within the past 25 years; this is the
  first such award. The Award Committee consisted of Catuscia
  Palamidessi, Gordon Plotkin, Wolfgang Thomas, and Moshe Vardi
  (chair).



ACM SIGLOG ANNOUNCEMENT
  http://siglog.acm.org
* The ACM has recently chartered a Special Interest Group on Logic and
  Computation (ACM SIGLOG).
* We are pleased to announce the 2016 ACM SIGLOG election results for
  the term of 1 July 2016 - 30 June 2019. The SIGLOG Chair is Prakash
  Panangaden and the other officers are Luke Ong (vice-Chair), Amy
  Felty (Treasurer) and Alexandra Silva (Secretary).
* The ACM-IEEE Symposium on Logic in Computer Science is the flagship
  conference of SIGLOG. SIGLOG will also actively seek association
  agreements with other conferences in the field. A SIGLOG newsletter
  (SIGLOG News) is also published quarterly in an electronic format
  with community news, technical columns, members' feedback,
  conference reports, book reviews and other items of interest to the
  community.
* One can join SIGLOG by visiting
  https://campus.acm.org/public/qj/gensigqj/siglist/gensigqj_siglist.cfm
  It is possible to join SIGLOG without joining ACM (the SIGLOG
  membership fee is $25 and $15 for students).



32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2017)
  Call for Workshop Proposals
  http://lics.siglog.org/lics17/
* The thirty-second Annual ACM/IEEE Symposium on Logic In Computer
  Science (LICS'17) will be held in Reykjavik, Iceland on June 20–23,
  2017. The workshops will take place on June 18 - 19, 2017. June 18
  will only be used by two-days workshops (if any), or in case the
  number of workshops is really large. This year, workshop fees should
  be around 65 euros for a one-day workshop (including lunch and two
  coffee breaks).
* Researchers and practitioners are invited to submit proposals for
  workshops on topics relating logic - broadly construed - to computer
  science qor related fields.  Typically, LICS workshops feature a
  number of invited speakers and a number of contributed
  presentations. LICS workshops do not usually produce formal
  proceedings. However, in the past there have been special issues of
  journals based in part on certain LICS workshops.
* Proposals should include:
   -  A short scientific summary and justification of the proposed
      topic.
      This should include a discussion of the particular
      benefits of the topic to the LICS community.
   -  A discussion of the proposed format and agenda.
   -  The proposed duration, which is typically one day (two-day
      workshops can be accommodated too).
   -  Procedures for selecting participants and papers.
   -  Expected number of participants. This is important for the room!
   -  Potential invited speakers.
   -  Plans for dissemination (for example, special issues of journals).
  Proposals should be sent to Patricia Bouyer: bouyer@lsv.fr
* IMPORTANT DATES
  - Submission deadline:            November 1, 2016
  - Notification:                   November 15, 2016
  - Program of the workshops ready: May 19, 2017
  - Workshops:                      June 18 - 19, 2017
  - LICS conference:                June 20 - 23, 2017
* The workshops selection committee consists of the LICS General
  Chair, LICS Workshops Chair, LICS 2017 PC Chair and LICS 2017
  Conference Chair.



20TH EUROPEAN JOINT CONFERENCES ON THEORY AND PRACTICE OF SOFTWARE
(ETAPS 2017)
  Joint call for papers
  Uppsala, Sweden, 22-29 April 2017
  http://www.etaps.org/2017
  Abstracts due (ESOP, FASE, FoSSACS, TACAS): 14 October 2016
  Papers due: 21 October 2016
* ABOUT ETAPS
  ETAPS is the primary European forum for academic and industrial
  researchers working on topics relating to software science. ETAPS,
  established in 1998, is a confederation of five main annual
  conferences, accompanied by satellite workshops. ETAPS 2017 is the
  twentieth event in the series.
* MAIN CONFERENCES (24-28 April)
  - ESOP: European Symposium on Programming
          (PC chair Hongseok Yang, University of Oxford, UK)
  - FASE: Fundamental Approaches to Software Engineering
          (PC chairs Marieke Huisman, Universiteit Twente, The
          Netherlands, and Julia Rubin, University of British Columbia,
          Canada)
  - FOSSACS: Foundations of Software Science and Computation Structures
          (PC chairs Javier Esparza, Technische Universität München,
          Germany, Andrzej Murawski, University of Warwick, UK)
  - POST: Principles of Security and Trust
          (PC chairs Matteo Maffei, Universität des Saarlandes, Germany,
          Mark D. Ryan, University of Birmingham, UK)
  - TACAS: Tools and Algorithms for the Construction and Analysis of
           Systems
          (PC chairs Axel Legay, INRIA Rennes, France,
          and Tiziana Margaria, LERO, Ireland)
* TACAS '17 hosts the 6th Competition on Software Verification
  (SV-COMP).
* INVITED SPEAKERS
   - Unifying speakers:
     Michael Ernst (University of Washington, USA)
     Kim G. Larsen (Aalborg University, DK)
   - FoSSaCS invited speaker:
     Joel Ouaknine (University of Oxford, UK)
   - TACAS invited speaker:
     Dino Distefano (Facebook and Queen Mary University of London, UK)
* IMPORTANT DATES
    -  Abstracts due (ESOP, FASE, FoSSACS, TACAS): 14 October 2016
    -  Papers due: 21 October 2016
    -  Rebuttal (ESOP and FoSSaCS only): 7-9 December 2016
    -  Notification: 22 December 2016
    -  Camera-ready versions due: 20 January 2017
* SATELLITE EVENTS (22-23 April, 29 April)
  Around 20 satellite workshops will take place before and after the
  main conferences.
* Please do not hesitate to contact the organizers at
  parosh.abdulla@it.uu.se, mohamed_faouzi.atig@it.uu.se



IN MEMORIAM: BORIS (BOAZ) TRAKHTENBROT (1921-2016)
  http://cacm.acm.org/news/207650-in-memoriam-boris-trakhtenbrot-1921-2016/fulltext
  https://www.eatcs.org/images/awards/LAUDATIO2011.pdf
* With deep sadness we announce the passing of a great pioneer of
  theoretical computer science, Boris Trakhtenbrot. He passed away on
  September 19, 2016 at the age of 95 leaving behind a wealth of
  seminal results in logic, model theory and computability theory,
  which have had enormous impact. In 2011, the European Association
  for Theoretical Computer Science (EATCS) awarded Trakhtenbrot its
  annual Distinguished Achievements Award.



2016 CAV AWARD ANNOUNCEMENT
  (from Ahmed Bouajjani - Univ. Paris Diderot,
   the CAV Award chair this year)
* The annual CAV (Computer-Aided Verification) Award recognizes a
  specific fundamental contribution or a series of outstanding
  contributions to computer-aided verification. The CAV award was
  established in 2008 by the steering committee of the CAV conference,
  which is the premier international event for reporting research on
  computer-aided verification, a sub-discipline of Computer Science
  that is concerned with ensuring that software and hardware systems
  operate correctly and reliably.  The 2016 CAV Award was given on
  July 21, 2016, at the 28th annual CAV conference held in Toronto, to
   -  Josh Berdine,
   -  Cristiano Calcagno,
   -  Dino Distefano,
   -  Samin Ishtiaq,
   -  Peter O'Hearn,
   -  John Reynolds, and
   -  Hongseok Yang
  for their pioneering work on Separation Logic. The aqward  citation
  acknowledges these researchers "For the development of
  Separation Logic and for demonstrating its applicability in the
  automated verification of programs that mutate data
  structures".
* THE AWARD-WINNING CONTRIBUTION
  Separation Logic is an extension of Hoare logic that allows
  reasoning about heap structures and pointer manipulation. The heap
  is the key aspect of imperative programs that makes their
  verification difficult, as compared to hardware designs or
  functional programs, especially, compositional reasoning about heap
  manipulating programs is particularly hard. Separation Logic
  provides the fundamental paradigm for achieving that, especially by
  introducing the crucial concept of the separating conjunction. This
  was a real breakthrough that changed our way of thinking, and opened
  the door to a wide field of research that lead to the development of
  efficient verification tools for heap manipulating programs.
  Separation Logic has been developed in a series of papers published
  between the years of 2000 to 2002, co-authored by Peter O'Hearn,
  John Reynolds, Samin Ishtiaq, and Hongseok Yang. This fundamental
  work was building on early work by Burstall in early 70's and by
  O'Hearn and Pym in late 90's on Bunched Logic.  Then, after the
  discovery of the logic, a team formed by Josh Berdine, Cristiano
  Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang, undertook
  the challenge of demonstrating the use of Separation Logic in
  practice. This group of researchers developed a series of prototype
  tools for automated program verification exploiting Separation Logic
  (tools such as Space Invader and Smallfoot), and applied these tools
  successfully to significant industrial-size case studies. The design
  of these tools was based on new decision procedures for useful
  fragments of the logic as well as on efficient techniques for
  abstract program analysis (using abstract interpretation and) partly
  building on the principles of the Shape Analysis defined by Sagiv,
  Reps and Wilhelm, and introducing the key concept of
  bi-abduction. The work of this team was absolutely crucial in making
  separation logic very popular in our research community.
* More generally, the work of the winners of 2016 CAV award had an
  important and deep impact on our community and is certainly among
  the major contributions to the area of formal methods and automated
  verification in the last two decades. The research around Separation
  Logic is still very active. Following the work initiated by the
  group of awardees, many researchers are nowadays working on both
  fundamental and practical issues related to Separation Logic and its
  use in efficient verification tools. Other examples of the impact of
  Separation Logic are the SLAyer tool developed at Microsoft, which
  was applied there to device drivers, and the Infer tool developed
  and currently used at Facebook for the verification of mobile
  applications.



DATES
* LICS 2017
  Call for Workshop Proposals
  http://lics.siglog.org/lics17/
  Submission deadline:    November 1, 2016
* ETAPS 2017
  Joint call for papers
  Uppsala, Sweden, 22-29 April 2017
  http://www.etaps.org/2017
  Abstracts due (ESOP, FASE, FoSSACS, TACAS): 14 October 2016
  Papers due: 21 October 2016
* TIME 2016
  Call for Participation
  October 17-19, 2016, Technical University of Denmark, Denmark
  http://time2016.compute.dtu.dk/
* TAMC 2017
  Call for Papers
  http://www.tamc2017.unibe.ch
  Bern, 20-22 April 2017
  Submission Deadline: October 31, 2016
* SETTA 2016
  Call for Participation
  Beijing, China, Nov. 9-11, 2016
  http://lcs.ios.ac.cn/setta/
  Early registration deadline: October 10, 2016
* NFM 2017
  Call for Papers
  http://ti.arc.nasa.gov/events/nfm-2017/
  May 16 - 18, 2017
  NASA Ames Research Center
  Moffett Field, CA, USA
* ITEQS 2017
  Call for Papers
  Tokyo - Japan
  http://www.mrtc.mdh.se/ITEQS/2017/
  Co-located with ICST 2017
  Submission deadline: December 1, 2016
* PODS 2017
  Call for Papers (2nd submission cycle)
  May 14-19, 2017, Raleigh, North Carolina, USA
  http://www.sigmod2017.org
  December 11, 2016, 11:59pm PST: Abstract submission
  December 18, 2016, 11:59pm PST: Paper submission
* SAC 2017
  Software Verification and Testing Track
  April 3-7, 2017, Marrakech, Morocco
  http://http://antares.sip.ucm.es/svt2017/ and
  http://www.sigapp.org/sac/sac2017/
* CAV 2017
  Call for Papers
  Heidelberg, Germany, July 22-28, 2017
  http://cavconference.org/2017/
* FSCD 2017
  Call for Workshop Proposals
  http://www.cs.ox.ac.uk/conferences/fscd2017
  Submission of workshop proposals: January 30, 2017



EDITOR-IN-CHIEF ACM TRANSACTIONS ON COMPUTATION THEORY
  Call for Nominations
* The term of the current Editor-in-Chief (EiC) of the ACM
  Transactions on Computation Theory (TOCT) is coming to an end, and
  the ACM Publications Board has set up a nominating committee to
  assist the Board in selecting the next EiC.  TOCT was established in
  2009 and has an average submission rate of approximately 67
  manuscripts per year.  It has been managed well and has a growing
  reputation.
* Nominations, including self nominations, are invited for a
  three-year term as TOCT EiC, beginning on January 1, 2017.  The EiC
  appointment may be renewed at most one time. This is an entirely
  voluntary position, but ACM will provide appropriate administrative
  support.
* Appointed by the ACM Publications Board, Editors-in-Chief (EiCs) of
  ACM journals are delegated full responsibility for the editorial
  management of the journal consistent with the journal's charter and
  general ACM policies. The Board relies on EiCs to ensure that the
  content of the journal is of high quality and that the editorial
  review process is both timely and fair. He/she has final say on
  acceptance of papers, size of the Editorial Board, and appointment
  of Associate Editors. A complete list of responsibilities is found
  in the ACM Volunteer Editors Position Descriptions:
  http://www.acm.org/publications/policies/position_descriptions
* Additional information can be found in
  the following documents:
  http://www.acm.org/publications/policies/RightsResponsibilities
  http://www.acm.org/publications/policies/evaluation/
* Nominations should include a vita along with a brief statement of
  why the nominee should be considered. Self-nominations are
  encouraged, and should include a statement of the candidate's vision
  for the future development of TOCT. The deadline for submitting
  nominations is October 27, 2016, although nominations will continue
  to be accepted until the position is filled.
* Please send all nominations to the nominating committee
  chair Chris Hankin at c.hankin@imperial.ac.uk.
* The search committee members are:
  Chris Hankin (Imperial College London), Chair and ACM Publications
  Board
  Liaison Johan Hastad (Royal Institute of Technology, Sweden)
  Ronitt Rubinfeld (MIT and Tel Aviv University)
  Rocco Servedio (Columbia University)
  Omer Reingold (Stanford University)



23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION
AND REASONING (TIME 2016)
  Call for Participation
  October 17-19, 2016, Technical University of Denmark, Denmark
  http://time2016.compute.dtu.dk/
* TIME 2016 aims to bring together researchers interested in reasoning
  about temporal aspects of information in any area of Computer
  Science. The symposium, currently in its 23rd edition, has a wide
  remit and intends to cater to both theoretical aspects and
  well-founded applications. One of the key aspects of the symposium
  is its interdisciplinarity, with attendees from distinct areas such
  as artificial intelligence, database management, logic and
  verification, and beyond. The symposium will encompass three tracks
  on temporal representation and reasoning in Artificial Intelligence,
  Databases and Logic and Verification.
* Further details about the topics of interest can be found on the webpage.
* Invited speakers:
  - Kim Guldstrand Larsen, Aalborg University, Denmark
  - Angelo Montanari, University of Udine, Italy
  - Paolo Terenziani, University of Piemonte Orientale, Italy
* Important dates:
  - Early registration until August 31, 2016
  - Registration until September 29, 2016
  - Late registration from September 30, 2016
  - Symposium: October 17-19, 2016



THEORY AND APPLICATIONS OF MODELS OF COMPUTATION 2017 (TAMC 2017)
  http://www.tamc2017.unibe.ch
  Bern, 20-22 April 2017
  Submission Deadline: October 31, 2016.
* TAMC 2017 aims at bringing together a wide range of researchers with
  interest in computational theory and its applications. The main
  themes of the conference are computability, computer science logic,
  complexity, algorithms, models of computation and systems theory.
  There are two special sessions planned: Logic in computer science
  and New models of computation.
* Typical but not exclusive topics of interest include: algebraic
  computation, algorithmic coding and number theory, approximation
  algorithms, automata theory, computational biology and biological
  computing, computational complexity, computational game theory,
  computational geometry, computer science logic, cryptography, domain
  models, learning theory, modal and temporal logics, model theory for
  computing, natural computation, networks in nature and society,
  online algorithms, optimization, privacy and security, process
  models, proof complexity, property testing, quantum computing,
  randomness and pseudo-randomness, space-time tradeoffs, streaming
  algorithms, systems theory, VLSI models of computation.
* INVITED SPEAKERS:
  Marta Kwiatkowska (Univesity of Oxford, Oxford),
  Pinyan Lu (Shanghai University of Finance and Economics, Shanghai),
  Maria Emilia Maietti (Universite di Padova, Padova),
  Johann A. Makowsky (Israel Institute of Technology, Haifa),
  Carlos Martin-Vide (Universitat Rovira i Virgili, Tarragona),
  Stefan Wolf (Universite della Svizzera italiana, Lugano),
  Jeffery Zucker (McMaster University, Hamilton)
* IMPORTANT DATES
  Submission Deadline: October 31, 2016.
  Notification of Acceptance: December 15, 2016.
  Final Camera Ready Version: January 15, 2017.
* PROGRAMME CHAIRS
  G. Jager (University of Bern),
  Co-chair: T V Gopal (Anna University, India),
* Please find the paper submission guidelines at:
  http://www.tamc2017.unibe.ch/submission.html



2ND SYMPOSIUM ON DEPENDABLE SOFTWARE ENGINEERING THEORIES, TOOLS AND
  APPLICATIONS (SETTA 2016)
  Call for Participation
  Beijing, China, Nov. 9-11, 2016
  http://lcs.ios.ac.cn/setta/
* IMPORTANT DATES
  Early registration deadline: October 10, 2016
  Conference: Nov. 9-11, 2016
* The aim of the symposium is to bring together international
  researchers and practitioners in the field of software
  technology. Its focus is on formal methods and advanced software
  technologies, especially for engineering complex, large-scale
  artifacts like cyber-physical systems, networks of things,
  enterprise systems, or cloud-based services. Contributions relating
  to formal methods or integrating them with software engineering, as
  well as papers advancing scalability or widening the scope of
  rigorous methods to new design goals are especially welcome.
* INVITED SPEAKERS
  - Prof. Edward A. Lee (University of California at Berkeley, USA):
  Dependable Cyber-Physical Systems
  - Prof. Sriram Sankaranarayanan(University of Colorado Boulder, USA):
  From finitely many simulations to flowpipes
  - Prof. Mingsheng Ying (University of Technology Sydney, Australia
  and Tsinghua University, China):
  Toward Automatic Verification of Quantum Programs
* CO-LOCATED EVENTS
  SETTA 2016 will be accompanied by two co-located events:
* 2nd Young Researchers Workshop on Formal Methods (YR-SETTA 2016)
  http://lcs.ios.ac.cn/setta/yr-setta/
*  FMAC 2016 (in Chinese)
  http://lcs.ios.ac.cn/setta/fmac2016/



THE 9TH NASA FORMAL METHODS SYMPOSIUM (NFM 2017)
  Call for Papers
  http://ti.arc.nasa.gov/events/nfm-2017/
  May 16 - 18, 2017
  NASA Ames Research Center
  Moffett Field, CA, USA
* THEME OF THE SYMPOSIUM
  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, desi= gn, 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
     - fault-detection, diagnostics, and prognostics systems
  - Use of formal methods in:
     - assurance cases
     - human-machine interaction analysis
     - requirements generation, specification, and validation
     - automated testing and verification
* IMPORTANT DATES
  Abstract Submission: November 28, 2016
  Paper Submission: December 5, 2016
  Paper notification: February 3, 2017
  Camera Ready Deadline: March 1, 2017
  Symposium: May 16-18, 2017



1ST INTERNATIONAL WORKSHOP ON TESTING EXTRA-FUNCTIONAL PROPERTIES AND
QUALITY CHARACTERISTICS OF SOFTWARE SYSTEMS (ITEQS 2017)
  Call for Papers
  Tokyo - Japan
  http://www.mrtc.mdh.se/ITEQS/2017/
  Co-located with ICST 2017
  Submission deadline: December 1, 2016
* TOPICS
   - Model-based testing of EFPs; e.g., choice of modeling languages to
   capture EFPs and their role on testability, model-based test case
   generation, etc.
   - Mutation-based testing for EFPs; e.g., application of mutation
   techniques for testing of EFPs particularly introduction of
   EFP-specific mutation operators
   - Search-based testing techniques for EFPs
   - Testability, observability, controllability and the role of the
   platform; e.g., how the choice of operating system can impact
   testability of EFPs, for instance, a real-time operating system,
   introducing testability mechanisms into a platform, designing -
   middlewares for testing of EFPs
   - Empirical studies and experience reports; e.g., on the importance
   of testing EFPs, evaluation of testing methods, case-study and
   reports on project failures due to EFPs, comparison of methods and
   techniques
   - Quality assurance, standards, and their impact on testing EFPs
   - Requirements and testing EFPs; e.g., identification and generation
   of test oracles for EFPs from requirements, requirements for
   testability, traceability
   - Coverage criteria in testing EFPs
   - Processes and their role in testing EFPs; e.g., agile and TDD
   - Fault localization for EFPs and debugging
   - Formal methods, model-checking, and reasoning about EFPs
   - Parallelism, Concurrency, and Testing of multicore applications
   - Performance, Robustness, and Security Testing
   - Testing real-time, embedded, and cyber-physical systems, and their
   challenges
   - Testing quality characteristics of distributed, mobile, and cloud
   applications
* IMPORTANT DATES
  Submission deadline: December 1, 2016
  Notifications: January 2, 2017
  Workshop date: March 12, 2017 (preliminary)
* ORGANIZERS
  Mehrdad Saadatmand, SICS Swedish ICT, Vasteras, Sweden
  (mehrdad@sics.se)
  Birgitta Lindstrom, University of Skovde, Sweden
  (birgitta.lindstrom@his.se)
  Markus Bohlin, SICS Swedish ICT, Vasteras, Sweden
  (markus.bohlin@sics.se)



36TH ACM SIGMOD-SIGACT-SIGAI SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS
(PODS 2017)
  Call for Papers (2nd submission cycle)
  May 14-19, 2017, Raleigh, North Carolina, USA
  http://www.sigmod2017.org
* The PODS symposium series, held in conjunction with the SIGMOD
  conference series, provides a premier annual forum for the
  communication of new advances in the theoretical foundations of data
  management, traditional or non-traditional (see
  http://www.sigmod.org/the-pods-pages/the-pods-pages).
* For the 36th edition, PODS continues to aim to broaden its scope, and
  calls for research papers providing original, substantial
  contributions along one or more of the following aspects:
  - deep theoretical exploration of topical areas central to data
    management;
  - new formal frameworks that aim at providing the basis for deeper
    theoretical investigation of important emerging issues in data
    management; and
  - validation of theoretical approaches from the lens of practical
    applicability in data management.
* TOPICS that fit the interests of the symposium include the following:
  - design, semantics, query languages
  - data models, data structures, algorithms for data management
  - concurrency and recovery, distributed and parallel databases, cloud
    computing
  - model theory, logics, algebras, computational complexity
  - graph databases and (semantic) Web data
  - data mining, information extraction, search
  - data streams
  - data-centric (business) process management, workflows, web services
  - incompleteness, inconsistency, uncertainty in data management
  - data and knowledge integration and exchange, data provenance, views
    and data warehouses, metadata management
  - domain-specific databases (multi-media, scientific, spatial,
    temporal, text)
  - deductive databases
  - data privacy and security
* PROGRAM CHAIR
  Floris Geerts (University of Antwerp, BE)
* IMPORTANT DATES
  - Dates for second submission cycle:
    December 11, 2016, 11:59pm PST: Abstract submission
    December 18, 2016, 11:59pm PST: Paper submission
    February 26, 2017, 11:59pm PST: Accept/Reject notification
    March 19, 2017, 11:59pm PST: Camera-ready deadline
* AWARDS
  - Best Paper Award: An award will be given to the best submission, as
    judged by the program committee.
  - Best Student Paper Award: There will also be an award for the best
    submission, as judged by the program committee, written by a student
    or exclusively by students.



32ND ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING
  Software Verification and Testing Track
  April 3-7, 2017, Marrakech, Morocco
  http://http://antares.sip.ucm.es/svt2017/ and
  http://www.sigapp.org/sac/sac2017/
  Sponsored by ACM Special Interest Group on Applied Computing
  www.sigapp.org
* IMPORTANT DATES
  - September 29, 2016: Papers and SRC submission
  - November 10, 2016: Paper and SRC notification
  - November 25, 2016: Camera-ready copies
  - Author registration: December 10, 2016
* ACM Symposium on Applied Computing
  The ACM Symposium on Applied Computing (SAC) has gathered scientists
  from different areas of computing over the last thirty years. The
  forum represents an opportunity to interact with different
  communities sharing an interest in applied computing.
* SAC 2017 is sponsored by the ACM Special Interest Group on Applied
  Computing (SIGAPP), and will be hosted by the University of Quebec
  (Montreal, Canada), University Cadi Ayyad (Marrakech, Morocco),
  Mohamed V University of Rabat Mohammadia School Of
  Engineers (Rabat, Morocco) and National School of Applied Sciences
  (Kenitra, Morocco).
* SOFTWARE VERIFICATION AND TESTING TRACK
  Possible topics include, but are not limited to:
  - model checking
  - theorem proving
  - correct by construction development
  - model-based testing
  - verification-based testing
  - symbolic execution
  - static and run-time analysis
  - abstract interpretation
  - analysis methods for dependable systems
  - software certification and proof carrying code
  - fault diagnosis and debugging
  - verification of large scale software systems
  - real world applications and case studies applying software
    verification
* TRACK ON CYBER-PHYSICAL SYSTEMS (CPS)
  https://conference.cs.cityu.edu.hk/saccps/
  Topics of Interest
  We plan to include all the important topics related to CPS. These
  topics include, but are not limited to:
  - Ubiquitous and pervasive computing for enhanced user interactions with CPS
  - Wearable cyber-physical systems and applications
  - Design automation and Tool Chains for CPS
  - Networking systems for CPS applications
  - Cloud computing and distributed systems to support scalability and
  complexity of CPS
  - Data analytics for CPS
  - Control of CPS
  - Security and privacy of CPS
  - Resilient and Robust System Design for CPS
  - Simulation and experimental prototypes of CPS
* STUDENT RESEARCH COMPETITION
  As previous editions, SAC 2017 organises a Student Research
  Competition (SRC) Program to provide graduate students the
  opportunity to meet and exchange ideas with researchers and
  practitioners in their areas of interest. Guidelines and information
  about the SRC program can be found at
  http://www.sigapp.org/sac/sac2017/.
* Program Committee Chairs
  Ylies Falcone, Universite Grenoble Alpes, Inria, France
  Mercedes G. Merayo, Universidad Complutense de Madrid, Spain



29TH INTERNATIONAL CONFERENCE ON COMPUTER-AIDED VERIFICATION (CAV 2017)
  Call for Papers
  Heidelberg, Germany, July 22-28, 2017
  http://cavconference.org/2017/
* IMPORTANT DATES
  All deadlines are AOE (Anywhere on Earth).
  Papers:
    Paper submission:          January 24, 2017 (Tuesday)
    Author response period:    March 20-22, 2017 (Monday - Wednesday)
    Author notification:       April 12, 2017 (Wednesday)
    Final version:             May 5, 2017 (Friday)
  Conference:
    Workshops:                 July 22-23, 2017
    Main conference:           July 24-28, 2017
* CAV 2017 is the 29th in a series dedicated to the advancement of the
  theory and practice of computer-aided formal analysis and synthesis
  methods for hardware and software systems.  CAV considers it vital
  to continue spurring advances in hardware and software verification
  while expanding to domains such as cyber-physical, social, and
  biological systems.  The conference covers the spectrum from
  theoretical results to concrete applications, with an emphasis on
  practical verification tools and the algorithms and techniques that
  are needed for their implementation. The proceedings of the
  conference will be published in the Springer LNCS series. A
  selection of papers will be invited to a special issue of Formal
  Methods in System Design and the Journal of the ACM.
* Topics of interest include but are not limited to:
  Algorithms and tools for verifying models and implementations
  Algorithms and tools for system synthesis
  Mathematical and logical foundations of verification and synthesis
  Specifications and correctness criteria for programs and systems
  Deductive verification using proof assistants
  Hardware verification techniques
  Program analysis and software verification
  Software synthesis
  Hybrid systems and embedded systems verification
  Compositional and abstraction-based techniques for verification
  Probabilistic and statistical approaches to verification
  Verification methods for parallel and concurrent systems
  Testing and run-time analysis based on verification technology
  Decision procedures and solvers for verification and synthesis
  Applications and case studies in verification and synthesis
  Verification in industrial practice
  New application areas for algorithmic verification and synthesis
  Formal models and methods for security
  Formal models and methods for biological systems
* Lightweight Double-Blind Reviewing Process CAV 2017 will employ a
  lightweight double-blind reviewing process. This means that
  committee members will not have access to authors' names or
  affiliations as they review a paper; however, authors' names will be
  revealed once reviews have been submitted.
* CHAIRS
    Viktor Kuncak, EPFL, Switzerland
    Rupak Majumdar, Max Planck Institute for Software Systems, Germany
* CAV Award Committee
    Tom Ball  (Chair), Microsoft research
    Kim G. Larsen, Aalborg University
    Natarajan Shankar, SRI International
    Pierre Wolper, Liege University



FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION (FSCD 2017)
  Call for Workshop Proposals
  September 2017, Oxford, UK
  http://www.cs.ox.ac.uk/conferences/fscd2017
* FSCD 2017, co-located with ICFP 2017, will be the second edition of
  the International Conference on Formal Structures for Computation
  and Deduction. The FSCD conference was created by the communities
  behind two major conferences, RTA (Rewriting Techniques and
  Applications) and TLCA (Typed Lambda Calculi and Applications). The
  first event took place in Porto, Portugal in June 2016 and was
  extremely successful, attracting 186 participants and 11 workshops.
* We invite proposals for workshops, tutorials or other satellite
  events, on any topic to related formal structures in computation and
  deduction, from theoretical foundations to tools and applications. A
  full list of suggested topics is given here:
    http://www.cs.ox.ac.uk/conferences/fscd2017/cfp.html
  Satellite events will take place on 7-9 September, after the main
  conference on 3-6 September. It is expected that satellite events
  would run for 1 or 2 days, and be open to participants of parallel
  events.
* PROPOSALS
  Proposals should be submitted by email directly to the workshop chair
  jamie.vicary@cs.ox.ac.uk, with the following information:
 - title of the satellite event, description of the topic and its
   relevance to FSCD;
 - names and affiliations of the organizers;
 - pointers to information about past editions of the event, if
   applicable;
 - proposed event duration and format (for example, paper
   presentations, tutorials, demo sessions, etc);
 - plans for invited speakers or special sessions;
 - estimate of the number of participants;
 - procedures for selecting papers and participants and plans for the
   publication of proceedings, if any;
 - tentative schedule for paper submission and notification of
   acceptance;
 - a brief description (up to 120 words) of the event for the website
   and publicity material;
 - any other special requirements.
* IMPORTANT DATES
  Submission of workshop proposals: January 30, 2017
  Notification of success of proposals: February 13, 2017
  Main conference: September 3-6, 2017
  Workshop dates: September 7-9, 2017



PHD POSITION AT THE RWTH AACHEN
* Applications are invited for a PhD position in theoretical computer
  science at the RWTH Aachen University. The successful applicant is
  expected to carry out research related to graph isomorphism and
  similar problems (interpreted in a wide sense). The position is one of
  several funded in the project "Logic, Structure, and the Graph
  Isomorphism Problem" lead by Martin Grohe and Pascal Schweitzer.
* Candidates should have a strong interest in the theory of
  computation and a solid background in computer science and
  mathematics. All applicants should have an excellent master's degree
in computer
  science, mathematics, or a related discipline. Applications should
  include a detailed CV, a copy of the master thesis, a brief statement
  of research interests, and a list of publications (if applicable).
  Please also mention names and contact details of one or two
  references, preferably one from the thesis advisor.
* The position is fulltime and can be started as soon as possible for
  the applicant. The position is funded for two years, with a possible
  extension of at least another year.
* Please send your application materials per email to Martin Grohe
  (grohe@informatik.rwth-aachen.de); the closing date is
  ***20 September 2016***.
* If you have further questions, please contact Martin Grohe.



POST-DOCTORAL POSITION IN PROOF THEORY, VIENNA UNIVERSITY OF TECHNOLOGY
* A position as post-doctoral researcher is available in the group for
  Computational Logic (http://www.dmg.tuwien.ac.at/fg2/) at the
  Faculty of Mathematics of the Vienna University of Technology. This
  position is part of a research project on the proof theory of
  induction. The aim of this project is to further deepen our
  understanding of the structure of proofs by induction and to develop
  new algorithms for the automation of inductive theorem proving.
  Techniques of relevance include cut-elimination, witness extraction,
  Herbrand's theorem.
* The successful candidate is expected to have (or be close to
  completing) a PhD in mathematics or computer science and a strong
  background in proof theory.  Experience in one or more of the
  following areas is an advantage: formal languages, computational
  complexity, automated theorem proving, unification theory. The
  ability to work in a team is an important prerequisite.
* The employment is full-time (40h / week). The salary is EUR 33.300,-
  after taxes per year. The position is initially for 1 year - an
  extension is possible in case of mutual interest. The starting date
  is negotiable, but qshould be within 6 months of the application
  deadline. The application deadline is October 21, 2016.
* The application should contain:
  - cover letter
    (Why are you interested in this position? Why are you qualified?)
  - curriculum vitae
  - list of publications
  - scan of graduation diploma and/or other relevant certificates
  - preferred starting date
  - up to two references or letters of recommendation
* Send informal inquiries and your application to:
  Stefan Hetzl 
  http://www.dmg.tuwien.ac.at/hetzl/



3-YEAR POSTDOC POSITION AT HASSELT UNIVERSITY
* We have a vacancy for a 3-year postdoc position at Hasselt
  University.  The salary is very good and it comes with social
  security, health insurance, what have you.  The topic is very
  flexible as long as it has to do with finite model theory,
  expressive power of database query languages, in particular
  query languages for novel data models such as JSON or graph
  data, tractable fragments of higher-order logic is also a theme
  that fits.
* The position needs to be filled by 1 January 2017 at the latest.
* The research group on Databases and Theoretical Computer
  Science at Hasselt University is a leading group in the
  theoretical foundations of data management.  Professors are
  Marc Gyssens, Bart Kuijpers, Frank Neven, and Jan Van den
  Bussche
* Please email Jan Van den Bussche
  (jan.vandenbussche@uhasselt.be) if you are interested.
* http://alpha.uhasselt.be/jan.vandenbussche



Back to the LICS web page.