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
sat2013@easychair.org . 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 blast2013@chapman.edu
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 (lkovacs@complang.tuwien.ac.at), 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: w.j.fokkink@vu.nl)
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
(ddino@eecs.qmul.ac.uk). 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, paolo.zuliani@ncl.ac.uk
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.