Newsletter 152
November  1, 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
  CSL-LICS'14
* DEADLINES
  Forthcoming Deadlines
* CALLS
  LIX Colloquium - Call for Participation
  SMC 2014 - Call for Participation
  I&C ICC - Call for Papers
  FM 2014 - Call for Papers, Workshops and DOC Symposium
  NASA FM SYMPOSIUM - Call for Papers
  TAMC 2014 - Call for Papers
  PODS 2014 - Call for Papers
  DAN DAVID PRIZE AND SCHOLARSHIPS - Call for Nominations and Applications
  FESCA 2014 - Call for Papers
  FLOPS 2014 - Call for Papers
  QAPL 2014 - Call for Papers
  WRLA 2014 - Call for Submissions
  EAPLS PHD AWARD 2012 - Call for Nominations
  DICE 2014 - Call for Contributions
  CMCS 2014 - Call for Papers
  IJCAR 2014 - Call for Papers
  MSCS COMPUTABLE ANALYSIS - Call for Submissions
  ESSAYS IN MEMORY OF MARK STICKEL - Call for Papers
  AiML 2014 - Call for Papers
* JOB ANNOUNCEMENTS
  PhD and Postdoc at University of Innsbruck
  Two PhD or Postdoc Positions at University of Twente
  Two Software Developers at Embedded Systems Unit of FBK, Trento
  Two Research Positions at Embedded Systems Unit of FBK, Trento
  PhD Position on Model-Based Testing of Software Product Lines at Halmstad, Sweden


CSL-LICS'14
* Next year LICS and CSL will hold a joint conference for the first time,
  as part of FLoC 2014. Tom Henzinger and Dale Miller are co-chairs of a
  joint PC of 38 members. The proceedings will be published by IEEE.
  The Call for Papers is available on the LICS website.
  http://lics.siglog.org/csl-lics14/
* Title and Short Abstracts Due        January 13, 2014
  Full Papers Due                      January 20, 2014



DEADLINES
* INFORMATION AND COMPUTATION SPECIAL ISSUE ON ICC
  Submission deadline: November 1, 2013
  http://dice2013.di.unito.it/
* FM 2014
  Abstract due: November 7, 2013
  Full papers due: November 14, 2013
  http://www.comp.nus.edu.sg/~pat/FM2014/
* NASA Formal Methods Symposium
  Abstract Submission: November 14, 2013
  Paper Submission:    November 21, 2013
  http://www.NASAFormalMethods.org/
* TAMC 2014
  Submission Deadline: November 15, 2013 (11:59pm EST)
  http://www.annauniv.edu/tamc2014/
* PODS 2014
  Abstract submission: November 25, 2013
  Paper submission: December 2, 2013
  http://www.sigmod2014.org/
* DAN DAVID PRIZE AND SCHOLARHIPS 2014
  Nomination deadline: November 30, 2013
  Applications deadline: February 28, 2014
  http://www.dandavidprize.org/prize-nominations
* FESCA 2014
  Paper registration: December 6, 2013
  Submission deadline: December 13, 2013
  http://fesca.ipd.kit.edu/fesca2014/
* FLOPS 2014
  Submission deadline: December 13, 2013
  http://www.jaist.ac.jp/flops2014/
* QAPL 2014
  Abstract (optional): December 24, 2013
  Submission (regular paper): December 31, 2013
  http://qapl14.inria.fr
* WRLA 2014
  Submission deadline: December 30th 2013
  http://www.dsic.upv.es/workshops/wrla2014/
* EAPLS PhD AWARD 2012
  Nomination deadline: December 31, 2013
  http://eapls.org/pages/phd_award/
* DICE 2014
  Abstract submission: January 5, 2014
  Notification: January 20, 2014
* CMCS 2014
  Abstract regular papers: 6 January 2014
  Submission regular papers: 10 January 2014 (strict)
  http://www.coalg.org/cmcs14
* CSL-LICS 2014
  Title and Short Abstracts Due: January 13, 2014
  Full Papers Due: January 20, 2014
  http://lics.siglog.org/csl-lics14/
* IJCAR 2014
  Abstract submission deadline: January 15, 2014
  Paper submission deadline: January 22, 2014
  http://cs.nyu.edu/ijcar2014/
* MSCS SPECIAL ISSUE ON COMPUTABLE ANALYSIS
  Abstracts submission deadline: January 31, 2014
  Deadline for full paper: February 28, 2014
  http://www.cs.swan.ac.uk/ccc2013/
* ESSAYS IN MEMORY OF MARK STICKEL
  Submission deadline: March 1, 2014
  https://www.easychair.org/conferences/?conf=festschriftmarkstick
* AiML 2014
  Abstract of full paper submission due: March 14, 2014
  Full paper submission due: March 21, 2014
  http://www.philos.rug.nl/AiML2014/



LIX COLLOQUIUM ON THE THEORY AND APPLICATION OF FORMAL PROOFS
  http://www.lix.polytechnique.fr/colloquium2013/
  5-7 November 2013
  Ecole Polytechnique, Palaiseau, France
  In association with: PSATTT, 8 Nov 2013.
* EVENTS
  This three-day colloquium will be composed of a number of hour long
  talks by invited speakers and 30 minute talks based on contributed
  abstracts. It is meant as a venue for the exchange of ideas. No
  proceedings are planned apart from a simple collection of short
  abstracts of all talks.
  The colloquium will be followed by the workshop: Proof Search in
  Axiomatic Theories and Type Theories (PSATTT) 2013.
* THEME
  Formal proofs are becoming increasingly important in a number of
  domains in computer science and mathematics. The topic of the
  colloquium is structural proof theory, broadly construed.
  The following are some examples of relevant topics:
  - STRUCTURE OF PROOFS
    sequential and parallel structures in proofs; sharing and
    duplication of subproofs; permutations of proof steps; canonical
    forms; focusing and polarities; graphical proof syntax; proof
    complexity
  - CHECKING PROOFS
    generating, transmitting, translating, and checking proof objects;
    universal proof languages; proof certificates; proof compression;
    cut-introduction; certification of high-performance systems (SMT,
    resolution, etc.)
  - PROOF SEARCH
    automated and interactive proof search in constrained logics
    (linear, temporal, bunched, probabilistic, etc.); combining
    deduction and computation in search; reasoning about inductive and
    co-inductive fixpoints; cyclic proofs; computational
    interpretations of proof search
  - COMPUTING WITH PROOFS
    cut-elimination strategies; cut-elimination by resolution (CERes);
    Curry-Howard correspondence
  These lists are not exhaustive.
* INVITED SPEAKERS
  Chad E. Brown, Saarland University
  Agata Ciabattoni, TU Vienna
  David Delahaye, CNAM, invited by PSATTT
  Alessio Guglielmi, University of Bath
  Dominic Hughes, Stanford University
  Sara Negri, University of Helsinki
  Claudio Sacerdoti Coen, University of Bologna
  Alex Simpson, University of Edinburgh
  [More to be confirmed]
* CALL FOR ABSTRACTS AND PARTICIPATION
  The colloquium is free and open to all, but registration is requested.
  If you would like to attend, please send a mail to Kaustuv Chaudhuri
  .
  If you would like to contribute a 30 minute presentation related to the
  themes of the colloquium, please submit a 1-2 page abstract (as
  PDF) via EasyChair at https://www.easychair.org/conferences/?conf=tafp2013
  The deadline for submissions is 1 October 2013. Decisions on
  submissions will be made before 8 October 2013.
* VENUE
  The colloquium and the PSATTT workshop will take place in the
  Laboratoire d'Informatique (LIX) of the Ecole Polytechnique. The
  Polytechnique is situated in the southern suburbs of Paris, about
  40 minutes from central Paris by regional train. LIX is co-located
  with INRIA Saclay.
* ORGANIZERS
  Dale Miller, Lutz Strassburger, Stephane Graham-Lengrand, Assia
  Mahboubi, Kaustuv Chaudhuri
* SUPPORT
  - Laboratoire d'Informatique (LIX) of the Ecole Polytechnique
    http://www.lix.polytechnique.fr/
  - ERC Advanced Grant ProofCert
    https://team.inria.fr/parsifal/proofcert/
* SEE ALSO
   - PSATTT Workshop 2013
     http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT13/
   - Travelling to LIX/Ecole Polytechnique
     https://team.inria.fr/parsifal/meetings/directions/



MATHEMATICAL STRUCTURES OF COMPUTATION (SMC 2014)
  Call for Participation
  January 13 - February 14 2014, Lyon, France
  http://smc2014.univ-lyon1.fr
* We are pleased to announce the programme "Mathematical Structures of
  Computation" organised in Lyon, from January 13th to February 14th, 2014.
* The programme proposes five consecutive workshops
  - Recent Developments in Type Theory, January 13-17.
  - Algebra and Computation, January 20-24.
  - Directed Algebraic Topology and Concurrency, January 27-31.
  - Formal Proof, Symbolic Computation and Computer Arithmetic, February 3-7.
  - Concurrency, Logic and Types, February 10-14.
* The program of the workshops 3-4-5 is partially open ; please feel
  free to propose talks to the corresponding organisers (contacts are
  available on the above web-page).
* Registration for one or several of these workshops is free, but
  needs to be performed on
  http://smc2014.univ-lyon1.fr/doku.php?id=registration
* Financial support for PhD students and postdocs for accomodation is
  available upon request to organiser of each workshop, deadline to apply
  for financial support is October 31 2013.
* The weeks Mathematical Structures of Computation are organised in Lyon
  with the support of the Labex MILYON - Mathematics and fundamental
  computer science in Lyon.
  Together with the trimester Semantics of proofs and certified
  mathematics organised at Institut Henri Poincare, Paris,
  (http://ihp2014.pps.univ-paris-diderot.fr) they constitute a French
  Semester on certified mathematics, programming languages and the
  mathematical structures of computation.
* The organisers: Patrick Baillot, Yves Guiraud, Philippe Malbos.



INFORMATION & COMPUTATION SPECIAL ISSUE ON IMPLICIT COMPUTATIONAL COMPLEXITY
  Call for Papers
  http://dice2013.di.unito.it
* GUEST EDITORS
  Simona Ronchi Della Rocca (ronchi@di.unito.it)
  Virgile Mogbil (virgile.mogbil@lipn.univ-paris13.fr)
* DATES
  Deadline: November 1st 2013
  Notification: May 15th 2013
* SCOPE
  The area of Implicit Computational Complexity (ICC) has grown out
  from several proposals to use logic and formal methods to delineate
  complexity-bounded computation (e.g. polynomial time, polynomial space
  or logspace computation). It aims at studying computational complexity
  without referring to external measuring conditions or a particular
  machine model, but only by considering language restrictions or
  logical/computational  principles implying complexity properties.
* TOPICS
  Contributions on various aspects of ICC including (but not exclusively)
  are welcome :
  - types for controlling complexity,
  - logical systems for implicit computational complexity,
  - linear logic,
  - semantics of complexity-bounded computation,
  - complexity analysis,
  - rewriting and termination orderings,
  - interpretation-based methods for implicit complexity,
  - programming languages for complexity bounded computation,
  - application of implicit complexity to other programming paradigms (e.g. imperative
    or object-oriented languages).
  This post-conference publication of DICE 2013 (http://dice2013.di.unito.it/)
  is open to everyone, also those who did not participate in the conference.
  It follows a series of annual workshop as satellite events of ETAPS :
  DICE 2010 in Paphos, DICE 2011 in Saarbrucken, DICE 2012 in Tallinn and
  DICE 2013 in Rome.
* SUBMISSIONS
  Submissions must be sent to us no later than NOVEMBER 1st 2013.
  Papers will be processed as soon as they are submitted.
  I&C solicits high quality papers reporting research results related to
  the topics mentioned above.
  All papers must be original, unpublished, and not submitted for publication
  elsewhere. Contributions should be submitted electronically as PDF, using
  Elsevier's elsarticle.cls latex macro package, that can be retrieved from
  http://www.elsevier.com/wps/find/authorsview.authors/elsarticle
  We encourage authors to look at
  http://www.elsevier.com/journals/information-and-computation/0890-5401/guide-for-authors
* ADDITIONAL INFORMATION
  See http://dice2013.di.unito.it/
  or email inquiries to us (ronchi@di.unito.it or virgile.mogbil@lipn.univ-paris13.fr)



19TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS (FM 2014)
  Call for Papers/Workshops/DOC Symposium
  Singapore, May 14-16, 2014
  http://www.comp.nus.edu.sg/~pat/FM2014/
* SERIES
  FM 2014 is the nineteenth in a series of symposia organized by
  Formal Methods Europe, an independent association whose aim is
  to stimulate the use of, and research on, formal methods for
  software development. The symposia have been notably successful
  in bringing together innovators and practitioners in precise
  mathematical methods for software and systems development,
  industrial users, as well as researchers. Submissions are
  welcomed in the form of original papers on research and
  industrial experience, proposals for workshops and tutorials,
  entries for the exhibition of software tools and projects, and
  reports on ongoing doctoral work.
* SCOPE AND TOPICS
  It will have the goal of highlighting the development and
  application of formal methods in connection with a variety of
  disciplines such as medicine, biology, human cognitive modeling,
  human automation interactions and aeronautics, among others. FM
  2014 particularly welcomes papers on techniques, tools and
  experiences in interdisciplinary frameworks, as well as on
  experience with practical applications of formal methods in
  industrial and research settings, experimental validation of
  tools and methods as well as construction and evolution of
  formal methods tools. The broad topics of interest for FM 2014
  include but are not limited to:
  - Interdisciplinary formal methods: techniques, tools and
  experiences demonstrating formal methods in interdisciplinary
  frameworks.
  - Formal methods in practice: industrial applications of formal
  methods, experience with introducing formal methods in industry,
  tool usage reports, experiments with challenge problems. Authors
  are encouraged to explain how the use of formal methods has
  overcome problems, lead to improvements in design or provided
  new insights.
  - Tools for formal methods: advances in automated verification and
  model-checking, integration of tools, environments for formal
  methods, experimental validation of tools. Authors are
  encouraged to demonstrate empirically that the new tool or
  environment advances the state of the art.
  - Role of formal methods in software and systems engineering:
  development processes with formal methods, usage guidelines for
  formal methods, method integration. Authors are encouraged to
  demonstrate that process innovations lead to qualitative or
  quantitative improvements.
  - Theoretical foundations: all aspects of theory related to
  specification, verification, refinement, and static and dynamic
  analysis. Authors are encouraged to explain how their results
  contribute to the solution of practical problems.
* PAPER SUBMISSION
  Papers will be evaluated by at least three members of the
  Program Committee. They should be in Springer LNCS format and
  describe, in English, original work that has not been published
  or submitted elsewhere. Papers should be submitted through the
  FM 2014 EasyChair web site at:
  http://www.easychair.org/conferences/?conf=fm2014
  Accepted papers will be published in the Symposium Proceedings,
  to appear in Springer's Lecture Notes in Computer Science.
* IMPORTANT DATES
  Abstract due: November 7, 2013
  Full papers due: November 14, 2013
  Acceptance / Rejection Notification: February 1, 2014
  Industry Track Submission: January 16, 2014
  Industry Track Notification: February 16, 2014
  Camera-ready: February 25, 2014
  Main Conference Date: May 14-16, 2014
  Tutorial / Workshops Date: May 12-13, 2014
* CALL FOR TUTORIALS, WORKSHOPS and DOC SYMPOSIUM
  The organizing committee of FM 2014 thus invites proposals for
  half- or full-day tutorials in the broad area of formal methods.
  Proposals from industry practitioners or academics are very
  welcome; proposals for tutorials on applications of formal
  methods to challenging problems are particularly welcome. All
  tutorials should focus on providing participants with the
  opportunity to learn new techniques, new application domains,
  and insightful uses of formal methods. Details on the call for
  tutorials can be found at
  http://www.comp.nus.edu.sg/~pat/FM2014/cft.html
  We are also inviting people to submit proposals for workshops.
  The purpose of the workshops is to provide an informal setting
  for workshop participants to discuss technical issues, exchange
  research ideas, and to discuss and/or demonstrate applications.
  These workshops may be driven by fundamental academic interests
  or by needs from specific application domains. We encourage a
  diversity of workshops relating to different varieties of formal
  models. Details on the call for workshops can be found at
  http://www.comp.nus.edu.sg/~pat/FM2014/cfp4w.html
* DOC SYMPOSIUM
  A Doctoral Symposium will be held on 12-13th May in conjunction
  with the FME Symposium FM2014. This aims to provide a helpful
  environment in which selected doctoral students can present and
  discuss their ongoing work, meet other students working on
  similar topics and receive helpful advice and feedback from a
  panel of researchers and academics. Details on the call for
  doctoral sympisum can be found at
  http://www.comp.nus.edu.sg/~pat/FM2014/cfd.html
* GENERAL CHAIR
  Jin Song Dong, National University of Singapore, Singapore.
* PC CHAIRS
  Cliff B Jones, Newcastle University, United Kindom.
  Pekka Pihlajasaari, Data Abstraction (Pty) Ltd, South Africa.
  Jun Sun, Singapore University of Technology and Design, Singapore.
* DOC SYMPOSIUM
  Annabelle McIver, Macquarie University, Australia.
* WORKSHOP CHAIR
  Shengchao Qin, University of Teesside, United Kindom.
* TUTORIAL CHAIR
  Richard Paige, University of York, United Kindom.



SIXTH NASA FORMAL METHODS SYMPOSIUM
  Call for Papers
  29 April - 1 May 2014
  NASA Johnson Space Center
  Houston, Texas, USA
  http://www.NASAFormalMethods.org/
* THEME
  The widespread use and increasing complexity of mission- and
  safety-critical systems require advanced techniques that address their
  specification, verification, validation, and certification requirements.
  The NASA Formal Methods Symposium is a forum for theoreticians and
  practitioners from academia, industry, and government, with the goals of
  identifying challenges and providing solutions to achieving assurance in
  mission- and safety-critical systems. Within NASA such systems include
  autonomous robots, separation assurance algorithms for aircraft, Next
  Generation Air Transportation (NextGen), and autonomous rendezvous and
  docking for spacecraft. Moreover, emerging paradigms such as
  property-based design, code generation, and safety cases are bringing
  with them new challenges and opportunities. The focus of the symposium
  will be on formal techniques, their theory, current capabilities, and
  limitations, as well as their application to aerospace, robotics, and
  other safety-critical systems in all design life-cycle stages. We
  encourage submissions on cross-cutting approaches marrying formal
  verification techniques with advances in safety-critical system
  development, such as requirements generation, analysis of aerospace
  operational concepts, and formal methods integrated in early design
  stages carrying throughout system development.
* TOPICS
     - Model checking
     - Theorem proving
     - Static analysis
     - Model-based development
     - Runtime monitoring
     - Formal approaches to fault tolerance
     - Applications of formal methods to aerospace systems
     - Formal analysis of cyber-physical systems, including hybrid and
       embedded systems
     - Formal methods in systems engineering, modeling, requirements,
       and specifications
     - Requirements generation, specification debugging, formal
       validation of specifications
     - Use of formal methods in safety cases
     - Use of formal methods in human-machine interaction analysis
     - Formal methods for parallel hardware implementations
     - Use of formal methods in automated software engineering and testing
     - Correct-by-design, design for verification, and property-based
       design techniques
     - Techniques and algorithms for scaling formal methods; e.g.
       abstraction and symbolic methods, compositional techniques, parallel and
       distributed techniques
     - Application of formal methods to emerging technologies
* IMPORTANT DATES
  Abstract Submission: 14 Nov 2013
  Paper Submission:    21 Nov 2013
  Paper Notifications: 14 Jan 2014
  Camera-ready Papers: 11 Feb 2014
  Symposium: 29 April - 1 May 2014
* LOCATION
  The symposium will take place at the Gilruth Center, NASA Johnson Space
  Center, Houston, Texas, USA, 29 April to 1 May 2013.
  There will be no registration fee for participants. All interested
  individuals, including non-US citizens, are welcome to attend, to listen
  to the talks, and to participate in discussions; however, all attendees
  must register.
* SUBMISSION DETAILS
  There are two categories of submissions:
    1. Regular papers describing fully developed work and complete
  results (15 pages)
    2. Short papers describing tools, experience reports, or
  descriptions of work in progress with preliminary results (6 pages)
  All papers should be in English and describe original work that has not
  been published or submitted elsewhere. All submissions will be fully
  reviewed by members of the Programme Committee. Papers will appear in a
  volume of Springer's Lecture Notes on Computer Science (LNCS), and must
  use LNCS style formatting. Papers should be submitted in PDF format.
* KEYNOTES SPEAKERS
  - Larry Paulson, University of Cambridge, UK
  - Moshe Y. Vardi, Rice University, USA
  - Special Guest Talk: "NASA Future Challenges in Formal Methods"
* ORGANIZERS
  Mike Hinchey (General Chair)
  Julia Badger (PC Chair)
  Kristin Yvonne Rozier (PC Chair)



11TH ANNUAL CONFERENCE ON THEORY AND APPLICATIONS OF MODELS OF COMPUTATION (TAMC 2014)
  11--13 April 2014
  Vivekananda Auditorium, Anna University, Chennai, India
  http://www.annauniv.edu/tamc2014/
* IMPORTANT DATES
  Submission Deadline: 15 November 2013 (11:59pm EST)
  Notification of Acceptance: 15 December 2013
  Final Camera Ready Version Due: 15 January 2014
* PROCEEDINGS
  Springer Lecture Notes in Computer Science
* SCOPE AND TOPICS
  TAMC 2014 aims at bringing together a wide range of researchers with
  interests in computational theory and applications. The main themes of the
  conference are computability, complexity, algorithms, models of
  computation and systems theory.



33RD ACM SIGMOD-SIGACT-SIGART SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS (PODS 2014)
  Call for Papers
  June 23-25, 2014
  Snowbird, Utah, USA
  http://www.sigmod2014.org/
* The PODS symposium series, held in conjunction with the SIGMOD
  conference series, provides a premier annual forum for the
  communication of new advances in the theoretical foundations of
  data management, traditional or non-traditional
  (see http://www.sigmod.org/the-pods-pages).
* Topics that fit the interests of the symposium include the following:
  design, semantics, and optimization of query and database languages;
  data modeling; data structures and algorithms for data management;
  dynamic aspects of databases (updates, views); query languages for
  semi-structured data (including XML and RDF); search query languages
  (including techniques from information retrieval); web services;
  automatic verification of database-driven systems; incompleteness,
  inconsistency, and uncertainty in databases; constraints
  (specification, reasoning, mining, constraint databases); domain-
  specific databases (multi-media, scientific, spatial, temporal, text);
  schema and query extraction; mining and learning of data models and
  queries; data integration; data exchange; provenance; workflows;
  metadata management; meta-querying; semantic, linked, networked, and
  crowdsourced data; foundation of "big data"; recommendation systems
  and social networks; distributed and parallel aspects of data
  management; cloud computing and distributed query processing; data
  streams; real-time and sensor data; approximate query answering;
  privacy; security; model theory, logics, algebras and computational
  complexity.
* Important dates:
  Abstract submission: November 25, 2013;
  Paper submission: December 2, 2013;
  Notification: February 24, 2014



2014 DAN DAVID PRIZE AND SCHOLARSHIPS: ARTIFICIAL INTELLIGENCE, THE DIGITAL MIND
  Call for Nominations and Scholarships
  http://www.dandavidprize.org/prize-nominations
* PRIZE
  Three prizes are awarded annually in fields chosen within the three time
  dimensions -- Past, Present, and Future. The selected field for 2014 in
  the Future dimension is Artificial Intelligence, the Digital Mind.
  The Dan David Prize is awarded to individuals and institutions with
  proven, exceptional excellence and contribution to humanity in the
  sciences, arts, humanities, public service and business.
* DEADLINE
  Nominations deadline: November 30, 2013
  Email: ddprize@post.tau.ac.il
* SCHOLARSHIPS
  Each year the Dan David Prize awards 20 scholarships of US$ 15,000
  each to outstanding doctoral students and postdoctoral researchers; 10
  scholarships are awarded to students from universities all over the world
  and 10 scholarships to students from Tel Aviv University. Advanced
  doctoral and postdoctoral students of excellent achievement and promise
  studying topics related to the fields chosen for this year are invited to
  apply for the Dan David Prize Scholarships 2014.
  Applications deadline: February 28, 2014 For details regarding scholarships,
  please consult the website: http://www.dandavidprize.org



11TH INTERNATIONAL WORKSHOP ON FORMAL ENGINEERING APPROACHES TO SOFTWARE COMPONENTS AND ARCHITECTURES (FESCA 2014)
  Call for Papers
  (Satellite event of ETAPS)
  April 12th, 2014, Grenoble, France
  http://fesca.ipd.kit.edu/fesca2014/
* WORKSHOP AIM
  In recent years, the growing importance of functional correctness and
  the increased relevance of system quality properties (e.g. performance,
  reliability, security) have stimulated the emergence of analytical and
  modelling techniques for the design and development of software systems.
  With the increasing complexity of today's software systems, FESCA aims
  at addressing two research questions: (1) what role the software
  architecture can play in systematic addressing of the analytical and
  modelling challenges, and (2) how formal and semi-formal techniques can
  be applied effectively to make the issues easier to address
  automatically, with lower human intervention.
* TOPICS
  We encourage submissions on (semi-)formal techniques and their
  application that aid analysis, design and implementation of software
  applications, including the techniques in the realm of Model-Driven
  Development.
  In this context, the topics include (but are not limited to):
  Modelling
   - Modelling formalisms;
   - Models, metamodels and model transformations;
  Correctness checking
   - Temporal properties and their formal verification;
   - Interface compliance and contractual use of components;
  Correctness of models, metamodels and model transformations
  Analysis and prediction of quality attributes
   - Formal prediction and analysis;
   - Static and dynamic analysis;
   - Instrumentation and monitoring approaches;
  Industrial case studies and experience reports.
  Besides general software systems, FESCA is interested in methods
  focusing on a specific application domain, such as:
  - Cloud environment
  - Mobile and embedded systems
  - Information systems
  - Hardware infrastructures
  We encourage not only mature research results, submissions presenting
  innovative ideas and early results are also of interest.
* SUBMISSIONS
  Three kinds of submissions are solicited:
  - regular papers (up to 15 pages) presenting original and unpublished
  work related to the workshop topics,
  - position papers (up to 10 pages) presenting ideas and directions of
  interesting ongoing and yet unpublished research related to the workshop
  topics, and
- tool demonstration papers (up to 8 pages) presenting and highlighting
  the distinguishing features of a topic-related tool (co-developed by the
  authors).
* PROCEEDINGS
  -  Final versions of accepted regular and position papers will be
  published in a volume of the Electronic Proceedings in Theoretical
  Computer Science (EPTCS).
  -  The tool demonstration papers will not appear in the EPTCS
  proceedings, but will be included in the electronic pre-proceedings
  (distributed at the workhop) and made available on the workshop website.
* IMPORTANT DATES
  - Paper registration: December 6, 2013
  - Submission deadline: December 13, 2013
  - Notification of acceptance: January 20, 2014
  - Final versions due: February 10, 2014
  - Workshop date:  April 12, 2014
* PC CO-CHAIRS
  - Barbora Buhnova (Masaryk University, Czech Republic)
  - Lucia Happe (Karlsruhe Institute of Technology, Germany)
  - Jan Kofron (Charles University in Prague, Czech Republic)



12TH INTERNATIONAL SYMPOSIUM ON FUNCTIONAL AND LOGIC PROGRAMMING (FLOPS 2014)
  Call for Papers
  June 4-6, 2014
  Kanazawa, Japan
  http://www.jaist.ac.jp/flops2014/
* GENERAL
  FLOPS is a forum for research on all issues concerning declarative
  programming, including functional programming and logic programming,
  and aims to promote cross-fertilization and integration between the
  two paradigms.  Previous FLOPS meetings were held at Fuji Susono
  (1995), Shonan Village (1996), Kyoto (1998), Tsukuba (1999), Tokyo
  (2001), Aizu (2002), Nara (2004), Fuji Susono (2006), Ise (2008),
  Sendai (2010), and Kobe (2012).
* TOPICS
  FLOPS solicits original papers in all areas of functional and logic
  programming, including (but not limited to):
  - Language issues: language design and constructs, programming
  methodology, integration of paradigms, interfacing with other
  languages, type systems, constraints, concurrency and distributed
  computing.
  - Foundations: logic and semantics, rewrite systems and narrowing,
  type theory, proof systems.
  - Implementation issues: compilation techniques, memory management,
  program analysis and transformation, partial evaluation,
  parallelism.
  - Applications: case studies, real-world applications, graphical user
  interfaces, Internet applications, XML, databases, formal methods
  and model checking.
  The proceedings will be published as an LNCS volume.  The proceedings
  of the previous meetings (FLOPS 1999, 2001, 2002, 2004, 2006, 2008,
  2010, and 2012) were published as LNCS 1722, 2024, 2441, 2998, 3945,
  4989, 6009, and 7294.
* PC CO-CHAIRS
  Michael Codish     (Ben-Gurion University of the Negev)
  Eijiro Sumii       (Tohoku University)
* LOCAL CHAIR
  Yuki Chiba         (JAIST)
* SUBMISSION
  Submissions must be unpublished and not submitted for publication
  elsewhere.  Work that already appeared in unpublished or informally
  published workshops proceedings may be submitted.  See also ACM
  SIGPLAN Republication Policy:
  http://www.sigplan.org/Resources/Policies/Republication
  Submissions should fall into one of the following categories:
  - Regular research papers: they should describe new results and will
  be judged on originality, correctness, and significance.
  - System descriptions: they should contain a link to a working system
  and will be judged on originality, usefulness, and design.
  - Declarative pearls: new and excellent declarative programs or
  theories with illustrative applications.
  System descriptions and declarative pearls must be explicitly marked
  as such in the title.
* SUBMISSIONS
  Submissions must be written in English and can be up to 15 pages long
  including references, though pearls are typically shorter.  Authors
  are required to use LaTeX2e and the Springer llncs class file,
  available at: http://www.springer.de/comp/lncs/authors.html
  Regular research papers should be supported by proofs and/or
  experimental results.  In case of lack of space, this supporting
  information should be made accessible otherwise (e.g., a link to a Web
  page, or an appendix).  Papers should be submitted electronically at:
  https://www.easychair.org/conferences/?conf=flops2014
* IMPORTANT DATES
  Submission deadline: December 13, 2013
  Author notification: February 10, 2014
  Camera-ready copy: March 7, 2014



12TH WORKSHOP ON QUANTITATIVE ASPECTS OF PROGRAMMING LANGUAGES AND SYSTEMS (QAPL 2014)
  Affiliated with ETAPS 2014
  April 12 - 13, 2014, Grenoble, France
  http://qapl14.inria.fr
* SCOPE
  Quantitative aspects of computation are important and sometimes essential in
  characterising the behaviour and determining the properties of systems. They
  are related to the use of physical quantities (storage space, time, bandwidth,
  etc.) as well as mathematical quantities (e.g. probability and measures for
  reliability, security and trust). Such quantities play a central role in
  defining both the model of systems (architecture, language design, semantics)
  and the methodologies and tools for the analysis and verification of system
  properties. The aim of this workshop is to discuss the explicit use of
  quantitative information such as time and probabilities either directly in the
  model or as a tool for the analysis of systems.
  In particular, the workshop focuses on:
  - the design of probabilistic, real-time, quantum languages and the
    definition of semantical models for such languages
  - the discussion of methodologies for the quantitative analysis of
    systems, for instance probabilistic and timing properties (e.g.
    security, safety, schedulability) and other quantifiable properties
    such as reliability (for hardware components), trustworthiness
    (in information security) and resource usage (e.g., worst-case
    memory/stack/cache requirements);
  - the probabilistic analysis of systems which do not explicitly incorporate
    quantitative aspects (e.g. performance, reliability and risk analysis)
  - applications to safety-critical systems, communication protocols, control
    systems, asynchronous hardware, and to any other domain involving
    quantitative issues
* TOPICS
  Topics include (but are not limited to) probabilistic, timing and general
  quantitative aspects in: Language design, Information systems, Asynchronous HW
  analysis, Language extension, Multi-tasking systems, Automated reasoning,
  Language expressiveness, Logic, Verification, Quantum languages, Semantics,
  Testing, Time-critical systems, Performance analysis, Safety, Embedded systems,
  Program analysis, Risk and hazard analysis, Coordination models, Protocol
  analysis, Scheduling theory, Distributed systems, Model-checking, Security,
  Biological systems, Cyber-physical systems, Concurrent systems, and Resource analysis.
* INVITED SPEAKERS
  - Stephen Gilmore, University of Edinburgh, UK
  - Oded Maler, Verimag, France
  - Nicolas Markey, LSV, CNRS and ENS Cachan, France
  - Enrico Vicario, University of Firenze, Italy
* SUBMISSIONS
  In order to encourage participation and discussion, this workshop solicits two
  types of submissions - regular papers and presentation reports:
  1. Regular paper submissions must be original work, and must not have been
     previously published, nor be under consideration for publication
     elsewhere. Regular paper submission must not exceed 15 pages, possibly
     followed by a clearly marked appendix which will be removed for the
     proceedings and contains technical material for the reviewers.
  2. Presentation reports concern recent or ongoing work on relevant topics and
     ideas, for timely discussion and feedback at the workshop. There is no
     restriction as for previous/future publication of the contents of a
     presentation. Typically, a presentation is based on a paper which recently
     appeared (or which is going to appear) in the proceedings of another
     recognized conference, or which has not yet been submitted. The (extended)
     abstract of presentation submissions should not exceed 4 pages.
  All submissions must be in PDF format and use the EPTCS latex style, see
  http://style.eptcs.org/. Submissions can be made on the following website:
    http://www.easychair.org/conferences/?conf=qapl14
  The workshop PC will review all regular paper submissions to select
  appropriate ones, ones for acceptance in each category, based on their
  relevance, merit,  originality, and technical content. Presentation reports
  will receive a light weight review to establish their relevance for the
  workshop. The authors of accepted submissions of both types are expected
  to present and discuss their work at the workshop. Accepted regular papers
  will be published in the Electronic Proceedings in Theoretical Computer
  Science (EPTCS). A special issue concerning the QAPL editions of 2011 and
  2012 is in preparation and a further special issues related to the QAPL
  editions of 2013 and 2014  will be considered.
* IMPORTANT DATES
  For regular papers:
    Abstract (optional): December 24, 2013
    Submission (regular paper): December 31, 2013
    Notification: February 7, 2014
    Final version (ETAPS proceedings): February 14, 2014
    Workshop: March 23 - 24, 2013
    Final version (EPTCS post proceedings): TBA
  For presentation reports:
    Submission:   February 5, 2014
    Notification: February 7, 2014
* PC CHAIRS
    - Nathalie Bertrand, INRIA Rennes, France
    - Luca Bortolussi, University of Trieste, Italy



10TH INTERNATIONAL WORKSHOP ON REWRITING LOGIC AND ITS APPLICATIONS (WRLA 2014)
  Grenoble, France, April 5th and 6th, 2014
  http://www.dsic.upv.es/workshops/wrla2014/
  (in conjunction with ETAPS 2014
  17th European Joint Conferences on Theory and Practice of Software
  April 5-13, 2014, http://www.etaps.org/2014)
* AIMS AND SCOPE
  Rewriting logic (RL) is a natural model of computation and an
  expressive semantic framework for concurrency, parallelism,
  communication, and interaction. It can be used for specifying
  a wide range of systems and languages in various application
  fields. It also has good properties as a metalogical framework
  for representing logics. In recent years, several languages
  based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed
  and implemented. The aim of the workshop is to bring together
  researchers with a common interest in RL and its applications,
  and to give them the opportunity to present their recent works,
  discuss future research directions, and exchange ideas.
* IMPORTANT DATES
  Submission deadline          December 30th 2013
  Author notification          February 2nd 2014
  Version informal proceedings February 14th 2014
* SUBMISSIONS
  The final program of the workshop will include regular papers,
  tool papers, and work-in-progress presentations. The program
  will also contain invited talks to be determined by the
  program committee. Papers must contain original contributions,
  be clearly written, include appropriate references, and
  comparison with related work. They must be unpublished and
  not submitted simultaneously for publication elsewhere.
  Tool papers present a new tool, a new tool component, or
  novel extensions to an existing tool. They should provide a
  short description of the theoretical foundations with
  relevant citations, emphasize the design and implementation,
  and give a clear account of the tool's functionality. The
  described tools must be publicly available via the web.
  All submissions should be formatted according to the
  guidelines for Springer LNCS papers, and should be submitted
  electronically using EasyChair.



EAPLS PHD AWARD 2012
  Call for Nominations
  http://eapls.org/pages/phd_award/
* AWARD
  The European Association for Programming Languages and Systems
  has established a Best Dissertation Award in the international
  research area of programming languages and systems. The award
  will go to the PhD student who in the previous period has made
  the most original and influential contribution to the area. The
  purpose of the award is to draw attention to excellent work, to
  help the career of the student in question, and to promote the
  research field as a whole.
* ELIGIBILITY
  Eligible for the award are those who successfully defended their PhD
  - at an academic institution in Europe
  - in the field of Programming Languages and Systems
  - in the period from 1 November 2012 – 1 November 2013
* NOMINATIONS
  Candidates for the award must be nominated by their supervisor.
  Nominating a candidate consists of submitting the thesis to
  https://www.easychair.org/conferences/?conf=eaplsphd2013. The
  nomination must be accompanied by (a zip file containing)
  - a letter from the supervisor describing why the thesis should be
    considered for the award;
  - a report from an independent researcher who has acted as examiner
    of the thesis at its defense.
  The theses will be evaluated with respect to originality, influence,
  relevance to the field and (to a lesser degree) quality of writing.
* PROCEDURE
  The nominations will be evaluated and compared by an international
  committee of experts from across Europe. The procedure to be
  followed is analogous to the review phase of a conference. The
  justification by the supervisor and the external report will play
  an important role in the evaluation.
  Members of the expert committee are barred from nominating their
  own PhD students for the award.
  The award consists of a certificate announcing the winner to have
  received the EAPLS PhD award 2011. The supervisor will receive a
  copy of this certificate. If possible, the certificate will be
  handed out ceremonially at a suitable occasion, as for instance
  the ETAPS conference.
  Apart from the winner, no further ranking of nominees will be
  published. The decision of the expert committee is final and
  binding, and will not be subject to discussion.
* IMPORTANT DATES
  31 December 2013: Deadline for nominations
  10 April 2014:    Announcement of the award winner
* EXPERT COMMITTEE
  The Expert committee includes:
  - Gilles Barthe, IMDEA Software Institute, Spain
  - Eerke Boiten, University of Kent, U.K.
  - Mark van den Brand, Universiteit Eindhoven, The Netherlands
  - Paolo Ciancarini, Universita di Bologna, Italy
  - Stefano Crespi Reghizzi, Politecnico di Milano, Italy
  - Kei Davis, Los Alamos National Laboratory, U.S.A.
  - Mariangiola Dezani, Universita di Torino, Italy
  - Josuka Díaz-Labrador, Universidad de Duesto, Spain
  - Marko van Eekelen, Radboud Universiteit Nijmegen, The Netherlands
  - Giorgio Ghelli, University of Pisa, Italy
  - Stefan Gruner, University of Pretoria, South Africa
  - Kevin Hammond, University of St Andrews, U.K.
  - Martin Hofmann, Ludwig-Maximilians-Universität München, Germany
  - Paul Klint, CWI and University of Amsterdam, The Netherlands
  - Jens Knoop, Technische Universität Wien, Austria
  - Ralf Lämmel, University of Koblenz-Landau, Germany
  - Rita Loogen, Philipps-Universität Marburg, Germany
  - Tiziana Margaria, University of Potsdam, Germany
  - Greg Michaelson, Heriot-Watt University , Edinburgh, U.K.
  - Alan Mycroft, University of Cambridge, U.K.
  - Catuscia Palamidessi, LIX, France
  - Ricardo Peña, Universidad Complutense de Madrid, Spain
  - Arnd Poetzsch-Heffter, Technische Universität Kaiserslautern, Germany
  - Arend Rensink, Universiteit Twente, The Netherlands
  - Bernhard Steffen, Technische Universität Dortmund, Germany
  - Peter Van Roy, Université Catholique de Louvain, Belgium



5TH WORKSHOP ON DEVELOPMENTS IN IMPLICIT COMPUTATIONAL COMPLEXITY (DICE 2014)
  Call for Contributions
  April 5-6, 2014
  Grenoble, France (a satellite event of ETAPS 2014)
  http://dice14.tcs.ifi.lmu.de
* SCOPE AND TOPIC
  The area of Implicit Computational Complexity (ICC) has grown from
  several proposals for using logic and formal methods to provide
  languages for complexity-bounded computation (e.g. PTIME, LOGSPACE
  computation). Its aim is to study computational complexity without
  reference to external measuring conditions or particular machine
  models, but only in terms of language restrictions or
  logical/computational principles implying complexity properties.
  This workshop focuses on ICC methods related to programs (rather than
  descriptive methods). In this approach one relates complexity classes
  to restrictions on programming paradigms (functional programs, lambda
  calculi, rewriting systems), such as ramified recurrence, weak
  polymorphic types, linear logic and linear types, and interpretative
  measures. The two main objectives of this area are:
  - to find natural implicit characterizations of various
    complexity classes of functions, thereby illuminating their
    nature and importance;
  - to design methods suitable for static verification of
    program complexity.
  Therefore ICC connects both to the study of complexity classes and to
  static program analysis.  The workshop is open to contributions
  on various aspects of ICC including (but not exclusively):
  - types for controlling complexity
  - logical systems for implicit computational complexity
  - linear logic
  - semantics of complexity-bounded computation
  - rewriting and termination orderings
  - interpretation-based methods for implicit complexity
  - programming languages for complexity-bounded computation
  - theoretical foundations of program complexity analysis
  - application of implicit complexity to security
* INVITED SPEAKERS
  - Akitoshi Kawamura, University of Tokyo
  - Georg Moser, University of Innsbruck
* IMPORTANT DATES
  - Abstract submission: January 5, 2014
  - Notification: January 20, 2014
  - Final version: February 10, 2014
* SUBMISSION
  Authors are invited to submit an extended abstract of up to 5 pages.
  Accepted abstracts will be presented at the workshop. Submissions will
  be judged on originality, relevance, interest and clarity. Preference
  will be given to abstracts describing work (including work in
  progress) that has not been published elsewhere before the workshop.
  Further details can be found at the workshop homepage.



12TH INTERNATIONAL WORKSHOP ON COALGEBRAIC METHODS IN COMPUTER SCIENCE (CMCS'14)
  Call for Papers
  5 - 6 April 2014, Grenoble, France
  http://www.coalg.org/cmcs14
* OBJECTIVES AND SCOPE
  Established in 1998, the CMCS workshops aim to bring together researchers
  with a common interest in the theory of coalgebras, their logics, and their
  applications. As the workshop series strives to maintain breadth in its scope,
  areas of interest include neighbouring fields as well. Topics of interest
  include, but are not limited to, the following:
  - The theory of coalgebras (including set theoretic and categorical
    approaches)
  - Coalgebras as computational and semantical models (for
   programming languages, dynamical systems, term rewriting, etc.)
  - Coalgebras in (functional, object-oriented, concurrent, and constraint)
    programming
  - Model checking, theorem proving and deductive verification
    using coalgebraic techniques
  - Coalgebraic data types, type systems and
    behavioural typing
  - Proof principles and (coinductive) definitions for
    coalgebras (e.g. with bisimulations or invariants)
  - Coalgebras and algebras
  - Coalgebraic specification and verification
  - Coalgebras and (modal) logic
  - Coalgebra and control theory (notably of discrete event
    and hybrid systems)
  - Coalgebra in quantum computing
  -  Coalgebra and game theory
  - Tools exploiting colgebraic techniques
* VENUE AND EVENT
  CMCS’14 will be held in Grenoble, France, co-located with ETAPS 2014 on
  5 - 6 April 2014.
* IMPORTANT DATES
  Abstract regular papers           6 January 2014
  Submission regular papers        10 January 2014 (strict)
  Notification regular papers     14 February 2014
  Camera-ready copy               21 February 2014
  Submission short contributions   23 February 2014 (strict)
  Notification short contributions  9 March 2014
* INVITED SPEAKERS
  Ichiro Hasuo, University of Tokyo, JP
  Marina Lenisa, University of Udine, IT
* PUBLICITY CHAIR
  Alexandra Silva, Radboud University Nijmegen, NL
* PC CHAIR
  Marcello Bonsangue, Leiden University, NL
* SUBMISSION GUIDELINES
  We solicit two types of contributions: regular papers and short contributions.
  Regular papers must be original, unpublished, and not submitted for
  publication elsewhere. They should not exceed 20 pages in length in Springer
  LNCS style. Short contributions may describe work in progress, or summarise
  work submitted to a conference or workshop elsewhere. They should be no more
  than two pages. Regular papers and short contributions should be submitted
  electronically as a PDF file via the Easychair system at
    http://www.easychair.org/conferences/?conf=cmcs2014.
  The proceedings of CMCS 2014 will include all accepted regular papers and
  will be published post-conference as a Springer volume in the IFIP-LNCS
  series. Accepted short contributions will be bundled in a technical report.



7TH INTERNATIONAL JOINT CONFERENCE ON AUTOMATED REASONING (IJCAR 2014)
  Call for Papers
  Vienna, Austria, July 19-22, 2014
  http://cs.nyu.edu/ijcar2014/
  as part of FLoC 2014 - Federated Logic Conference
  http://www.floc-conference.org/
  as part of VSL 2014 - Vienna Summer of Logic
  http://vsl2014.at/
* IJCAR is the premier international joint conference on all topics
  in automated reasoning. The IJCAR technical program will consist
  of presentations of high-quality original research papers,
  system descriptions, and invited talks.
* IJCAR 2014 is a merger of leading events in automated reasoning:
  CADE (Conference on Automated Deduction),
  FroCoS (Workshop on Frontiers of Combining Systems) and
  TABLEAUX (Conference on Analytic Tableaux and Related Methods)
  IJCAR 2014 invites submissions related to all aspects of automated
  reasoning, including foundations, implementations, and applications.
  Original research papers and descriptions of working automated deduction
  systems are solicited.
* TOPICS
  IJCAR topics include the following ones:
  - Logics of interest include: propositional, first-order, classical,
  equational, higher-order, non-classical, constructive, modal,
  temporal, many-valued, substructural, description, type theory, etc.
  - Methods of interest include: tableaux, sequent calculi, resolution,
  model-elimination, inverse method, paramodulation, term rewriting,
  induction, unification, constraint solving, decision procedures,
  model generation, model checking, semantic guidance, interactive
  theorem proving, logical frameworks, AI-related methods for
  deductive systems, proof presentation, automated theorem provers,
  etc.
  - Applications of interest include: verification, formal methods,
  program analysis and synthesis, computer mathematics, declarative
  programming, deductive databases, knowledge representation, etc.
  The proceedings of IJCAR 2014 will be published by Springer-Verlag in
  the LNAI/LNCS series.
* PROGRAM CO-CHAIRS
  Stephane Demri (New York University & CNRS)
  Deepak Kapur (University of New Mexico, USA)
  Christoph Weidenbach (MPI-INF Saarbr??cken, Germany)
* CONFERENCE CO-CHAIRS
  Christian Fermueller (TU Vienna, Austria)
  Stefan Hetzl (TU Vienna, Austria)
* IMPORTANT DATES
  Abstract submission deadline:                     January 15, 2014
  Paper submission deadline:                        January 22, 2014
  Notification of paper decisions:                    March 31, 2014
  Final version of papers due:                        April 19, 2014
  Conference dates:                                 July 19-22, 2014
* STUDENT TRAVEL AWARDS
  Travel awards will be available to enable selected students to attend the
  conference.  Details will be published in March 2014.



MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE SPECIAL ISSUE ON COMPUTABLE ANALYSIS
  Call for Submissions
  http://www.cs.swan.ac.uk/ccc2013/
* GUEST EDITORS
  Hajime Ishihara (JAIST, Japan)
  Margarita Korovina (Novosibirsk, Russia)
  Arno Pauly (Cambridge, UK)
  Monika Seisenberger (Swansea, UK)
  Dieter Spreen (Siegen, Germany, and Pretoria, South Africa)
* DATES
  Abstracts submission deadline: January 31, 2014
  Deadline for full paper: February 28, 2014
* GENERAL
  After a year of successful work in the EU-IRSES project COMPUTAL
  http://computal.uni-trier.de
  and an excellent workshop "Continuity, Computability, Constructivity:
  From Logic to Algorithms (CCC 2013)" in Gregynog (Wales) in June this year,
  we are planning to publish a special issue of MATHEMATICAL STRUCTURES IN
  COMPUTER SCIENCE. The special issue should reflect progress made in
  Computable Analysis and related areas and is open for everyone.
* TOPICS
  Computable analysis
  Complexity of real number computations
  Computing with continuous data
  Domain theory and analysis
  Randomness and computable measure theory
  Models of computation with real numbers
  Realizability theory and analysis
  Reverse analysis
  Exact real number computation
  Program extraction in analysis
* SUBMISSIONS
  We want to split the submission process into two parts: Please, first submit
  an abstract of your paper and then later the full paper. Submit both the
  abstract as well as the full manuscript to
  https://www.easychair.org/account/signin.cgi?conf=ccc2013mscspostproce
  Papers will be processed according to high MSCS standards as soon as they
  are submitted. All papers must be original, unpublished, and not submitted
  for publication elsewhere. Please prepare your manuscript using the MSCS
  style file which can be downloaded from ftp.cup.cam.ac.uk
* ADDITIONAL INFORMATION
  Please email inquiries to spreen@informatik.uni-siegen.de.



MAKING AUTOMATED REASONING PRACTICAL: ESSAYS IN MEMORY OF MARK STICKEL
  Call for Papers
* DEADLINE
  Submission Deadline: March 1st, 2014
* AIM
  This is a book of collected articles presenting research in all aspects of
  automated reasoning, in particular the design of automated reasoning
  systems and their applications.
  A common theme behind Mark Stickel's work was developing techniques for
  building better automated reasoning systems. His discoveries were
  ground-breaking and include AC-unification, reasoning modulo a theory, term
  indexing, and thorough development of the SNARK and PTTP provers. In 2002 he
  received the Herbrand award for all his work, the highest award in automated
  reasoning (http://www.cadeinc.org/).
  We would like to honour Mark's achievements by editing a Festschrift
  comprised of articles in the spirit of his research approach: developing
  fundamental techniques driven by practical applications and informed by
  rigorous theory.
* SCOPE
  We invite high-quality submissions on the general topic of
  automated reasoning and its applications, especially but not
  exclusively to the design of automated theorem proving systems, with
  connections to any of Mark Stickel's research areas:
  - Automated theorem proving, including deductive and abductive reasoning
  - Implementation of and practice with automated reasoners
  - Algorithmics for automated reasoners: unification,
    matching, rewriting, indexing
  - Integration of general-purpose reasoning with external procedures
  - Spatial and temporal reasoning
  - Inference control, theory reasoning, semantic guidance for automated reasoners
  - Application of automated reasoners in mathematics,
    logic, program synthesis, natural language, and natural sciences
  - SAT-solving
  - Applications related to formal methods
* PUBLICATION DETAILS
  It is planned that the book will be published as an LNAI Festschrift
  with Springer.
* SUBMISSION INSTRUCTIONS
  While it is expected that most of the papers will be regular
  technical papers, a few papers that combine scientific content
  with recollections of Mark Stickel's work and personality,
  as can be written by those who worked with him, are also sought.
  All papers will be refereed by anonymous peer reviewers, and
  read by the editors, according to the highest standards in terms
  of originality, significance, technical quality, and readability.
  Submissions must be in English and standard conforming pdf
  format. They must be unpublished and not submitted for
  publication elsewhere. However, significantly extended versions
  of papers published at conferences are welcome. Submissions
  of any length will be considered, but final versions may be
  limited by the editors depending on the totality of submissions.
  Authors are strongly encouraged to produce their papers in LaTeX.
  Formatting instructions and the LNCS style files can be obtained
  via http://www.springer.de/comp/lncs/authors.html.
  Electronic submission via EasyChair is open at
  https://www.easychair.org/conferences/?conf=festschriftmarkstick .
  In order to facilitate the planning of the book, authors are
  invited to notify the editors as soon as possible of their
  intention to submit with proposed topic and length. Early
  submission would be especially helpful for completing the
  review process sooner.
* EDITORS
  Peter Baumgartner      NICTA and Australian National University,
                         http://users.cecs.anu.edu.au/~baumgart/
  Richard Waldinger      SRI International,
                         http://www.ai.sri.com/~waldinge/



10TH INTERNATIONAL CONFERENCE ON ADVANCES IN MODAL LOGIC (AiML 2014)
  Call for Papers
  August 5-8, 2014
  Groningen, The Netherlands
  http://www.philos.rug.nl/AiML2014/
* SCOPE
  AiML is an initiative aimed at presenting the state of the art in
  modal logic and its various applications. The initiative consists
  of a conference series together with volumes based on the conferences.
  Information about the AiML series can be obtained at http://www.aiml.net.
  AiML-2014 is the tenth conference in the series.
* TOPICS
  We invite submission on all aspects of modal logic, including:
  history of modal logic; philosophy of modal logic; applications of modal
  logic; computational aspects of modal logic (complexity and decidability of
  modal and temporal logics, modal and temporal logic programming,
  model checking, model generation, theorem proving for modal logics);
  theoretical aspects of modal logic (algebraic/categorical perspectives
  on modal logic, coalgebraic modal logic, completeness and canonicity,
  correspondence and duality theory, many-dimensional modal logics,
  modal fixed point logics, model theory of modal logic, proof theory
  of modal logic); specific instances and variations of modal logic (description
  logics, modal logics over non-boolean bases, dynamic logics and other
  process logics, epistemic and deontic logics, modal logics for agent-based
  systems, modal logic and game theory, modal logic and grammar
  formalisms, provability and interpretability logics, spatial and temporal
  logics, hybrid logic, intuitionistic logic, substructural logics, computationally
  light fragments of all such logics). Papers on related subjects will also be
  considered.
* IMPORTANT DATES
  Abstract of full paper submission due: 14 March 2014
  Full paper submission due: 21 March 2014
  Full paper notification: 2 May 2014
  Short presentation submission due: 12 May 2014
  Short presentation notification: 2 June 2014



PHD AND POSTDOC AT UNIVERSITY OF INNSBRUCK
* Within   the   FWF   project  "Automated   Complexity   Analysis   via
  Transformations (ACAT)"
  - a PhD position (3 years) and
  - a postdoctoral research position (2 years)
  are available. Both positions are potentially extendable.
* The  project  is  hosted  at  the Computational  Logic  group  of  the
  Institute    of   Computer    Science,   University    of   Innsbruck,
  Austria. Candidates for the postdoctoral position are required to hold
  a PhD degree.  A strong background in key areas of the ACAT project is
  an asset: program transformation, program analysis, runtime complexity
  analysis, etc.
  Candidates are expected to contribute  to research within the project.
  Knowledge  of German  is  not required.   We  follow the  renumeration
  scheme of FWF, see http://www.fwf.ac.at/.
  Applications (including CV, publication  list, and two references) may
  be sent by email, to georg.moser@uibk.ac.at
  no later than November 30, 2013. Informal inquiries are also welcome at
  the same email address.
  Further information is available from the following links:
  - Project ACAT:
    http://cl-informatik.uibk.ac.at/research/projects/automated-complexity-analysis-via-transformations/
  - Institute of Computer Science:
    http://informatik.uibk.ac.at/
  - University of Innsbruck:
    http://www.uibk.ac.at/



TWO PHD OR POSTDOC POSITIONS AT UNIVERSITY OF TWENTE
  http://fmt.cs.utwente.nl/vacancies/
* The Formal Methods & Tool Group has at University of Twente
  two PhD or Postdoc positions available in stochastic model checking.
* POSITION 1: smart railroad maintenance via stochastic model checking
  (ArRangeer)
  Goal of the ArRangeer project is to develop smart railroad maintenance
  techniques through stochastic modeling, analysis and optimization. In
  particular, our aim is to extend the widely used fault tree formalism with
  maintenance models. The scientific core is the extension and refinement of
  stochastic model checking and stochastic decisions techniques to
  maintenance planning problems.
  We will extensively cooperate with the RWTH Aachen University, and
  maintenance engineers from ProRail, Movares and NedTrain. Key project
  deliverables are efficient analysis algorithms and a workable tool to be
  used in the ProRail context. For more information on this project, see
  http://fmt.cs.utwente.nl/vacancies/
  or contact m.i.a.stoelinga@utwente.nl or j.p.katoen@utwente.nl
* POSITION 2: Quantitative security analysis via stochastic model checking
  (EU FP7 project TREsPASS)
  Goal of the TREsPASS project is to develop an attack navigator to predict,
  prioritize and prevent information security attacks. We will use a
  model-based and quantitative approach. In particular, we will develop
  methods and techniques to expose which attack opportunities are possible;
  which of them are most urgent; and which countermeasures are most effective.
  Scientific core of our work is the extension, refinement, and tailoring of
  stochastic model checking and stochastic decision-theory techniques to
  quantify risks on attacks, attack scenarios and the effectiveness of
  countermeasures. Key project deliverables are efficient analysis algorithms
  and their implementation in a workable tool. For more information on this
  project, see http://fmt.cs.utwente.nl/vacancies/
  or contact m.i.a.stoelinga@utwente.nl or j.c.vandepol@utwente.nl
  During the whole project, we will extensively cooperate with the TREsPASS
  partners, most notably with Aalborg University Denmark, Technical
  University Denmark, University of Luxemburg, and the industrial partners
  Cybernetica and Consult Hyperion.
* MORE INFORMATION  AND OUR OFFER
  - We are looking for a candidates with a strong background in
  mathematics or theoretical computer science, and the will to apply this
  expertise in practical case studies.
  - The projects are supervised by Dr Marielle Stoelinga (both), Prof.dr.
  Jaco van de Pol (TREsPASS) and Prof.dr.Joost-Pieter Katoen (ArRangeer)
  - PhD student/Postdoc: Full status as an employee at the University of
  Twente, including pension and health care benefits.
  - Gross salary PhD student: ranging from EUR 2083 (1st year) to EUR 2664
  (4th year) per month, plus holiday allowance (8%) and end-of-year bonus
  (8.3%).
  - Gross salary Postdoc: starting from EUR 2919 plus holiday allowance
  (8%) and end-of-year bonus (8.3%)
  We are looking forward to your application (deadline December 1) via the
  following links:
  http://ssl1.peoplexs.com/Peoplexs22/CandidatesPortalNoLogin/Vacancy.cfm?PortalID=2537&VacatureID=613409&BedrijfID=55061100
  for ArRangeer.
  http://ssl1.peoplexs.com/Peoplexs22/CandidatesPortalNoLogin/Vacancy.cfm?portalID=2537&VacatureID=613321&BedrijfID=55061100
  for
  TREsPASS.



TWO SOFTWARE DEVELOPERS AT EMBEDDED SYSTEMS UNIT OF FBK, TRENTO
* Closing date: 17th November 2013
  Two programmer positions are available in the Embedded Systems "ES"
  Research Unit at Bruno Kessler Foundation, Center for Information
  Technology.
* The Embedded System Research Unit (ES Unit) of the Information and
  Communication Technology Center of the Bruno Kessler Foundation,
  Trento, Italy consists of about 25 persons, including researchers,
  post-Doc, PhD students, and programmers. The Unit carries out
  research, tool development and technology transfer in the fields of
  design and verification of embedded systems.
* The ES Unit is looking for two skilled programmers for software
  development activities in research and industrial projects in the
  field of formal verification of Embedded Systems.
  The activities will be carried out within various research and
  industrial projects, including several projects with the European
  Space Agency, the ARTEMIS projects SafeCer (www.safecer.eu) and
  CRYSTAL (www.crystal-artemis.eu), and the FP VII project D-MILS
  (www.d-mils.org).
* Emails should have the following reference code: ES_2013PGM
  Application deadline: November 17, 2013
  For further information, please contact the Human Resources Service at
  jobs@fbk.eu.



TWO RESEARCH POSITIONS AT EMBEDDED SYSTEMS UNIT OF FBK, TRENTO
* Closing date: 17th November 2013
  Two research positions are available in the Embedded System Research
  Unit (ES) at Bruno Kessler Foundation, Center for Information
  Technology.
* The Embedded System Research Unit (ES Unit) of the Information and
  Communication Technology Center of the Bruno Kessler Foundation,
  Trento, Italy consists of about 25 persons, including researchers,
  post-Doc, PhD students, and programmers. The Unit carries out
  research, tool development and technology transfer in the fields of
  design and verification of embedded systems.
* The ES Unit is looking for two candidates to carry out research
  activities in the field of target algorithms, methodologies and tools
  for the design and formal verification of Embedded Systems.
  The activities will be carried out within various research projects,
  including ARTEMIS projects SafeCer (www.safecer.eu) and CRYSTAL
  (www.crystal-artemis.eu), and the FP VII project D-MILS
  (www.d-mils.org).
  The successful candidates will be enrolled with a fixed length
  contract (1 to 2 years), and will be subject to a 6 months trial work
  period.
* Duration: up to 2 years (until the end of December 2015)
  Emails should have the following reference code: ES_2013postdoc
  Application deadline: November 17, 2013
  For further information, please contact the Human Resources Service at
  jobs@fbk.eu.



PHD POSITION ON MODEL-BASED TESTING OF SOFTWARE PRODUCT LINES AT HALMSTAD UNIVERSITY, SWEDEN
* Software Product Lines (SPLs) have become common practice and have been
  proven effective in mass production and customisation of software.
  There have been several attempts to provide a  structured discipline for
  testing SPLs.
  However, fundamental approaches to model-based testing (based on finite
  state machines and labeled transition systems) are not yet fully adapted to
  and adopted in this domain.
  This project aims at closing this gap by providing fundamental theories and
  developing tool support for model-based testing of SPLs.
* The Ph.D. student will be performing research in a very vigorous and
  international research environment at the Center for Research on Embedded
  Systems (CERES) at Halmstad University.
  The research project will be carried out in collaboration with several
  internationally renowned research groups including
  the Verified Systems Group at the University of Bremen and the Dependable
  Systems Group at Saarland University.
  For more information on the Model-Based Testing research at CERES, please
  see:
  http://ceres.hh.se/mediawiki/index.php/Research_in_Model-Based_Testing_and_Verification
  For more information on CERES please see:
  http://ceres.hh.se/
* The position concerns a funded 4-year Ph.D. position (extensible for 1 more
  year). It offers a very competitive salary (ca. 24K SEK/month gross for the
  first year, increasing annually to ca. 30k SEK/month for the last year) and
  attractive employment terms. The application should comprise a single PDF
  file and should be received no later than November 30, 2013.
  Informal enquiries regarding the position, the project and the working
  environment are most welcome and should be addressed to Mohammad Mousavi (
  m.r.mousavi@hh.se).



Back to the LICS web page.