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: firstname.lastname@example.org * 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 email@example.com, firstname.lastname@example.org 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 email@example.com. * 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 (firstname.lastname@example.org) Birgitta Lindstrom, University of Skovde, Sweden (email@example.com) Markus Bohlin, SICS Swedish ICT, Vasteras, Sweden (firstname.lastname@example.org) 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 email@example.com, 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 (firstname.lastname@example.org); 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 (email@example.com) if you are interested. * http://alpha.uhasselt.be/jan.vandenbussche
Back to the LICS web page.