Newsletter 146 May 2, 2013 ******************************************************************* * 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 * LICS-RELATED NEWS LICS 2013 - Call for Participation (MFPS/LICS/CSF registration is open!) Test-of-Time Awards (LICS 1993) * DEADLINES Forthcoming Deadlines * CALLS FORMAL METHODS IN SECURITY SUMMER SCHOOL - Call for Registration PLMMS 2013 - Call for Papers FMCAD 2013 - Call for Papers SBMF 2013 - Call for Papers FMICS 2013 - Call for Papers PERSYVAL CPS SUMMER SCHOOL - Call for Applications FMSPLE 2013 - Call for Papers SAT 2013 - Call for Posters CAV 2013 - Call for Participation SAT/SMT SUMMER SCHOOL - Call for Applications CADE-24 - Call for Participation CALCO Early Ideas Workshop 2013 - Call for Contributions Samson@60 - Call for Participation AVOCS 2013 - Call for Papers CiE 2013 - Call for Informal Presentations GALOP 2013 - Call for Talks CICLOPS 2013 - Call for Papers FOPARA 2013 - Call for Papers APLAS 2013 - Call for Papers ESSLLI 2014 - Call for Course and Workshop Proposals BLAST 2013 - Call for Abstracts and Participation LPAR-19 - Call for Papers and Workshop Proposals MihalisFest 2013 - Call for Participation * JOB/COURSE ANNOUNCEMENTS Assistant/Associate Professor in TCS at VU Amsterdam Postdoc in Verification of Binary Code at Queen Mary, University of London PhD Studentship in Verification of Cyber-Physical Systems at Newcastle European Master's Programme in Computational Logic 28TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2013) LICS conference: June 25-28, 2013 Workshops: June 28-29, 2013 New Orleans, USA http://lics.siglog.org/lics13/ * COLOCATION The twenty-eighth ACM/IEEE Symposium on Logic In Computer Science (LICS 2013) will be held in New Orleans, USA, 25-28 June 2013. It will be colocated with MFPS (Mathematical Foundations of Programming Semantics) and CSF (IEEE Computer Security Foundations). * REGISTRATION Registration is now open for all three events. Early registration deadline: May 22nd, 2013 http://www.regonline.com/mfps_lics_csf * INVITED SPEAKERS LICS 2013 will feature invited lectures by Rajeev Alur, Joseph Halpern (with CSF), Nancy Lynch and Prakash Panangaden. It will also include a special session to mark the 80th birthday of Dana Scott, which will have the following invited speakers: Andrew Pitts, Steve Awodey, Andrej Bauer, Robert Harper, and Dana Scott. * TUTORIAL SPEAKERS Tutorials will be given by Hubert Comon and Jan Rutten (with MFPS). * AFFILIATED WORKSHOPS Foundations of Computer Security (FCS) http://prosecco.gforge.inria.fr/personal/bblanche/fcs13/ Higher-Order Program Analysis (HOPA) http://hopa.cs.rhul.ac.uk Syntax and Semantics of Low-Level Languages (LOLA) http://research.microsoft.com/en-us/events/lola2013/ Natural Language and Computer Science (NLCS) http://www.indiana.edu/~iulg/nlcs.html * ACCEPTED PAPERS http://lics.siglog.org/lics13/accepted.html LICS TEST-OF-TIME AWARDS (LICS 93) * The Awards Committee consisting of Prakash Panangaden (chair), Jean-Pierre Jouannaud, Martin Grohe and Tom Henzinger decided to honour the following three outstanding papers from LICS'93 (held in Montreal, Quebec, Canada): - Leo Bachmair, Harald Ganzinger and Uwe Waldmann Set constraints are the monadic class, - Andre Joyal, Mogens Nielsen and Glynn Winskel Bisimulation via open maps, - Benjamin C. Pierce and Davide Sangiorgi Typing and subtyping for mobile processes. DEADLINES * PLMMS 2013 Abstract submission: May 6, 2013 http://www.cicm-conference.org/2013/cicm.php?event=plmms&menu=general * FMCAD 2013 Abstract submission: May 8, 2013 http://www.fmcad.org/FMCAD13 * SBMF 2013 Abstract Submission Deadline: May 08, 2013 Full Paper Submission Deadline: May 14, 2013 http://cbsoft2013.unb.br/en/sbmf-en * FMICS 2013 Paper submission: May 10, 2013 http://lvl.info.ucl.ac.be/Fmics2013 * PERSYVAL CPS SUMMER SCHOOL Deadline for applications: May 15, 2013 https://persyval-lab.org/summer-school/cps * FMSPLE 2013 Submission deadline: May 17, 2013 http://people.cs.kuleuven.be/dave.clarke/FMSPLE2013.html * SAT 2013 Poster submission deadline: May 17, 2013 http://sat2013.cs.helsinki.fi/ * CAV 2013 Early registration deadline: May 20, 2013 http://cav2013.forsyte.at * SATSMT 2013 Registration deadline: May 20, 2013 http://satsmt2013.ics.aalto.fi * CADE-24 Early registration deadline: May 22, 2013 http://www.cade-24.info/ * LICS 2013 Early registration deadline: May 22, 2013 http://lics.siglog.org/lics13/ * CALCO Early Ideas Workshop 2013 Submission deadline: May 27, 2013 http://coalg.org/calco13/workshops.html#ei * AVOCS 2013 Abstract submission: May 31, 2013 Paper submission: June 7, 2013 http://www.avocs2013.org.uk * CiE 2013 Informal presentations deadline: May 31, 2013 http://cie2013.disco.unimib.it * GALOP 2013 Submission deadline: May 31, 2013 http://www.gamesemantics.org * CICLOPS 2013 Abstract submission: June 1, 2013 http://akira.ruc.dk/~cth/ciclops13 * FOPARA 2013 Draft submission: June 3, 2013 http://fopara2013.cs.unibo.it * APLAS 2013 Abstract due: June 10, 2013 http://aplas2013.soic.indiana.edu/ * ESSLLI 2014 Proposal submission deadline: June 15, 2013 http://www.esslli2014.de * BLAST 2013 Abstract submission deadline: July 1, 2013 http://www.chapman.edu/events/blast-2013/ * LPAR-19 Workshop proposal deadline: July 15, 2013 Abstract submission: July 22, 2013 http://www.LPAR-19.info SUMMER SCHOOL ON FORMAL METHODS FOR THE SCIENCE OF SECURITY Call for Registration July 22-26 2013 Information Trust Institute University of Illinois at Urbana-Champaign (UIUC) http://www.iti.illinois.edu/summerschool * GOALS The goal of this Summer School is to give graduate students and security professionals a comprehensive view of the different research directions in which Formal Methods are advancing the Science of Security. The lecturers are world-renowned researchers advancing the use of Formal Methods in Security. * LECTURERS The School Director is Jose Meseguer, (UIUC). The lecturers include: Gilles Barthe (IMDEA-Software, Spain) Felix Klaedtke (ETH-Zurich, Switzerland) Catherine Meadows (Naval Research Laboratory) Dusko Pavlovic (Royal Holloway, UK) Fred Schneider (Cornell University) Graham Steel (INRIA, France) * PARTICIPANTS The Summer School encourages participation of graduate students in Computer Science, Computer Engineering, and related disciplines (e.g., Mathematics), and of professionals working in security. Graduate students can apply for scholarships to attend the Summer School. * VENUE AND REGISTRATION The Summer School will be held at the Campus of the University of Illinois at Urbana-Champaign Monday July 22 through Friday July 26; 8 - 5 each day. To facilitate interaction with the lecturers and due to classroom sizes, registration is limited and will be determined on a first-come-first-serve basis among registering participants. The $250 registration fee covers all materials, lunches and coffee breaks, and a Summer School dinner. * Registration can be made electronically at: http://www.iti.illinois.edu/summerschool 5TH INTERNATIONAL WORKSHOP ON PROGRAMMING LANGUAGES FOR MECHANIZED MATHEMATICS SYSTEMS (PLMMS 2013) Part of CICM-2013, at University of Bath, UK 8-12th of July 2013 http://www.cicm-conference.org/2013/cicm.php?event=plmms&menu=general * IMPORTANT DATES - Abstract submission: Mon May 6 2013 - Paper submission: Mon May 13 2013 - Notification of acceptance: Mon June 3 2013 - Camera ready copy due: Mon June 10 2013 * PLMMS Scope The program committee welcomes submissions on programming language issues related to all aspects of mechanised mathematics systems (MMS). In particular: - Mathematical algorithms - Tactics and proof search - Proofs - Mathematical notation Of particular interest are the dimensions of: - Expressiveness - Efficiency - Correctness - Understandability and Usability - Modularity and Extensibility - Design and implementation Mechanised mathematics systems, whether stand-alone or embedded in larger systems, include but are not limited to: - Dependent typed programming languages - Proof assistants - Computer algebra systems - Proof planning systems - Theorem proving systems - Theory formation systems * SUBMISSION DETAILS Papers should be submitted via the PLMMS 2013 easychair website: https://www.easychair.org/conferences/?conf=plmms2013 Submissions must describe original unpublished work which is not been submitted for publication elsewhere. At least one author of each accepted paper is expected to attend PLMMS 2013 and present her or his paper. FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2013) Call for Papers Portland, OR, USA October 20-23, 2013 http://www.fmcad.org/FMCAD13 * CONFERENCE SCOPE FMCAD 2013 is the thirteenth in a series of conferences on the theory and application of formal methods in hardware and system design and verification. FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing novel methods, technologies, theoretical results, and tools for formal reasoning about computing systems, as well as open challenges therein. * TOPICS OF INTEREST FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods technology and its application to computer-aided design. * IMPORTANT DATES Abstract Submission: May 8 Paper Submission: May 15 Author Notification: July 17 * SUBMISSIONS Submissions must be made electronically in PDF format via EasyChair. More details will be provided soon on the FMCAD web site. * CO-LOCATED EVENTS The following meetings will be co-located with this year's edition: - MEMOCODE 2013, the ACM/IEEE International Conference on Formal Methods and Models for Codesign (http://www.memocode-conference.com). - DIFTS 2013, International Workshop on Design and Implementation of Formal Tools and Systems We are also proud to host this year's Hardware Model Checking Competition (HWMCCC 2013). 15TH BRAZILIAN SYMPOSIUM ON FORMAL METHODS (SBMF) Call for Papers Brasília, Brazil 29 September to 04 October, 2013 http://cbsoft2013.unb.br/en/sbmf-en * IMPORTANT DATES Abstract Submission Deadline (American Samoa Time Zone): May 08, 2013 Full Paper Submission Deadline (American Samoa Time Zone): May 14, 2013 Full Paper Acceptance Notification: July 05, 2013 Full Paper Camera-ready Version: July 12, 2013 Short Paper Submission Deadline: July 20, 2013 Short Paper Acceptance Notification: August 20, 2013 Short Paper Camera-ready Version: August 31, 2013 * INTRODUCTION SBMF 2013 is the sixteenth of a series of events devoted to the development, dissemination and use of formal methods for the construction of high-quality computational systems. It is now a well-established event with an international reputation. Keynote speakers will be: Kenneth McMillan, Microsoft Research, USA Christiano Braga, UFF, Brazil The symposium will be part of a larger event, CBSoft, the Brazilian Conference on Software: Theory and Practice ( http://cbsoft2013.cic.unb.br/?lang=en) including, in addition to SBMF, three other symposia: XXVII Brazilian Symposium on Software Engineering (SBES) XVII Brazilian Symposium on Programming Languages (SBLP) VII Brazilian Symposium on Components, Software Architecture and Software Reuse (SBCARS) * PAPER SUBMISSION Papers with a strong emphasis on Formal Methods, whether practical or theoretical, are invited for submission. They should present unpublished and original work that has a clear contribution to the state of the art on the theory and practice of formal methods. They should not be simultaneously submitted elsewhere. There are two types of submissions: - Full papers: (max. 16 pages in LNCS format) should contain theory- or application-oriented results which must be original, significant, and sound; they will undergo a full reviewing process. Papers from industry should emphasize practical application of formal methods and/or report open challenges. The proceedings will be published in LNCS/Springer. - Short papers: (max. 6 pages in LNCS format) should describe recent research activities, practical experience, and preliminary results that are worth discussing. Papers can be submitted via the following link: http://www.easychair.org/conferences/?conf=sbmf2013 * PROGRAM COMMITTEE CHAIRS Leonardo de Moura, Microsoft Research, USA Juliano Iyoda, UFPE, Brazil 18TH INTERNATIONAL WORKSHOP ON FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2013) Call for Papers September 23-24, 2013 Madrid, Spain Co-located with SEFM 2013 http://lvl.info.ucl.ac.be/Fmics2013 * SCOPE The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS workshop series also strives to promote research and development for the improvement of formal methods and tools for industrial applications. * TOPICS - Design, specification, code generation and testing based on formal methods. - Methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, real-time systems and embedded systems. - Verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues). - Tools for the development of formal design descriptions. - Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions. - Impact of the adoption of formal methods on the development process and associated costs. - Application of formal methods in standardization and industrial forums. * SUBMISSIONS Submissions must describe authors' original research work and their results. Contributions should not exceed 15 pages formatted according to the LNCS style (Springer), and should be submitted as Portable Document Format (PDF) files using the EasyChair submission site: https://www.easychair.org/conferences/?conf=fmics2013 All submissions must report on original research. Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any such published or concurrently submitted paper must be clearly indicated. Submissions should clearly demonstrate relevance to industrial application. Case study papers should identify lessons learned, validate theoretical results (such as scalability of methods), or provide specific motivation for further research and development. * IMPORTANT DATES Paper submission: May 10th Notification: June 24th Final version due: July 12th Workshop: September 23th-24th * PROGRAM CHAIRS Michael Dierkes (Rockwell Collins, France) Charles Pecheur (Université catholique de Louvain, Belgium) PERSYVAL-LAB SUMMER SCHOOL ON CYBER-PHYSICAL SYSTEMS Call for Applications July 8-12, 2013 Grenoble, France https://persyval-lab.org/en/summer-school/cps * IET ICT Labs and PERSYVAL-Lab (Pervasive systems and algorithms at the convergence of physical and digital worlds) Based on high-level research laboratories present at Grenoble in Mathematics, Computer Science, Automatic Control, Signal Processing, and Hardware Architecture, is organizing the 1st edition of the CPS Summer School. * This school will bring together some of the best lecturers from Europe and the USA, in a one week programme, and be a fantastic opportunity for interaction. It will be held in the campus of Grenoble University-France. * IMPORTANT DATES Deadline for Application: May 15, 2013. Response to Applicants: May 20, 2013. Online Registration and Fee payment: May 29, 2013. * FEES Registration fee is EUR 350 for students, EUR 500 for non-students, which includes lunches from Monday 8th through Friday 12th. The registration fee only partially covers the costs incurred. The remaining costs are covered by the EIT ICT Labs and PERSYVAL-Lab. 4TH WORKSHOP ON FORMAL METHODS AND ANALYSIS IN SOFTWARE PRODUCT LINE ENGINEERING (FMSPLE 2013) Call for Papers August 27, 2013 Tokyo, Japan Co-located with SPLC 2013 (http://www.splc2013.net/) http://people.cs.kuleuven.be/dave.clarke/FMSPLE2013.html * BACKGROUND AND OBJECTIVES Software product line engineering (SPLE) aims at developing a family of systems by reuse in order to reduce time to market and to increase product quality. The objective of the workshop “Formal Methods and Analysis in Software Product Line Engineering (FMSPLE)” is to bring together researchers and practitioners from the SPLE community with researchers and practitioners working in the area of formal methods and analysis. So far, both communities are only loosely connected, despite very promising initial work on formal analysis techniques for software product lines. The workshop aims at reviewing the state of the art and the state of the practice in which formal methods and analysis approaches are currently applied in SPLE. This leads to a discussion of a research agenda for the extension of existing formal approaches and the development of new formal techniques for dealing with the particular needs of SPLE. To achieve the above objectives, the workshop is intended as a highly interactive event fostering discussion and initiating collaborations between the participants from both communities. * TOPICS The proposed workshop focuses on the application of formal methods and analysis approaches in all phases of SPLE, including domain and application engineering, in order to ensure the correctness of individual artifacts as well as the consistency among them. The topics of interest include, but are not limited to: - Analysis approaches and formal methods for: - domain analysis and scoping - variability modeling - specification and verification of functional and non-functional properties in SPLE - safety and security aspects in SPLE - product line architectures and component-based product line development - product line implementation, such as type systems, programming languages, formal semantics - formal verification of product lines and product line artifacts - correctness-by-construction techniques in SPLE - automated test case generation and model-based testing in SPLE - product derivation and application engineering - product line life-cycle management (e.g., consistency assurance) - reuse and evolution of SPLs - Proofs of concept, industrial experiences and empirical evaluations - Tool presentations - Vision and position papers on formal methods and analyses applied to SPLE * SUBMISSION AND PUBLICATION The contributed papers are expected to comprise research papers containing novel and previously unpublished results, experience reports, reports of industrial case studies, tool descriptions, and short papers describing work in progress or exploratory ideas. All papers have to follow the ACM two-column conference proceedings format (Letter) and be 4–8 pages of length. Easychair submission: https://www.easychair.org/conferences/?conf=fmsple2013 * IMPORTANT DATES Paper Submission: May 17, 2013 Notification: June 10, 2013 Camera-ready versions: June 28, 2013 Workshop: August 27, 2013 16TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING (SAT 2013) Call for Presentation-Only Posters Helsinki, Finland July 8-12, 2013 http://sat2013.cs.helsinki.fi/ * IMPORTANT DATES -- Acceptance notifications are sent within one week of submission -- Poster abstract submissions by: May 17, 2013 Notifications by: May 22, 2013 Conference early registration deadline : May 27, 2013 * GENERAL The SAT 2013 conference invites submissions of 200-400 word poster abstracts. Each submitted abstract will be checked for suitability for presentation as a poster during a poster-session at the main conference. The poster abstracts may be about (but not restricted to): - SAT-related work-in-progress. - SAT-related work recently published or accepted for publication at other major conferences, workshops, or journals. - Descriptions of SAT-related systems, interesting benchmark problems, etc. - Overviews of SAT-related PhD theses or currently on-going PhD work. - Overviews of SAT-related research projects. * SUBMISSION DETAILS To submit a poster abstract, send the title, list of authors and their affiliations, and a 200-400 word abstract of your poster by email to email@example.com . The submissions should be in ASCII text. The accepted poster abstracts will not appear in the SAT 2013 proceedings, but will be included in the informal conference booklet made available to all registered attendees. Each poster presenter is expected to register to the main conference. SAT 2013 includes three high-quality invited talks (by Albert Atserias, Edmund M. Clarke, and Peter Stuckey), around 30 scientific presentations, various satellite events including the SMT, PoS, and QBF workshops, as well as a lively social program. 25TH INTERNATIONAL CONFERENCE ON COMPUTER-AIDED VERIFICATION (CAV 2013) Call for Participation July 13–19, 2013 Sokos Hotel Palace Bridge, St. Petersburg, Russia http://cav2013.forsyte.at * HIGHLIGHTS OF CAV - 53 regular papers, 16 tool papers, 3 invited talks, 4 invited tutorials - 25th Anniversary Panel on the Future of CAV - Special tracks on Hardware Verification, Security, SAT/SMT, and Biology - Details at http://cav2013.forsyte.at * REGISTRATION FOR CAV AND WORKSHOPS - Early Registration Deadline: May 20, 2013 - Regular Registration Deadline: July 1, 2013 * HOTEL REGISTRATION - Hotel Registration Deadline: June 1, 2013 - http://cav2013.forsyte.at/accommodation/#booking * Please note that due to the famous White Nights, July is touristic high season in St. Petersburg, and hotels may be expensive after the deadline. * VISAS TO RUSSIA - Information at http://cav2013.forsyte.at/visa/ - Please start the visa application process EARLY!!! For some countries including the US, the visa processing may take several weeks and requires substantial paper work. * CAV INVITED SPEAKERS - Jennifer Welch (Texas A&M University) - Jeannette Wing (Microsoft Research International) - Maria Vozhegova (Sberbank) * CAV INVITED TUTORIAL SPEAKERS - Cristian Cadar (Imperial College London) - David Harel (The Weizmann Institute of Science) - Andreas Podelski (University of Freiburg) - Andrei Voronkov (The University of Manchester) * ASSOCIATED WORKSHOPS AND ORGANIZERS - 6th International Workshop on Exploiting Concurrency Efficiently and Correctly - Fun with Formal Methods - Interpolation: From Proofs to Applications - Second International Workshop on Memory Consistency Models - Second CAV Workshop on Synthesis - Verification and Assurance - Verification of Embedded Systems - Verification and Program Transformation 3RD INTERNATIONAL SAT/SMT SUMMER SCHOOL 2013 Call for participation Aalto University, Otaniemi Campus Espoo, Finland, July 3-5th, 2013 http://satsmt2013.ics.aalto.fi/ * AIMS The SAT/SMT Summer School aims at providing graduate students and researchers from universities and industry with a comprehensive overview of research and methodology in satisfiability testing (SAT) and satisfiability modulo theories (SMT). The lectures cover the foundational and practical aspects of SAT and SMT technologies and their applications. * LECTURERS Olaf Beyersdorff, Humboldt-Universitaet zu Berlin, Germany Alessandro Cimatti, IRST, Trento, Italy Leonardo de Moura, Microsoft Research, Redmond, USA John Franco, University of Cincinnati, USA Enrico Giunchiligia, University of Genova, Italy Marijn Heule, University of Texas at Austin, USA Joao Marques-Silva, University College Dublin, Ireland Albert Oliveras, Technical University of Catalonia, Barcelona, Spain Stefan Szeider, Vienna University of Technology, Austria * REGISTRATION Registration for the school is now open. Full details of the registration procedure are available at the school website: http://satsmt2013.ics.aalto.fi/ (deadline: May 20th, 2013) * ORGANIZING COMMITTEE Keijo Heljanko, Aalto University Tomi Janhunen, Aalto University Matti Jarvisalo, University of Helsinki 24TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION (CADE-24) June 9-14, 2013, Lake Placid, New York, USA http://www.cade-24.info/ * CADE is the major forum for the presentation of research in all aspects of automated deduction. CADE-24 is held in Lake Placid, a charming village on the shore of two lakes surrounded by the beautiful Adirondacks Mountains, upstate New York. * PROGRAM - Invited talks: - Jean-Christophe Filliatre: One Logic to Use Them All - Greg Morrisett: Defining, Testing, and Reasoning About an x86 Decoder - Natarajan Shankar: Automated Reasoning, Fast and Slow - Douglas R. Smith: Coalgebraic Specification and Refinement - Presentation of 31 papers including the CADE-24 Best Paper Award winner (details at http://www.cade-24.info/) - Tutorials: - Franz Baader: Reasoning in Lightweight Description Logics - Bernhard Beckert: Program Verification with the KeY System - Morgan Deters, Dejan Jovanovic, Clark Barrett and Cesare Tinelli: Becoming a Power User of SMT: The CVC4 Solver - Marijn Heule: State-of-the-art SAT Solving - Carsten Schuermann, Taus Brock-Nannestad and Chris Martens: Twelf - Several Workshops (details at http://www.cade-24.info/) - The CADE ATP System Competition (CASC): http://www.tptp.org/CASC/24/ organized by Geoff Sutcliffe During the conference, the Herbrand Award for Distinguished Contributions to Automated Reasoning will be presented to Greg Nelson for his invention of equality sharing, also known as the Nelson-Oppen method, and his pioneering work on theorem proving and program checking, including fast congruence closure algorithms and the Simplify theorem prover. * IMPORTANT DATES Early registration deadline: 22 May 2013 Workshops and Tutorials: 9-10 June 2013 Conference: 11-14 June 2013 CASC: 12 June 2013 CALCO EARLY IDEAS WORKSHOP September 2, 2013 Warsaw, Poland http://coalg.org/calco13/workshops.html#ei * SCOPE CALCO 2013 will be preceded by the CALCO Early Ideas Workshop, dedicated to presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. Attendance at the workshop is open to all - it is anticipated that many CALCO conference participants will want to attend the CALCO Early Ideas workshop (and vice versa). * TOPICS The CALCO Early Ideas Workshop invites submissions on the same topics as the CALCO conference: reporting results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. The list of topics of particular interest is shown on the main CALCO 2013 page: http://coalg.org/calco13/. * SUBMISSIONS CALCO Early Ideas presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page short contributions. It can be work in progress, a summary of work submitted to a conference or workshop elsewhere, or work that in some other way might be interesting to the CALCO audience. A booklet with the accepted short contributions will be available at the workshop. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calcoearlyideas2013 The use of LNCS style is strongly encouraged. * IMPORTANT DATES 2-page short contribution submission: May 27, 2013 Notification for short contribution: June 24, 2013 Final short contribution due: July 15, 2013 CALCO Early Ideas Workshop: September 2, 2013 10-15 page paper submission: October 15, 2013 Notification for paper: December 15, 2013 Final paper version due: January 15, 2014 SAMSON@60: A CONFERENCE IN HONOUR OF SAMSON ABRAMSKY, ON THE EVENT OF HIS 60TH BIRTHDAY Call for Participation 28-30 May 2013 Department of Computer Science, University of Oxford Lecture Theatre B http://www.cs.ox.ac.uk/sa60/ * TALKS Speakers will cover the wide range of subjects to which Samson made pioneering contributions, stretching from the semantics of programming languages, including domain theory and game semantics, via logic where he introduced important notions such as full completeness, to quantum computing and quantum foundations, where he is a father of categorical quantum mechanics. * LOCAL ARRANGEMENTS Conference fee is GBP50 per person for speakers and participants. Cash (in sterling pounds) payable on 28th May 2013 at the arrival registration. Limited funding is available for students and young researchers. Please contact Destiny Chen for further details prior to your booking. * ORGANISERS Bob Coecke, Luke Ong, Prakash Panangaden * LOCAL ORGANISERS Destiny Chen, Aleks Kissinger 13TH AUTOMATED VERIFICATION OF CRITICAL SYSTEMS (AVOCS) Call for Papers http://www.avocs2013.org.uk 11-13th September, 2013 University of Surrey, UK * SCOPE The aim of Automated Verification of Critical Systems (AVoCS) 2013 is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, business-critical, performance-critical, etc). Contributions that describe different techniques, or industrial case studies are encouraged. The technical programme will consist of invited and contributed talks and also allow for short presentations of ongoing work. The workshop will be relatively informal, with an emphasis on discussion. There will be a few studentships available funded by Formal Methods Europe in order to support PhD students who present a paper at the workshop. * TOPICS Topics include (but are not limited to) Model Checking Automatic and Interactive Theorem Proving SAT, SMT or Constraint Solving for Verification Abstract Interpretation Specification and Refinement Requirements Capture and Analysis Verification of Software and Hardware Specification and Verification of Fault Tolerance and Resilience Probabilistic and Real-Time Systems Dependable Systems Verified System Development Industrial Applications * IMPORTANT DATES Submission (abstract for full paper): 31st May 2013 Submission (full papers): 7th June 2013 Notification (full papers): 12th July 2013 Submission (short papers): 19nd July 2013 Notification (short papers): 26th July 2013 Registration deadline (including accommodation): 30th July 2013 Submission of final versions: 5th August 2013 Workshop: 11-13th September 2013 * SUBMISSION DETAILS - Full Papers: Submissions of full papers to the workshop must not have been published or be concurrently considered for publication elsewhere. - Short Contributions: AVoCS'13 encourages the submissions of short contributions in order to stimulate discussions at the workshop. COMPUTABILITY IN EUROPE 2013: THE NATURE OF COMPUTATION Call for Informal Presentations Milan, Italy July 1 - 5, 2013 http://cie2013.disco.unimib.it * TUTORIAL SPEAKERS Gilles Brassard (Universite de Montreal) and Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and University of Colorado at Boulder) * PLENARY TALKS Ulle Endriss (University of Amsterdam) Lance Fortnow (Georgia Institute of Technology) Anna Karlin (University of Washington) Bernard Moret (Ecole Polytechnique Federale de Lausanne) Mariya Soskova (Sofia University) Endre Szemeredi (Hungarian Academy of Sciences, Rutgers University * SUBMISSION DETAILS http://cie2013.disco.unimib.it/call-for-informal-presentations/ * SUBMISSION DEADLINE for Informal Presentations: MAY 31, 2013 Authors will be notified of acceptance, usually within one week of submission. Authors of abstracts accepted for presentation are invited to submit a paper extending the abstract to the journal Computability. 8TH WORKSHOP ON GAMES FOR LOGIC AND PROGRAMMING LANGUAGES (GALOP 2013) Call for Talks July 18-19, 2013 Queen Mary, University of London, London, UK http://www.gamesemantics.org * GENERAL GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials as well as contributed papers and invited talks. GaLoP VIII will be held in London, UK, on 18-19 July 2013. It will be a stand-alone workshop hosted at the Mile End campus of Queen Mary, University of London. Contributions are invited on all pertinent subjects, with particular interest in game-semantic and interaction models for logics and programming languages, and applications to program analysis. * TOPICS Typical but not exclusive areas of interest are: - Game theory and interaction models in semantics; - Games-based program analysis and verification; - Logics for games and games for logics; - Algorithmic aspects of games; - Categorical aspects; - Programming languages and full abstraction; - Higher-order automata and Petri nets; - Geometry of interaction; - Ludics; - Epistemic game theory; - Logics of dependence and independence; - Computational linguistics. There will be no formal proceedings but the possibility of a special issue in a journal will be considered (the 2005, 2008 and 2011 workshops led to special issues in Annals of Pure and Applied Logic). * SUBMISSION INSTRUCTIONS Please submit an abstract of your proposed talk on the easychair submission page below. You may also submit an accompanying paper for the talk. https://www.easychair.org/conferences/?conf=galop2013 * IMPORTANT DATES Submission: May 31 Notification: June 7 Workshop: July 18-19 * INVITED SPEAKERS - Ichiro Hasuo, Tokyo - Colin Stirling, Edinburgh - Viktor Winschel, Mannheim - Nobuko Yoshida, Imperial 13TH INTERNATIONAL COLLOQUIUM ON IMPLEMENTATION OF CONSTRAINT AND LOGIC PROGRAMMING SYSTEMS (CICLOPS 2013) http://akira.ruc.dk/~cth/ciclops13 Istanbul, Turkey, August 24/25, 2013 Co-located with ICLP 2013 * IMPORTANT DATES Abstract Submission: June 1, 2013 Paper Submission: June 8, 2013 Notification: July 1, 2013 Camera-ready: July 13, 2013 Workshop: August 24/25, 2013 * TOPICS CICLOPS is a well established line of workshops. This will be the 13th edition in a successful series of workshops which is traditionally co-located with ICLP. The CICLOPS workshop aims at discussing and exchanging experience on the design, implementation, and optimization of constraint and logic programming systems, and other systems based on logic as a means of expressing computations. Preference will be given to the description and analysis of real implementations and their evaluation, problems found in their design, steps taken towards the solutions, as well as descriptions of work in progress in that direction. * SUBMISSION Authors are invited to submit papers in PDF using the Springer LNCS LaTeX format. Submissions must be written in English, not exceed 15 pages, and describe new, original and unpublished research results or work in progress. Submissions will be handled by the EasyChair conference system at https://www.easychair.org/conferences/?conf=ciclops2013. We plan for the informal workshop proceedings to be available on-line at the Computing Research Repository (CoRR) after the workshop. An electronic copy will also be distributed during the conference. 3RD INTERNATIONAL WORKSHOP ON FOUNDATIONAL AND PRACTICAL ASPECTS OF RESOURCE ANALYSIS (FOPARA 2013) August 29th to 31st, 2013, Bertinoro, Italy Co-located with WST 2013 http://fopara2013.cs.unibo.it * SCOPE The workshop will serve as a forum for presenting original research results that are relevant to the analysis of resource (time, space, and others) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged. We also encourage papers that combine theory and practice. The following list of topics is non-exhaustive: - resource static analysis for embedded or/and critical systems; - logical and machine-independent characterisations of complexity classes; - logics closely related to complexity classes; - type systems for controlling/inferring/checking complexity; - semantic methods to analyse resources, including quasi-interpretations; - practical applications of resource analysis; - complexity analysis by term and graph rewriting. * SUBMISSIONS FOPARA 2013 is a two-phase workshop. All participants are invited to submit a draft paper describing the work to be presented at the workshop. These submissions will be screened by the program committee chair to make sure they are within the scope of FOPARA and will appear in the draft proceedings distributed at the workshop. Submissions appearing in the draft proceedings are not peer-reviewed publications. After the workshop, authors will be given the opportunity to incorporate the feedback from discussions at the workshop and will be invited to submit a revised full article for the formal review process. These revised submissions will be reviewed by the program committee using prevailing academic standards to select the best articles that will appear in the formal proceedings. All contributions must be written in English, conform to the Springer LNCS series format and not exceed 16 pages. The papers selected after the reviewing process will be published as a volume of the Springer LNCS series (Springer’s approval is pending). * IMPORTANT DATES The following deadlines are strict. - Draft Submission: June 3rd, 2013; - Notification (Draft): June 21st, 2013; - Final Version: July 5th, 2013; - Paper Submission: September 30th, 2013; - Notification (Paper): December 2nd, 2013; - Camera Ready: December 23rd, 2013. 11TH ASIAN SYMPOSIUM ON PROGRAMMING LANGUAGES AND SYSTEMS (APLAS 2013) Call for Papers 9-11 December 2013 Melbourne, Australia (colocated with CPP 2013) * BACKGROUND APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community. * TOPICS The symposium is devoted to foundational and practical issues in programming languages and systems. Papers are solicited on topics such as - semantics, logics, foundational theory; - design of languages, type systems and foundational calculi; - domain-specific languages; - compilers, interpreters, abstract machines; - program derivation, synthesis and transformation; - program analysis, verification, model-checking; - logic, constraint, probabilistic and quantum programming; - software security; - concurrency and parallelism; - tools and environments for programming and implementation. * SUBMISSION We solicit submissions in two categories: - Regular research papers - System and Tool presentations Papers should be submitted electronically via the submission web page: https://www.easychair.org/conferences/?conf=aplas2013 * DATES Abstract due: 10 June 2013 (Monday), 23:59 UTC Submission due: 14 June 2013 (Friday), 23:59 UTC Notification: 26 August 2013 (Monday) Final paper due: 19 September 2013 (Thursday) Conference: 9-11 December 2013 (Monday-Wednesday) 26TH EUROPEAN SUMMER SCHOOL IN LOGIC, LANGUAGE AND INFORMATION (ESSLLI 2014) Call for Course and Workshop Proposals Tuebingen, Germany August 11-22, 2014 http://www.esslli2014.de * IMPORTANT DATES 15 June 2013: Proposal submission deadline 15 September 2013: Notification 1 June 2014: Course material due * TOPICS AND FORMAT Proposals for courses and workshops at ESSLLI'2014 are invited in all areas of Logic, Linguistics and Computing and Information Sciences. Cross-disciplinary and innovative topics are particularly encouraged. Each course and workshop will consist of five 90 minute sessions, offered daily (Monday-Friday) in a single week. Proposals for two-week courses should be structured and submitted as two independent one-week courses, e.g. as an introductory course followed by an advanced one. In such cases, the ESSLLI program committee reserves the right to accept just one of the two proposals. All instructional and organizational work at ESSLLI is performed completely on a voluntary basis, so as to keep participation fees to a minimum. However, organizers and instructors have their registration fees waved, and are reimbursed for travel and accommodation expenses up to a level to be determined and communicated with the proposal notification. ESSLLI can only guarantee reimbursement for at most one course/workshop organizer, and can not guarantee full reimbursement of travel costs for lecturers or organizers from outside of Europe. The ESSLLI organizers would appreciate any help in controlling the School's expenses by seeking complete coverage of travel and accommodation expenses from other sources. 5TH BLAST CONFERENCE (BLAST 2013) Call for Abstracts and Participation August 5 - 9, 2013 at Chapman University, Orange, California, USA. * SERIES The BLAST conference series brings together researchers in B = Boolean algebra L = Lattice theory, algebraic and quantum Logic A = Universal Algebra S = Set theory T = Set theoretic and point-free Topology The first four BLAST conferences were at the University of Denver, New<http://subsessile.nmsu.edu/blast/index.htm> Mexico State University<http://subsessile.nmsu.edu/blast/index.htm>, the University of Colorado at Boulder<http://euclid.colorado.edu/~kasterma/blast/> and the University of Kansas<http://www.math.ku.edu/conferences/blast2011/>. * INVITED TALKS BLAST 2013 will feature invited talks by - Bernhard Banaschewski (McMaster University) - William DeMeo (University of South Carolina) - Francois Dorais (Dartmouth College) - Mai Gehrke (Université Diderot - Paris 7 and CNRS) - Steven Givant (Mills College) - Steve Jackson (University of North Texas) - Michael Pinsker (Technische Universität Wien) - Dima Sinapova (University of Illinois at Chicago) - Sam van Gool (Radboud Universiteit Nijmegen) and invited tutorials by - Martin Escardo (University of Birmingham) - Heinz-Peter Gumm (Universität Marburg) - Hilary Priestley (University of Oxford) The conference is funded by NSF, Chapman University and the Center for Excellence in Computation, Algebra and Topology (CECAT). * SUBMISSION Abstract submission is through Atlas-conferences by July 1 at http://atlas-conferences.com/cgi-bin/abstract/submit/cbgq-01. * REGISTRATION Registration will be $90 before July 1, 2013, and $110 after that. Electronic registration is available on the conference web page http://www.chapman.edu/events/blast-2013/. A limited amount of financial support is available for graduate students and recent PhDs. To apply for support, send an email of request to firstname.lastname@example.org
by May 15, 2013 (see web page for details). More information can be found at the conference web page: http://www.chapman.edu/events/blast-2013/ 19TH INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING (LPAR-19) Call for Papers Stellenbosch, South Africa, 14-19 December 2013 http://www.LPAR-19.info * SERIES The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 19th LPAR will be held in Stellenbosch, South Africa. * TOPICS New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. * PROGRAMME CHAIRS - Ken McMillan - Aart Middeldorp - Andrei Voronkov * CONFERENCE CHAIRS - Bernd Fischer - Geoff Sutcliffe * WORKSHOP CHAIR - Laura Kovacs * SUBMISSION DETAILS Submissions of two kinds are welcome: - Regular papers that describe solid new research results. They can be up to 15 pages long in LNCS style, including figures and references, but excluding appendices (that reviewers are not required to read). - Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the LNCS style. Both types of papers can be electronically submitted in PDF via EasyChair: http://www.easychair.org/conferences/?conf=lpar19. Prospective authors are required to register a title and an abstract a week before the paper submission deadline (see below). * IMPORTANT DATES - Abstract submission: 22nd July - Paper submission: 2nd August - Notification of acceptance: 27th September - Camera-ready papers: 9th October - Conference: 14th-19th December - Workshop proposals: 15th July - Notification of workshops proposals: 29th July * WORKSHOP PROPOSALS LPAR-19 workshops will be held on 14th December either as one-day or half-day events. If you would like to propose a workshop for LPAR-19, please contact the workshop chair via email (email@example.com), by the proposal deadline. HORIZONS IN TCS: A CELEBRATION OF MIHALIS YANNAKAKIS's 60TH BIRTHDAY Call for Participation Workshop at Center for Computational Intractability (CCI) Princeton University, NJ, USA August 27-29, 2013. http://intractability.princeton.edu/blog/2013/01/mihalisfest-2013/ * See the workshop's webpage for further information, including list of speakers. ASSISTANT/ASSOCIATE PROFESSOR IN TCS AT VU AMSTERDAM * GENERAL At the Department of Computer Science of the VU University Amsterdam there is an open tenure-track position for Assistant/Associate Professor in Theoretical Computer Science. * CONTACT For information, see http://www.vu.nl/nl/werken-bij-de-vu/vacatures/2013/047.asp Deadline for application is June 1, 2013. Contact person is Prof. Wan Fokkink (tel: +31 (0)20 5987735, e-mail: firstname.lastname@example.org) POSTDOC IN VERIFICATION AT QUEEN MARY, UNIVERSITY OF LONDON * GENERAL Applications are invited for a full time Postdoctoral Research Assistant to undertake research within the context of an EPSRC funded project, "Compositional Security Analysis for Binaries". This project aims at theoretical and practical advances in static analysis and automatic verification applied to security of binary code. The project will be carried out in collaboration between the Theory Group at Queen Mary University of London, the Programming Principles, Logic and Verification group at UCL, and the Security Group at University of Kent. The post-holder will be based at Queen Mary, working with the Principal Investigator (www.dcs.qmul.ac.uk/~ddino) in the School of Electronic Engineering and Computer Science. * CONTACT Informal enquiries should be addressed to Prof. Dino Distefano (email@example.com). To apply, please visit the Human Resources website on http://www.jobs.qmul.ac.uk and search for reference QMUL1934. The closing date for applications is 2nd June 2013. Interviews are expected to be held week commencing 17th June 2013. PHD STUDENTSHIP IN VERIFICATION OF CYBER-PHYSICAL SYSTEMS AT NEWCASTLE * GENERAL One PhD position is available with Dr. Paolo Zuliani at Newcastle University to work on SAT/SMT-based verification techniques for cyber-physical systems. The position is part of a research project with Carnegie Mellon University (USA) funded by the Office of Naval Research, and it covers stipend (14,790GBP per year) and tuition fees for three years. This project is a collaborative effort between Carnegie Mellon University, Newcastle University, and Smart Information Flow Technologies. The Principal Investigator is Prof. Edmund M. Clarke, co-recipient of the 2007 ACM Turing Award. The project investigator at Newcastle is Dr. Paolo Zuliani. * ADVERTISEMENT, PROJECT SUMMARY AND DEADLINE Closing Date: 31st May 2013 http://www.ncl.ac.uk/postgraduate/funding/search/list/cs040 https://sites.google.com/site/zupaolo/ONRsummary.pdf?attredirects=0 * CONTACT Dr. Paolo Zuliani, firstname.lastname@example.org EUROPEAN MASTER'S PROGRAM IN COMPUTATIONAL LOGIC * GENERAL We are glad to announce to you the possibility to join our European Master's Program of Computational Logic. This program is offered jointly at the Free-University of Bozen-Bolzano in Italy, the Technische Universität Dresden in Germany, the Universidade Nova de Lisboa in Portugal and the Technische Universität Wien in Austria. Within this program you have the choice to study at two /three of the four European universities. In addition you can do your project work at the National ICT of Australia (NICTA). You will graduate with a MSc in Computer Science and obtain a multiple degree. * FURTHER DETAILS Information on the universities and the program is provided here: http://www.emcl-study.eu/home.html. Language of instruction is English. Tuition fees are 3.000 EUR (for non-European students) and 1.000 (for European students) per year. The ERASMUS-MUNDUS consortium offers tuition fee waivers and small grants (http://www.emcl-study.eu/grants.html). More information on the application procedure is available from: http://www.emcl-study.eu/application.html Application deadline is 31 May, applicants must use our online application system.
Back to the LICS web page.