Newsletter 151
October  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
  CSL-LICS'14
* DEADLINES
  Forthcoming Deadlines
* CALLS
  FMCAD 2013 - Call for Participation
  ICFEM 2013 - Call for Participation
  SMC 2014 - Preliminary Announcement
  CIE 2014 - Preliminary Announcement
  LIX Colloquium - Call for Abstracts and Participation
  ETAPS 2014 - Call for Papers
  FASE 2014 - Call for Papers
  FOSSACS 2014 - Call for Papers
  TACAS 2014 - Call for Papers
  IWIL 2013 - Call for Contributions
  ISAIM 2014 - Call for Papers
  FOPARA 2013 - Call for Contributions (post-proceedings)
  FVHMS 2014 - Call for Papers
  RAMiCS 2014 - Call for Papers
  I&C ICC - Call for Papers
  FM 2014 - Call for Papers, Workshops and DOC Symposium
  NASA FM SYMPOSIUM - Call for Papers
  PODS 2014 - Call for Papers
  FESCA 2014 - Call for Papers
  FLOPS 2014 - Call for Papers
  QAPL 2014 - Call for Papers
  CMCS 2014 - Call for Papers
  EAPLS PHD AWARD 2012 - Call for Nominations
* JOB ANNOUNCEMENTS
  Open PhD Fellowship in Component-Based Systems at Verimag in Grenoble
  PhD and PostDoc Positions at ETH Zurich
  Postdoc Position in Operational Semantics in Warsaw
  Formal Methods Positions at NASA


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
* ETAPS 2014
  Submission deadline (abstracts): October 4, 2013
  Submission deadline (full papers): October 11, 2013
  http://www.etaps.org/2014
* FASE 2014
  Submission deadline (abstracts): October 4, 2013
  Submission deadline (full papers): October 11, 2013
  http://www.etaps.org/2014/fase
* FOSSACS 2014
  Submission deadline (abstracts): October 4, 2013
  Submission deadline (full papers): October 11, 2013
  http://www.etaps.org/2014/fossacs
* TACAS 2014
  Submission deadline (abstracts): October 4, 2013
  Submission deadline (full papers): October 11, 2013
  http://www.etaps.org/2014/tacas
* IWIL 2013
  Submission of papers/abstracts: October 14, 2013
  http://www.eprover.org/EVENTS/IWIL-2013.html
* ISAIM 2014
  Paper submission: October 15, 2013
  http://www.cs.uic.edu/Isaim2014/
* FOPARA 2013 (post-proceedings)
  Paper Submission: October 18th, 2013
  http://fopara2013.cs.unibo.it
* FVHMS 2014
  Submission deadline: October 18, 2013
  http://faculty.cs.byu.edu/~mike/mikeg/WORKSHOP/
* RAMiCS 2014
  Title and abstract submission: October 25, 2013
  Submission of full papers: November 1, 2013
  http://mathcs.chapman.edu/ramics2014
* 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/
* PODS 2014
  Abstract submission: November 25, 2013
  Paper submission: December 2, 2013
  http://www.sigmod2014.org/
* 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
* 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/
* EAPLS PhD AWARD 2012
  Nomination deadline: December 31, 2013
  http://eapls.org/pages/phd_award/



INTERNATIONAL CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2013)
  Call for Participation
  October 20-23, 2013
  Portland, Oregon, USA
  http://www.fmcad.org/FMCAD13
* VENUE
  University Place Hotel and Conference Center
  310 SW Lincoln St.
  Portland, Oregon 97201.  USA
* OVERVIEW
  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.
  FMCAD 2013 is co-located with MEMOCODE 2013, the ACM/IEEE
  International Conference on Formal Methods and Models for
  Codesign, and DIFTS 2013, the International Workshop on
  Design and Implementation of Formal Tools and Systems.
  DIFTS will be held on October 19.  MEMOCODE will take place
  from October 18 to 19, followed by a joint FMCAD/MEMOCODE
  tutorial day on October 20.  FMCAD will continue from
  October 21 to 23, 2013.
* REGISTRATION
  Early Registration Deadline: September 30, 2013
  Registration details are available from the conference Web
  page.  See URL
  http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/registration.shtml.
  In addition to traditional full-conference (student and
  regular) registrations with discounts for ACM/IEEE members,
  FMCAD provides discounted registration to participants who
  register for FMCAD and DIFTS together.  FMCAD also provides
  single-day registrations for participants who are already
  registered full-conference for MEMOCODE during the early
  registration period (no late single-day registration
  available).  Furthermore, note that MEMOCODE provides
  single-day registration to MEMOCODE for full-conference
  registrants of FMCAD.
* TECHNICAL PROGRAM
  The technical program is available at the conference Web
  page.  It includes 2 invited keynotes, 4 invited tutorials
  (jointly with MEMOCODE 2013), 23 regular papers, 7 short
  papers, a special session for Student Forum, and a panel.
* KEYNOTES
  - Pranav Ashar, Chief Technology Officer, Real Intent,
  "Static Verification Based Signoff - A Key Enabler for
  Managing Verification Complexity in the Modern SoC"
  - Lori A. Clarke, Professor, University of Massachusetts,
  Amherst, "Using Process Modeling and Analysis Techniques
  to Reduce Errors in Healthcare"
* TUTORIALS
  - Rajeev Alur, University of Pennsylvania:
  "Syntax-Guided Synthesis"
  - Nate Foster, Mark Reitblatt, Cole Schlesinger (Cornell
  University), and Arjun Guha (University of Massachussetts, Amherst):
  "Network Programming in Frenetic"
  - Jim Grundy, Intel Corporation:
  "Firmware Validation: Challenges and Opportunities"
  - Somesh Jha, Bill Harris, Tom Reps, University of Wisconsin-Madison:
  "Secure Programs via Game-Based Synthesis"
* STUDENT FORUM
  FMCAD 2013 will feature a Student Forum that provides a
  platform for graduate students at any career stage to
  introduce their research to the wider Formal Methods
  community, and solicit feedback on it.  The event will
  consist of 14 short presentation by student authors
  (selected from among 29 submissions), together with a poster
  corresponding to each presented topic that will be on
  display throughout the duration of the conference.  All
  FMCAD participants are strongly encouraged to attend the
  student presentations and the subsequent poster session, and
  engage with the presenters throughout the duration of the
  conference.
* VENUE
  The conference will be held at the University Place Hotel
  and Conference Center, Portland, Oregon.  We have negotiated
  a special rate with the hotel for conference attendees,
  under group name "FMCAD".  Please book early to secure the
  reduced rate.  Please submit your individual reservation
  requests directly to the hotel, either by phone at
  +1-866-845-4647, or via an email to Bich-Hahn Le at
  bichhahn@pdx.edu
  The banquet will be held in Portland City Grill.  For
  details, please see the conference web page.
* CO-LOCATED EVENTS
  - MEMOCODE, the ACM/IEEE International Conference on Formal
  Methods and Models for Codesign (MEMOCODE 2013).  See
  http://memocode.irisa.fr/2013/
  - DIFTS, International Workshop on Design and Implementation
  of Formal Tools and Systems (DIFTS 2013).  See
  http://www.cmpe.boun.edu.tr/difts13/
  - HWMCC, Hardware Model Checking Competition (HWMCC'13).
  See http://fmv.jku.at/hwmcc13/
* SPONSORS
  - Sponsored by: FMCAD, Inc.
  - Technical Co-sponsor: IEEE CEDA
  - In-cooperation with: ACM SIGDA
  - Industrial Financial Support:
  Galois, IBM, Intel, Jasper, Mentor Graphics, Microsoft,
  NEC, NVIDIA, Onespin Solutions, Oski Technology, Real
  Intent, Synopsys, Xpliant



15TH INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS (ICFEM 2013)
  Queenstown, New Zealand
  29 October - 1 November 2013
  http://www.cs.auckland.ac.nz/icfem2013/
* GENERAL
  The 15th International Conference on Formal Engineering Methods
  (ICFEM 2013) will be held at the Crowne Plaza Hotel in
  Queenstown, New Zealand from 29 October to 1 November 2013.
  Since 1997, ICFEM has been serving as an international forum for
  researchers and practitioners who have been dedicated to
  applying formal methods to practical computer systems.
  Researchers and practitioners, from industry, academia, and
  government, are encouraged to attend, and to help advance the
  state of the art. We are interested in work that has been
  incorporated into real production systems, and in theoretical
  work that promises to bring practical and tangible benefit.
  ICFEM 2013 is organized and sponsored by The University of
  Auckland and will be held in the world renowned travel
  destination - Queenstown. Around 1.9 million visitors are drawn
  to Queenstown each year to enjoy their own unforgettable travel
  experience. We are looking forward to your submissions and
  participation.
* GENERAL CHAIRS
  Jin Song Dong, National University of Singapore, Singapore.
  Ian Hayes, The University of Queensland, Australia.
  Steve Reeves, The University of Waikato, New Zealand.
* PC CHAIRS
  Lindsay Groves, Victoria University of Wellington, New Zealand.
  Jing Sun, The University of Auckland, New Zealand.
* WORKSHOP AND TUTORIAL CHAIRS
  Yang Liu, Nanyang Technological University, Singapore.
  Jun Sun, Singapore University of Technology and Design, Singapore.
* LOCAL ORGANIZATION CHAIR
  Gillian Dobbie, The University of Auckland, New Zealand.



MATHEMATICAL STRUCTURES OF COMPUTATION (SMC 2014)
  Preliminary announcement
  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.
* Information on the programme can be found at http://smc2014.univ-lyon1.fr
* Registration for the programme is free and will open in early September 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.



COMPUTABILITY IN EUROPE 2014: LANGUAGE, LIFE, LIMITS (CiE 2014)
  Preliminary Announcement
  Budapest, Hungary
  June  23 - 27, 2014
  http://www.illc.uva.nl/CiE/index.php?page=22_8
* SCOPE
  CiE 2014 is the tenth conference organized by CiE (Computability
  in Europe), a European association of mathematicians, logicians,
  computer scientists, philosophers, physicists and others
  interested in new developments in computability and their
  underlying significance for the real world. Previous meetings
  have taken place in Amsterdam (2005), Swansea (2006), Siena
  (2007), Athens (2008), Heidelberg (2009), Ponte Dalgada (2010),
  Sofia (2011), Cambridge (2012), and Milan (2013). Please mark the
  conference dates in your agendas for 2014.
* CONFIRMED TUTORIAL SPEAKER
  Wolfgang Thomas (RWTH Aachen)
* CONFIRMED INVITED SPEAKERS
  Alessandra Carbone (Universite Pierre et Marie Curie and CNRS Paris)
  Maribel Fernandez        (King's College London)
  Przemyslaw Prusinkiewicz (University of Calgary)
  Eva Tardos               (Cornell University)
  Albert Visser            (Utrecht University)
* SPECIAL SESSIONS
  History and Philosophy of Computing
        organizers: Liesbeth de Mol, Giuseppe Primiero
  Computational Linguistics
        organizers: Maria Dolores Jimenez-Lopez, Gabor Proszeky
  Computability Theory
        organizers: Karen Lange, TBA
  Bio-inspired Computation
        organizers: Marian Gheorghe, Florin Manea
  Online Algorithms
        organizers: Joan Boyar, Csanad Imreh
  Complexity in Automata Theory
        organizers: Markus Lohrey, Giovanni Pighizzini
* MOTTO
  The motto of CiE 2014 "Language, Life, Limits" intends to put a
  special focus on relations between computational linguistics,
  natural computing, and more traditional fields of computability
  theory.
  This is to be understood in its broadest sense including
  computational aspects of problems in linguistics, studying models
  of computation and algorithms inspired by physical and biological
  approaches as well as exhibiting limits (and non-limits) of
  computability when considering different models of computation
  arising from such approaches.
  As with previous CiE conferences, the allover glueing perspective
  is to strengthen the mutual benefits of analyzing traditional and
  new computational paradigms in their corresponding frameworks
  both with respect to practical applications and a deeper
  theoretical understanding.
  The conference will address these aspects besides the more
  established lines of research of Computational Complexity and the
  interplay between Proof Theory and Computation.
  Novel views that rely on physical and biological processes and
  models to find new ways of tackling computations and improving
  their efficiency are welcome.  Also, massive data analysis and
  computations are a recent subject of attention, since the most
  recent technologies produce huge amounts of data, and managing
  such data requires some theoretical frameworks.
  In all cases we are looking for fundamental and theoretical
  submissions. In line with other conferences in this series, CiE
  2014 has a broad scope and provides a forum for the discussion of
  theoretical and practical issues in Computability with an
  emphasis on new paradigms of computation and the development of
  their mathematical theory.
  We particularly invite papers that build bridges between
  different parts of the research community.
* CALL
  In a Call for Papers to be sent out in October 2013, the PC will
  invite all researchers in the area of the conference to submit
  their papers for presentation at CiE 2014.  The best of the
  accepted papers will be published in the conference proceedings
  within the Lecture Notes in Computer Science (LNCS) series of
  Springer, which will be available at the conference.



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/



17TH EUROPEAN JOINT CONFERENCES ON THEORY AND PRACTICE OF SOFTWARE (ETAPS 2014)
  Call for Papers
  Grenoble,  France
  5-13 April 2014
  http://www.etaps.org/2014
* ABOUT ETAPS
  ETAPS is the primary European forum for academic and industrial
  researchers working on topics relating to software science. ETAPS,
  established in 1998, is a confederation of six main annual
  conferences, accompanied by satellite workshops. ETAPS 2014 is the
  seventeenth event in the series.
* MAIN CONFERENCES (7-11 April)
  - CC: Compiler Construction
  - ESOP: European Symposium on Programming
  - FASE: Fundamental Approaches to Software Engineering
  - FOSSACS: Foundations of Software Science and Computation Structures
  - POST: Principles of Security and Trust
  - TACAS: Tools and Algorithms for the Construction and Analysis of Systems
  TACAS '14 hosts the 3rd Competition on Software Verification
  (SV-COMP).
* INVITED SPEAKERS
  - Robert Harper (Carnegie Mellon University, US)
  - John Launchbury (Galois, US)
  - Benoit Dupont de Dinechin (Kalray, France)
  - Maurice Herlihy (Brown University, US)
  - Christel Baier (Technical University of Dresden, Germany)
  - Petr Jancar (Technical Univ of Ostrava, Czech Republic)
  - David Mazieres (Stanford University, US)
  - Orna Kupferman (Hebrew University Jerusalem, Israel)
* IMPORTANT DATES
  -  4 October  2013: Submission deadline for abstracts (strict)
  - 11 October  2013: Submission deadline for full papers (strict)
  - 20 December 2013: Notification of acceptance
  - 17 January  2014: Camera-ready versions due
  ESOP and FoSSaCS will use a rebuttal (author response) phase.
* GENERAL SUBMISSION INFORMATION
  ETAPS conferences accept two types of contributions: research papers
  and tool demonstration papers. Both types will appear in the
  proceedings and have presentations during the conference. (TACAS has
  more categories, see below.)
  A condition of submission is that, if the submission is accepted, one
  of the authors attends the conference to give the
  presentation. Submitted papers must be in English presenting original
  research. They must be unpublished and not submitted for publication
  elsewhere. In particular, simultaneous submission of the same
  contribution to multiple ETAPS conferences is forbidden. The
  proceedings will be published in the Advanced Research in Computing
  and Software Science (ARCoSS) subline of Springer's Lecture Notes in
  Computer Science series.
  Papers must follow the formatting guidelines specified by Springer at
  the URL http://www.springer.de/comp/lncs/authors.html
  and be submitted electronically in pdf through the Easychair author
  interface of the respective conference.
  Submissions not adhering to the specified format and length may be
  rejected immediately.
* RESEARCH PAPERS
  Different ETAPS 2014 conferences have different page limits.
  Specifically, FASE, FOSSACS and TACAS have a page limit of 15 pages,
  whereas CC, ESOP and POST allow at most 20 pages. Additional material
  intended for the referees but not for publication in the final version
  - for example, details of proofs - may be placed in a clearly marked
  appendix that is not included in the page limit. ETAPS referees are at
  liberty to ignore appendices and papers must be understandable without
  them. TACAS solicits not only regular research papers, but also case study
  papers.
* TOOL DEMONSTRATION PAPERS
  Submissions should consist of two parts:
  - The first part, at most 4 pages, should describe the tool
  presented. Please include the URL of the tool (if available) and
  provide information that illustrates the maturity and robustness of
  the tool. (This part will be included in the proceedings.)
  - The second part, at most 6 pages, should explain how the
  demonstration will be carried out and what it will show, including
  screen dumps and examples. (This part will be not be included in the
  proceedings, but will be evaluated.)
  ESOP and FOSSACS do not accept tool demonstration papers.
  In addition to tool demonstration papers (max 6 pages in their case),
  TACAS solicits also regular tool papers (max 15 pages) adhering to
  specific instructions about content and organization.
* SATELLITE EVENTS (5-6 April, 12-13 April)
  Around 20 satellite workshops will take place before and after the
  main conferences. In addition, on 6 April, some tutorials on topics of
  wide interest will be offered.
* HOST CITY
  Located in the southeastern part of France, Grenoble is considered as
  the capital of the Alps. Grenoble is surrounded by nature and high
  mountains: down the Alps, Grenoble is the meeting point of two
  important rivers, Drac and Isere. Grenoble has important historical
  and gastronomic heritages. Leisure activities in breathtaking nature
  are easily organizable and within short-distance. Grenoble is also a
  major scientific center in Europe dedicated to high-tech technologies,
  e.g., nano, micro, bio, and information technologies.
* HOST INSTITUTION
  The event is organized by Universite Joseph Fourier. Located at the
  heart of the Alps, in outstanding scientific and natural surroundings,
  the Universite Joseph Fourier in Grenoble is a leading University of
  Science, Technology and Health.
* ORGANIZERS
  - General chair: Saddek Bensalem
  - Conferences chair: Yassine Lakhnech
  - Workshops chair: Axel Legay
  - Publicity chair: Ylies Falcone
  - Finance chair: Nicolas Halbwachs
  - Web site chair: Marius Bozga
* FURTHER INFORMATION
  Please do not hesitate to contact the organizers at
  etaps2014.organization@imag.fr.



17TH INTERNATIONAL CONFERENCE ON FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2014)
  Call for Papers,
  7-11 April 2014, Grenoble, France
  http://www.etaps.org/2014/fase
* IMPORTANT DATES
  - Abstract Submission: 4 October 2013
  - Paper Submission: 11 October 2013
  - Author Notification: 20 December 2013
  - Camera-ready version: 17 January 2014
* DESCRIPTION
  FASE is concerned with the foundations on which software engineering is
  built. Submissions should focus on novel techniques and the way in which
  they contribute to making software engineering a more mature and
  soundly-based discipline. Contributions that combine the development of
  conceptual and methodological advances with their formal foundations and
  tool support are particularly encouraged. We welcome contributions on
  all such fundamental approaches, including:
  - Software engineering as an engineering discipline, including its
    interaction with and impact on society;
  - Requirements engineering: capture, consistency, and change management
    of software requirements;
  - Software architectures: description and analysis of the architecture
    of individual systems or classes of applications;
  - Specification, design, and implementation of particular classes of
    systems: adaptive, collaborative, embedded, distributed, mobile,
    pervasive, or service-oriented applications;
  - Software quality: validation and verification of software using
    theorem proving, model checking testing, analysis, refinement methods,
    metrics or visualisation techniques;
  - Model-driven development and model transformation: meta-modelling,
    design and semantics of domain-specific languages, consistency and
    transformation of models, generative architectures;
  - Software processes: support for iterative, agile, and open source
    development;
  - Software evolution: refactoring, reverse and re-engineering,
    configuration management and architectural change, or aspect-orientation.
* SUBMISSION
  FASE accept two types of contributions: research papers and tool
  demonstration papers. Both types will appear in the proceedings and have
  presentations during the conference. Submit your paper via
  https://www.easychair.org/conferences/?conf=fase2014. A condition of
  submission is that, if the submission is accepted, one of the authors
  attends the conference to give the presentation. Submitted papers must
  be in English presenting original research. They must be unpublished and
  not submitted for publication elsewhere. In particular, simultaneous
  submission of the same contribution to multiple ETAPS conferences is
  forbidden. The proceedings will be published in the Advanced Research in
  Computing and Software Science (ARCoSS) subline Springer's Lecture Notes
  in Computer Science series.
  Research papers have a page limit of 15 pages. Additional material
  intended for reviewers but not for publication in the final version -
  for example, details of proofs - may be placed in a clearly marked
  appendix that is not included in the page limit. Reviewers are at
  liberty to ignore appendices and papers must be understandable without them.
  Tool demonstration papers should consist of two parts. The first part,
  at most 4 pages, should describe the tool presented. Please include the
  URL of the tool (if available) and provide information that illustrates
  the maturity and robustness of the tool (this part will be included in
  the proceedings). The second part, at most 6 pages, should explain how
  the demonstration will be carried out and what it will show, including
  screen dumps and examples. (This part will be not be included in the
  proceedings, but will be evaluated.)
* INVITED SPEAKER
  Christel Baier (Technical University of Dresden, Germany)
* PROGRAMME CHAIRS
  - Stefania Gnesi (ISTI-CNR, Italy)
  - Arend Rensink (University of Twente, the Netherlands)



17TH INTERNATIONAL CONFERENCE ON FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2014)
  Call for Papers
  An ETAPS Member Conference
  Grenoble, France
  5-13 April 2014
  http://www.etaps.org/2014/fossacs
  FoSSaCS is one of the main conferences of ETAPS (European Joint Conferences
  on Theory And Practice of Software).
* SCOPE
  FoSSaCS seeks original papers on foundational research with a clear
  significance for software science. The conference invites submissions on
  theories and methods to support the analysis, integration, synthesis,
  transformation, and verification of programs and software systems.
  The specific topics covered by the conference include, but are not
  limited to, the following:
  - Categorical models and logics;
  - Language theory, automata, and games;
  - Modal, spatial, and temporal logics;
  - Type theory and proof theory;
  - Concurrency theory and process calculi;
  - Rewriting theory;
  - Semantics of programming languages;
  - Program analysis, correctness, transformation, and verification;
  - Logics of programming;
  - Software specification and refinement;
  - Models of concurrent, reactive, stochastic, distributed, hybrid,
    and mobile systems;
  - Emerging models of computation;
  - Logical aspects of computational complexity;
  - Models of software security;
  - Logical foundations of data bases.
* INVITED SPEAKER --
  Petr Jančar (Technical Univ of Ostrava, Czech Republic)
* IMPORTANT DATES
  - 4 October 2013: Submission deadline for abstracts (strict)
  - 11 October 2013: Submission deadline for full papers (strict)
  - 26-28 November 2013: Author response (rebuttal)
  - 20 December 2013: Notification of acceptance
  - 17 January 2014: Camera-ready versions due
* SUBMISSION INFORMATION --
  Submitted papers must be in English presenting original
  research. They must be unpublished and not submitted for publication
  to other conferences with published proceedings or to journals.
  In particular, simultaneous submission of the same
  contribution to other ETAPS conferences is forbidden. Submission by
  PC members is not possible. Submitted papers must respect a page limit
  of 15 pages. Additional material intended for the referees but not for
  publication in the final version - for example, details of proofs - may
  be placed in a clearly marked appendix that is not included in the page
  limit. Referees may ignore appendices and submitted papers must be
  understandable without them.
  If the submission is accepted, one of the authors must attend the
  conference to give the presentation.
  The proceedings will be published in the Advanced Research in Computing
  and Software Science (ARCoSS) subline Springer's Lecture Notes in
  Computer Science series.
  Papers must follow the formatting guidelines specified by Springer at
  the URL http://www.springer.de/comp/lncs/authors.html
  and be submitted electronically in pdf through the Easychair author
  interface (the submission site opens on September 15th):
  https://www.easychair.org/account/signin.cgi?conf=fossacs14
  Submissions not adhering to the specified format and length may be
  rejected immediately.
* CONTACT INFORMATION
  Anca Muscholl (chair), anca@labri.fr



20TH INTERNATIONAL CONFERENCE ON TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2014)
  Call for Papers
  An ETAPS Member Conference
  Grenoble, France
  5-13 April 2014
  http://www.etaps.org/2014/tacas
* SCOPE
  TACAS is a forum for researchers, developers and users interested in
  rigorously based tools and algorithms for the construction and
  analysis of systems. The conference serves to bridge the gaps between
  different communities with this common interest and to support them
  in their quest to improve the utility, reliability, flexibility and
  efficiency of tools and algorithms for building systems.
* TOPICS
  Theoretical papers with clear relevance for tool construction and
  analysis, as well as tool descriptions and case studies with a
  conceptual message, are all encouraged. The topics covered by the
  conference include, but are not limited to:
  - Specification and verification techniques
  - Software and hardware verification
  - Analytical techniques for real-time, hybrid, or stochastic systems
  - Analytical techniques for safety, security, or dependability
  - Model checking
  - Theorem proving
  - SAT and SMT solvers
  - Static and dynamic program analysis
  - Testing
  - Abstraction techniques for modeling and verification
  - Compositional and refinement-based methodologies
  - System construction and transformation techniques
  - Tool environments and tool architectures
  - Applications and case studies
* PAPER CATEGORIES
  TACAS accepts four types of submissions: research papers, case study
  papers, regular tool papers, and tool demonstration papers.
  - Research papers clearly identify and justify a principled advance
  to the theoretical foundations for the construction and analysis of
  systems and, where applicable, are supported by experimental
  validation. Research papers can have a maximum of 15 pages.
  - Case study papers report on case studies (preferably in a "real
  life" setting). They should provide information about the following
  aspects: the system being studied and why it is of interest, the
  goals of the study, the challenges the system poses to automated
  analysis, research methodologies and the approach used, the degree to
  which goals were attained, and how the results can be generalized to
  other problems and domains. Case study papers can have a maximum of
  15 pages.
  - Regular 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,
  and emphasize the design and implementation concerns including
  software architecture and core data structures. A regular tool paper
  should give a clear account of the tool's functionality, discuss the
  tool's practical capabilities with reference to the type and size of
  problems it can handle, experience with realistic case studies, and
  where applicable, provide a rigorous experimental evaluation. Papers
  that present extensions to existing tools should clearly focus on the
  improvements or extensions with respect to previously published
  versions of the tool, preferably substantiated by data on
  enhancements in terms of resources and capabilities. We strongly
  suggest authors make their tools available via the web, even if only
  for the evaluation process. Tool papers can have a maximum of 15
  pages.
  - Tool demonstration papers focus on the usage aspects of tools. The
  described tools must be publicly available. Theoretical foundations
  and experimental evaluation are not required, however, a motivation
  as to why the tool is interesting and significant should be provided.
  Tool demonstration papers can have a maximum of 6 pages. They should
  have an appendix of up to 6 additional pages with details on the
  actual demonstration.
  The proceedings will be published in the Advanced Research in
  Computing and Software Science (ARCoSS) subline of Springer's Lecture
  Notes in Computer Science series. Papers of all four types will
  appear in the proceedings and have presentations during the
  conference.
* SUBMISSION
  A condition of submission is that, if the submission is accepted, one
  of the authors attends the conference to give the presentation.
  Submitted papers must be in English presenting unpublished research
  not submitted for publication elsewhere. In particular, simultaneous
  submission of the same contribution to multiple ETAPS conferences is
  forbidden. Papers must follow the formatting guidelines specified by
  Springer at the URL: http://www.springer.de/comp/lncs/authors.html
  and be submitted electronically in pdf through Easychair:
  https://www.easychair.org/account/signin.cgi?conf=tacas2014.
  Submissions not adhering to the specified format and length may be
  rejected immediately.
* IMPORTANT DATES
  Abstract Submission: 4 October 2013
  Paper Submission: 11 October 2013
  Author Notification: 20 December 2013
* COMPETITION ON SOFTWARE VERIFICATION
  TACAS 2014 hosts the third competition on software verification with
  the goal to evaluate technology transfer and compare state-of-the-art
  software verifiers with respect to effectiveness and efficiency. More
  information can be found on the competition website:
  http://sv-comp.sosy-lab.org/2014.
* INVITED SPEAKER
  Orna Kupferman (Hebrew University Jerusalem, Israel)
* PROGRAMME CHAIRS
  Erika Abraham (RWTH Aachen University, Germany)
  Klaus Havelund (NASA JPL, USA)
* TOOL CHAIR
  Nikolaj Bjørner (Microsoft Research, USA)



10TH INTERNATIONAL WORKSHOP ON THE IMPLEMENTATION OF LOGICS (IWIL 2013)
  Call for Contributions
  December 14th, 2013
  Stellenbosch, South Africa
  http://www.eprover.org/EVENTS/IWIL-2013.html
* The 10th International Workshop on the Implementation of Logics will
  be held on December 14th, 2013, colocated with the 19th International
  Conference on Logic for Programming, Artificial Intelligence, and
  Reasoning in Stellenbosch, South Africa.
  We are looking for contributions describing implementation techniques
  for and implementations of automated reasoning programs, theorem
  provers for various logics, logic programming systems, and related
  technologies. Topics of interest include, but are not limited to:
  + Propositional logic and decision procedures, including SMT
  + First-order and higher order logics
  + Non-classical logics, including modal, temporal, description, and
    non-monotonic logics
  + Formal foundations for efficient implementation of logics
  + Data structures and algorithms for the efficient representation and
    processing of logical concepts
  + Proof/model search organization and heuristics for logical reasoning
    systems
  + Data analysis and machine learning approaches to search control
  + Techniques for proof/model search visualization and analysis
  + Practical constraint handling
  + Reasoning with ontologies and other large theories
  + Implementation of efficient theorem provers and model finders for
    different logics
  + System descriptions of logical reasoning systems
  + Issues of reliability, witness generation, and  witness verification
  + Evaluation and benchmarking of provers and other logic-based systems
  + I/O standards and communication between reasoning systems
  We are particularly interested in contributions that help the
  community to understand how to build useful and powerful reasoning
  systems, and how to apply them in practice.
* CONTRIBUTIONS
  Researchers interested in participating are invited to submit a
  position statement (2 pages), a short paper (up to 5 pages), or a full
  papers (up to 15 pages). Submissions should be made via EasyChair at
  http://www.easychair.org/conferences/?conf=iwil2012
  Submissions will be refereed by the program committee, which will
  select a balanced program of high-quality contributions.
  Submissions should be in standard-conforming PDF. Final versions will
  be required to be submitted in LaTeX using the easychair.cls class
  file. Proceedings will be published as EasyChair Proceedings.
  If number and quality of the submissions warrant it, we plan to
  produce a special issue of a recognized journal on the topic of the
  workshop.
* IMPORTANT DATES
  Submission of papers/abstracts:  October 14th, 2013
  Notification of acceptance:      November 11th, 2013
  Camera ready versions due:       December 2nd, 2013
  Workshop:                        December 14th, 2013
* CHAIRS
  Stephan Schulz (Co-Chair)   TU Muenchen
  Geoff Sutcliffe (Co-Chair)  University of Miami
  Boris Konev (Co-Chair)      University of Liverpool



13TH INTERNATIONAL SYMPOSIUM ON ARTIFICIAL INTELLIGENCE AND MATHEMATICS (ISAIM 2014)
  Call for Papers
  January 6-8, 2014, Fort Lauderdale FL, USA
  http://www.cs.uic.edu/Isaim2014/
* The International Symposium on Artificial Intelligence and Mathematics (ISAIM)
  is a biennial meeting that fosters interactions between mathematics,
  theoretical computer science, and artificial intelligence.  This is the
  thirteenth Symposium in the series, which is sponsored by Annals of Mathematics
  and Artificial Intelligence.  We seek submissions of recent results with
  particular emphasis on the foundations of AI and mathematical methods used in
  AI.  Papers describing applications are also encouraged, but the focus should
  be on principled lessons learned from the development of the application.
  Traditionally, the Symposium attracts participants from a variety of
  disciplines, thereby providing a unique forum for scientific exchange. The
  three-day Symposium includes invited speakers, presentations of technical
  papers, and special topic sessions.
* Special Topic Invited Sessions:
   - Boolean and pseudo-Boolean Functions, organized by Endre Boros, Rutgers
       University, and Yves Crama, University of Liège
   - Mathematical Theories of Natural Language Processing, organized by
       András Kornai, Hungarian Academy of Sciences
   - Theory of Machine Learning, organized by Lev Reyzin, University of
       Illinois at Chicago
   - Proposals for organizing additional special sessions can be sent to the
       chairs for consideration by September 15, 2013
* Important Dates:
   - Paper submission:  October 15, 2013
   - Notification:      November 15, 2013
   - Final version due: December 15, 2013
   - Workshop:          January 6-8, 2014, Ft. Lauderdale, Florida
* Send inquiries and requests to isaim2014 at cs DOT uic DOT edu.
* Visit  http://www.cs.uic.edu/Isaim2014/.
* Join isaim@googlegroups.com to receive announcements related to ISAIM.



3RD INTERNATIONAL WORKSHIP ON FOUNDATIONAL AND PRACTICAL ASPECTS OF RESOURCE ANALYSIS (FOPARA 2013)
  Call for Contributions to LNCS Post-Proceedings
  http://fopara2013.cs.unibo.it/
* SCOPE
  FOPARA serves 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 took place in Bertinoro, at the end of August. Not only the
  authors of papers presented at the workshop, but all interested researchers,
  are invited to submit a paper. These 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. To submit a paper,
  please follow the link below:
  https://www.easychair.org/conferences/?conf=foparapostproceeding
* IMPORTANT DATES
  The following deadlines are strict
  - Paper Submission: October 18th, 2013;
  - Notification: December 31st, 2013;
  - Camera Ready: January 23rd, 2013.



FORMAL VERIFICATION AND MODELING IN HUMAN-MACHINE SYSTEMS (AAAI 2014 SPRING SYMPOSIUM, FVHMS 2014)
  Call for Papers
  March 24-26, 2014
  Palo Alto, USA
  http://faculty.cs.byu.edu/~mike/mikeg/WORKSHOP/
* OVERVIEW
  The goal of the workshop is to bring together the fields of
  formal verification, cognitive modeling, and task analysis to study
  the design and verification of real human-machine systems. Recent
  papers in each of these communities discuss modeling challenges and
  the application of basic formal verification in human-machine
  interaction; however, there is little communication between
  researchers in these different areas and there are many open questions
  that require cross-disciplinary collaboration. The workshop is to
  bring together experts from many communities in an environment where
  it is possible to explore key research areas, common solutions,
  near-term research problems, and advantages in combining the best of
  the different communities.
* SUBMISSIONS
  We solicit papers describing original work either
  in-progress or finished, position papers or extended abstracts
  describing research or positions. Papers should follow the AAAI
  formatting, with a page-limit of 6 pages. Proceedings of the symposium
  will be published by AAAI as a CD, distributed at the
  symposium. Selected papers will be invited to submit extended versions
  of their contributions for review in a follow-on special issue of the
  IEEE Transactions on Human-Machine Systems dedicated to the same
  topic.
* TOPICS
  - What model classes, methodologies, and constructs are appropriate
  for modeling human and machine activities in a way that is amenable
  to formal verification? Examples include
           - Programming languages
           - State Machines
           - Activity models (e.g. Brahms)
           - Cognitive models (SOAR, ACT-R, DIARC, etc.)
           - Task analyses-based models (GDTA, CWA, etc.)
           - Probabilistic models
           - Behavioral game theory
  - What levels of abstraction are appropriate for such modeling, and
  what information is lost in using abstraction?
  - What are the contexts, if any, for which the trade offs between
  authority between humans, autonomy, and model-based reasoning can be
  specified?
  - What is the impact on design for including explicit (meta-)
  reasoning models in the human-machine interaction loop?
  - What types of model-checkers are appropriate, and what other lessons
  from formal verification apply to human-machine systems?
  - What are the ethical considerations of using verified models to
  allocate responsibility and authority between humans and machines?
  - What organizational structures are appropriate for human-machine
  collaborative work?
         + Master-slave
         + Teammates
         + Principal-agent
  - How can dynamic models evolve in the presence of learning agents,
  both human and machine, and in the presence of inaccurate mental
  models.
* IMPORTANT DATES
  Oct 18, 2013: Submission deadline
  Dec 10, 2013: Notification of acceptance/rejection
  Jan 10, 2014: Camera-ready papers due
  Mar 1, 2014: Registration deadline
  March 24-26, 2014: Symposium
* ORGANIZERS
  Michael Goodrich, Brigham Young University, USA
  Eric Mercer, Brigham Young University, USA
  Neha Rungta, NASA Ames Research Center, USA
  Ellen Bass, Drexel University, USA
* INVITED SPEAKERS
  Amy Pritchett, Georgia Tech, USA
  Philippe Palanque, IRIT, University Paul Sabatier, France
  Christian Lebiere, CMU, USA



14TH INTERNATIONAL CONFERENCE ON RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMiCS 2014)
  Call for Papers
  27 April - 1 May 2014
  Marienstatt im Westerwald, Germany
  http://mathcs.chapman.edu/ramics2014
* SCOPE
  We invite submissions in the general area of Relational and Algebraic Methods
  in Computer Science. Special focus will lie on formal methods for software
  engineering, logics of programs and links with neighbouring disciplines.
* HISTORY
  Since 1994, the RelMiCS meetings on Relational Methods in Computer Science
  have been a main forum for researchers who use the calculus of relations
  and similar algebraic formalisms as methodological and conceptual tools.
  The AKA workshop series on Applications of Kleene algebra started with a
  Dagstuhl seminar in 2001 and was co-organised with the RelMiCS conference
  until 2009. Since 2011, joint RAMiCS conferences continue to encompass
  the scope of both RelMiCS and AKA.
* STUDENT PROGRAM
  The conference will be accompanied by a PhD training program. Details will
  be published in due time in a special call and on the conference website.
* PROCEEDINGS AND SUBMISSION
  All papers will be formally reviewed. We plan to publish the
  proceedings in the series Lecture Notes in Computer Science ready at
  the conference. Submissions must be in English, in Postscript or PDF
  format, and provide sufficient information to judge their merits.
  They must be unpublished and not submitted for publication elsewhere.
  Submission is via EasyChair at the following address:
  https://www.easychair.org/conferences/?conf=ramics2014
* IMPORTANT DATES
  Title and abstract submission:       October 25, 2013
  Submission of full papers:           November 1, 2013
  Notification:                        December 13, 2014
  Final versions due (firm deadline):  January 17, 2014
  Conference                           April 27 - May 1, 2014



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)



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



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



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.



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



PHD FELLOWSHIP IN COMPONENT-BASED SYSTEMS AT VERIMAG, GRENOBLE, FRANCE
* Grenoble University and Verimag recruits motivated candidates for
  a Ph.D. fellowship. The position is for 3 year starting in September
  or October 2013. The (net) salary is approximately 1600 Euros per month,
  medical insurance included.
* CONTEXT
  The purpose of the Ph.D. is to develop new monitoring techniques for
  component-based systems in the context of the European CERTAINTY project.
  A component-based approach consists in building complex systems by clustering
  components (building blocks). This confers numerous advantages (e.g.,
  productivity, incremental construction, compositionality) that allow to
  deal with complexity in the construction phase. Component-based systems
  (CBS) are desirable because they allow reuse of sub-systems as well as
  their incremental modification without requiring global changes. Their
  development requires methods and tools supporting a concept of
  architecture which characterizes the coordination between components.
  Runtime-verification (RV) is an effective technique to ensure, at runtime,
  that a system meets a desirable behavior. It can be used in numerous
  application domains, and more particularly when integrating together
  unreliable software components. In RV, a run of the system under scrutiny
  is analyzed incrementally using a decision procedure: a monitor. This
  monitor may be generated from a user-provided high level specification
  (e.g., a temporal formula, an automaton). This monitor aims to detect
  violation or satisfaction w.r.t. the given specification. The main challenge
  in augmenting a system with runtime verification is dealing with its runtime
  overhead.
  Monitoring component-based systems is quite different from monitoring
  traditional monolithic systems. The challenges of the thesis are to propose
  methods and tools to:
  - minimize the monitoring overhead in component-based systems;
  - tackle the possible distribution of components,
  - study and assess the modularity of monitors for component-based systems.
* RESEARCH ENVIRONMENT
  The selected application will conduct his research at Verimag. Research
  at Verimag provides theoretical and technical means for developing embedded
  systems, contributing to scientific advancement and industrial progress.
  Over the last fifteen years, Verimag has actively contributed to the
  development of the state-of-the-art, in particular for synchronous languages,
  verification, testing and modeling. The tools produced at Verimag are
  regularly transferred to commercial CASE tools and are used in a number
  of industrial applications.
  Located in the southeastern part of France, Grenoble is considered as the
  capital of the Alps. Grenoble is surrounded by nature and high mountains:
  down the Alps, Grenoble has important historical and gastronomic heritages.
  Leisure activities in breathtaking nature are easily organizable and within
  short-distance. Grenoble is also a major scientific center in Europe
  dedicated to high-tech technologies, e.g., nano, micro, bio, and
  information technologies.
* APPLICATION
  The successful candidate should have a background in at least one of the
  following topics:
  - formal methods and software engineering
  - component-based systems
  - testing and runtime verification
  Applications should include:
  - a detailled resume,
  - Master grades, ranking, MSc document,
  - a motivation letter from the candidate,
  - recommendation letters.
  and should be sent as a single PDF file to Saddek.Bensalem@imag.fr and
  Ylies.Falcone@imag.fr.



PHD AND POSTDOC POSITIONS AT ETH ZURICH
* The Chair of Programming Methodology (http://www.pm.inf.ethz.ch)
  and the Software Reliability Lab (http://www.srl.inf.ethz.ch)
  at ETH Zurich are recruiting students to pursue a PhD in one or more of the
  following areas:
  -         Program analysis
  -         Program verification
  -         Program synthesis
  -         Concurrency
  Key requirements for successful applications:
  -         Strong commitment to research
  -         Interest in combining theory and practice
  -         Proficiency in English and excellent communication skills, both
            oral and written
  -         Excellent M.Sc. degree in Computer Science or in a related subject
            with a strong Computer Science component.
  Applications and questions should be sent to Mrs. Marlies Weissert at
  jobs-pm@inf.ethz.ch. The application should
  include a CV and a description of research interests. We will consider
  applications until the Positions are filled. The start date is negotiable.
* More details about the positions:
  - A PhD position is fully funded and has an attractive salary and social
    benefits.
  - Full scholarships are available for outstanding B.Sc. students interested
    in the PhD.
  - A position is for a maximum of 6 years.
  - ETH has one of the top computer science departments in the world: CS
    University Rankings<http://www.topuniversities.com/university-rankings/faculty-rankings/engineering-and-technology/2013>
  - Zurich is consistently ranked among the top destinations in the world for
    quality of life
  - General information on doctoral studies at ETH is available at
    http://www.ethz.ch/doctorate/index_EN and
    http://www.inf.ethz.ch/education/ds
  Post-doc positions are also available for candidates with a PhD degree and
  a strong publication record.



POSTDOC POSITION IN OPERATIONAL SEMANTICS IN WARSAW
*  A three-year postdoctoral position is available under the direction
   of Bartek Klin in the Institute of Informatics, University of Warsaw.
  The position is in the field of semantics of programming languages
  and process algebras, within the project
  "Modular operational semantics: a bialgebraic approach",
  funded by the Polish National Science Center. The applicants should have
  (or be close to completion of) a PhD degree in Mathematics or Computer
  Science, and be interested in topics such as semantics of programming
  languages, process algebra, formal methods, and/or category theory.
  The position is available from November 2013, but the starting date may
  be postponed on request of a suitable candidate.
  In addition, interested candidates are invited to apply for a postdoctoral
  fellowship at the Warsaw Center of Mathematics and Computer Science
  (http://www.wcmcs.edu.pl/node/41), with the rather short deadline of
  OCTOBER 15TH, 2013.
  These are one-year positions (with a possible extension to two years),
  with an excellent salary which may be used as an additional source of
  funding for the first years of stay in Warsaw.
  For further information please contact Bartek Klin (klin@mimuw.edu.pl).



FORMAL METHODS POSITIONS AT NASA
* The Formal Methods team at NASA Langley Research Center, Hampton,
  Virginia, U.S., has opened the following positions (U.S. citizenship is
  required to apply).
* ANNOUNCEMENT NO:  LA13D0064
  POSITION:  Research Computer Scientist, AST, Computer Research and
  Development, GS-1550-12/13, Promotion Potential GS-13
  LOCATION:  Org D320, Safety-Critical Avionics Systems Branch
  OPENING DATE: September 18, 2013
  CLOSING DATE: October 09, 2013
  AREA OF CONSIDERATION:  This announcement is open to all qualified U.S.
  citizens.
  This position is located in the Safety-Critical Avionics Systems
  Branch within the Research Directorate. This position involves
  conducting research to develop formal verification methods for the
  analysis, design, and implementation of advanced future aircraft and
  spacecraft safety-critical systems.
  Additional details are available at the following websites prior to the
  closing date:
  http://www.usajobs.gov/GetJob/ViewDetails/351820600
* ANNOUNCEMENT NO:  LA13P0045
  POSITION: NASA's Pathways Program Recent Graduate, Research Computer
  Scientist, GS-1550-12 Promotion Potential GS-13
  LOCATION: D320, Safety-Critical Avionics Systems Branch
  OPENING DATE: September 18, 2013
  CLOSING DATE: October 09, 2013
  AREA OF CONSIDERATION: Current students from education institutions
  interested in paid opportunities with Federal agencies or recent
  Graduates from qualifying institutions within two years of degree or
  certification (Veterans precluded by their military service obligation,
  will have up to six years to apply) or Presidential Management
  Fellowships for individuals who have received a qualifying advanced
  degree within the preceding two years.
  This position is located in the Safety-Critical Avionics Systems
  Branch within the Research Directorate. This position involves
  conducting research to develop formal verification methods for the
  analysis, design, and implementation of advanced future aircraft and
  spacecraft safety-critical systems.
  Additional details are available at the following websites prior to
  theclosing date:
  http://www.usajobs.gov/GetJob/ViewDetails/351743700
* For more information on NASA's application process, go to
  http://nasajobs.nasa.gov




Back to the LICS web page.