Newsletter 150
September 7, 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
Kiel Declarative Programming Days 2013 - Call for Participation
AVOCS 2013 - Call for Participation
FroCoS 2013 - Last Call for Participation
FMICS 2013 - Call for Participation
FMCAD 2013 - Call for Participation
ICFEM 2013 - Call for Participation
SMC 2014 - Preliminary Announcement
CIE 2014 - Preliminary Announcement
STACS 2014 - Call for Papers
FLOC 2014 - Call for Workshops
LIX Colloquium - Call for Abstracts and Participation
ETAPS 2014 - Call for Papers
IWIL 2013 - Call for Contributions
ISAIM 2014 - Call for Papers
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
FLOPS 2014 - Call for Papers
QAPL 2014 - Call for Papers
EAPLS PHD AWARD 2012 - Call for Nominations
* JOB ANNOUNCEMENTS
Assistant Professor (UD) Position in Logic at ILLC, Amsterdam
Assistant/Associate Professors at DTU
Postdoctoral Scholar Positions in Secure and Dependable Systems at Idaho
Postdoc in SMT Techniques at Trento
11 PhD Scholarships in Computer Science at Verona
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.
A preliminary Call for Papers is available on the LICS website.
http://lics.siglog.org/csl-lics14/
DEADLINES
* STACS 2014
Paper submission: September 20, 2013
http://stacs2014.sciencesconf.org/
* FLOC 2014
Workshop proposal submission: September 30, 2013
http://vsl2014.at/floc-ws/
* LIX Colloquium
Abstract submission deadline: October 1, 2013
http://www.lix.polytechnique.fr/colloquium2013/
* ETAPS 2014
Submission deadline (abstracts): October 4, 2013
Submission deadline (full papers): October 11, 2013
http://www.etaps.org/2014
* 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/
* 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/
* 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
* EAPLS PhD AWARD 2012
Nomination deadline: December 31, 2013
http://eapls.org/pages/phd_award/
KIEL DECLARATIVE PROGRAMMING DAYS 2013
Call for Participation
September 11-13, 2013
Kiel, Germany
http://www-ps.informatik.uni-kiel.de/kdpd2013/
* EVENT
The Kiel Declarative Programming Days 2013 unifies the following events:
- 20th International Conference on Applications of Declarative Programming
and Knowledge Management (INAP 2013, http://www.dcc.fc.up.pt/INAP-2013/)
- 22nd International Workshop on Functional and (Constraint) Logic
Programming (WFLP 2013, http://www-ps.informatik.uni-kiel.de/wflp2013/)
-27th Workshop on Logic Programming
(WLP 2013, http://www-ps.informatik.uni-kiel.de/wflp2013/)
All events will be jointly organized. Look at the web sites
about detailed registration, accommodation, and travel information.
13TH AUTOMATED VERIFICATION OF CRITICAL SYSTEMS WORKSHOP (AVOCS 13)
11-13th September, 2013
University of Surrey, UK
http://www.avocs2013.org.uk
* REGISTRATION
Registration via the conference website: Regular £220, PhD £170
* INVITED SPEAKERS
- Marcio Roveri, Senior Researcher Fondazione Bruno Kessler, Italy. His
talk will be on software model checking with explicit scheduler and
symbolic threads. The talk will refer to the software model checker Kratos
and its use in the railway domain.
- Alessio Lomuscio, Professor in logic for multi-agent systems in the
Department of Computing, Imperial College London. His talk will be on
verification of multi-agent systems via model checking.
- Sofia Guerra, Adelard. Partner in Adelard and responsible for Adelard¹s
Quality Assurance System. Her industrial talk will be on software
assessment of smart sensors.
* PRESENTATIONS
We have 14 regular papers and 2 short papers. Details of the programme are
on the website.
* OBJECTIVES OF WORKSHOP
The aim of Automated Verification of Critical Systems (AVoCS) 2013 is to
contribute to the interaction and exchange of ideas among members of the
international research community on tools and techniques for the
verification of critical systems. The subject is to be interpreted broadly
and inclusively. It covers all aspects of automated verification,
including model checking, theorem proving, SAT/SMT constraint solving,
abstract interpretation, and refinement pertaining to various types of
critical systems which need to meet stringent dependability requirements
(safety-critical, business-critical, performance-critical, etc.). The
workshop will be relatively informal, with an emphasis on discussion.
* PC CHAIRS
Steve Schneider (University of Surrey, UK, Co-Chair)
Helen Treharne (University of Surrey, UK, Co-Chair)
9TH INTERNATIONAL SYMPOSIUM ON FRONTIERS OF COMBINING SYSTEMS (FROCOS 2013)
Last Call for Participation
Nancy, France
September 18-20, 2013
http://frocos2013.loria.fr/
Co-located with TABLEAUX 2013
* ONLINE REGISTRATION
Visit http://frocos2013.loria.fr/registration.html
Please note the reduced fees for the joint registration FroCoS+TABLEAUX.
Please refer to the conference website for registration, accommodation
and travel information.
* GENERAL INFORMATION
The 9th International Symposium on Frontiers of Combining
Systems will be held in Nancy, France, from 18-20 September
2013. The aim of the conference is to publish and promote
progress in research areas requiring the development of general
techniques and methods for the combination and integration of
special, formally defined systems, as well as for the analysis
and modularization of complex systems.
* PROGRAMME
The conferences features 4 invited talks and 20 contributed
papers. The full programme is available at the conference website.
* INVITED TALKS
- Stephane Demri, New York University & LSV, CNRS
Counter Systems: The Quest for Pushing the Decidability
Borders (joint invited talk with TABLEAUX 2013)
- Konstantin Korovin, The University of Manchester
From Resolution and DPLL to Solving Arithmetic Constraints
- Joel Ouaknine, University of Oxford
Specification and Verification of Linear Dynamical Systems:
Advances and Challenges
- Lawrence C. Paulson, University of Cambridge
MetiTarski's Menagerie of Cooperating Systems
* CO-LOCATED EVENT
FroCoS 2013 will be co-located with the 22nd International
Conference on Automated Reasoning with Analytic Tableaux and
Related Methods (TABLEAUX 2013) held 16-19 September 2013.
Participation in the TABLEAUX sessions is open to FroCoS
participants on the overlapping days. There is also an
attractive option for joint registration to both FroCoS
and TABLEAUX.
* IMPORTANT DATES
16-19 Sep 2013 Tableaux Conference
18-20 Sep 2013 FroCoS Conference
* ORGANIZATION
- Pascal Fontaine (PC Co-Chair),
LORIA, INRIA, University of Lorraine, France
- Christophe Ringeissen (Conference Chair),
LORIA, INRIA, France
- Renate Schmidt (PC Co-Chair),
The University of Manchester, UK
18TH INTERNATIONAL WORKSHOP ON FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2013)
Call for Participation
September 23-24, 2013
Madrid (Spain)
Co-located with SEFM 2013
http://lvl.info.ucl.ac.be/Fmics2013
* INVITED TALKS
- Alessandro Fantechi (Universit à degli Studi di Firenze):
Twenty-Five Years of Formal Methods and Railways: What Next?
- Benjamin Monate (TrustInSoft):
TrustInSoft: Industrial Formal Methods to Protect Security-Sensitive
Systems
* SCOPE
The aim of the FMICS workshop series is to provide a forum for
researchers who are interested in the development and application of
formal methods in industry. In particular, FMICS brings together
scientists and engineers who are active in the area of formal methods
and interested in exchanging their experiences in the industrial usage
of these methods. The FMICS workshop series also strives to promote
research and development for the improvement of formal methods and
tools for industrial applications.
* REGISTRATION
Registration proceeds via the SEFM conference
http://madrid.nethotels.com/mice/english/sefm_2013
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.
31ST INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2014)
Call for Papers
March 5 - March 8, 2014, Lyon, France
Submission Deadline: Sep 20, 2013 (23:59:59 GMT/UTC)
http://stacs2014.sciencesconf.org/
* SUBMISSIONS
Authors are invited to submit papers presenting original and
unpublished research on theoretical aspects of computer
science. Typical areas include (but are not limited to):
- algorithms and data structures, including: parallel, distributed,
approximation, and randomized algorithms, computational geometry,
cryptography, algorithmic learning theory, analysis of algorithms;
- automata and formal languages, games;
- computational complexity, parameterized complexity, randomness in computation;
- logic in computer science, including: semantics, specification and
verification, rewriting and deduction;
- current challenges, for example: natural computing, quantum
computing, mobile and net computing.
* INVITED SPEAKERS
- Javier Esparza, TUM - Technische Universitaet Muenchen
- Peter Bro Miltersen, Aarhus University
- Luc Segoufin, INRIA, Ecole Normale Superieure de Cachan
* TUTORIAL
Neeraj Kayal, Microsoft Research India: Arithmetic Circuit Complexity
THE SIXTH FEDERATED LOGIC CONFERENCE (FLoC 2014)
Call for Workshops
Part of VIENNA SUMMER OF LOGIC (VSL 2014)
July 2014, Vienna, Austria
* FLOC 2014
The Sixth Federated Logic Conference (FLoC 2014) will be part of the
Vienna Summer of Logic (VSL), the largest logic event in history, with
over 2000 expected participants. FLoC 2014 will host eight conferences
and many workshops. Each workshop will be affiliated with at least one
of the eight conferences.
- 26th International Conference on Computer Aided Verification (CAV)
Workshop Chair: Martina Seidl http://fmv.jku.at/seidl/
- 27th IEEE Computer Security Foundations Symposium (CSF)
Workshop Chair: Luca Vigano http://profs.sci.univr.it/~vigano/
- 30th International Conference on Logic Programming (ICLP)
Workshop Chair: Haifeng Guo http://faculty.ist.unomaha.edu/hguo/
- 7th International Joint Conference on Automated Reasoning (IJCAR)
Workshop Chair: Matthias Horbach http://www.mpi-inf.mpg.de/~horbach/
- 5th Conference on Interactive Theorem Proving (ITP)
Workshop Chair: David Pichardie http://www.irisa.fr/celtique/pichardie/
- Joint meeting of the 23rd EACSL Annual Conference on Computer Science
Logic (CSL) and the 29th ACM/IEEE Symposium on Logic in Computer Science
(LICS)
Workshop Chairs:
Patricia Bouyer-Decitre http://www.lsv.ens-cachan.fr/~bouyer/
Georg Moser http://cl-informatik.uibk.ac.at/users/georg/
- 25th International Conference on Rewriting Techniques and Applications
(RTA) joined with the 12th International Conference on Typed Lambda
Calculi and Applications (TLCA)
Workshop Chair: Aleksy Schubert http://www.mimuw.edu.pl/~alx/
- 17th International Conference on Theory and Applications of
Satisfiability Testing (SAT) Workshop Chair: Ines Lynce
http://sat.inesc-id.pt/~ines/
* SUBMISSION OF WORKSHOP PROPOSALS
Researchers and practitioners are invited to submit proposals for
workshops on topics in the field of computer science, related to logic
in the broad sense. Each workshop proposal must indicate at least one
conference to be affiliated with, and among those exactly one primary
hosting conference.
It is suggested that prospective workshop organizers contact the
relevant conference Workshop Chair(s) before submitting a proposal.
Proposals should be submitted electronically to EasyChair at the
following address: http://www.easychair.org/conferences/?conf=floc14cfw
Proposals should consist of two parts. First, a short scientific
justification of the proposed topic, its significance, and the
particular benefits of the workshop to the community, as well as a list
of previous or related workshops (if relevant). A second, organizational
part should include:
- contact information of the workshop organizers
- proposed primary hosting conference (and possibly other affiliated
conference(s))
- estimate of the audience size
- proposed format and agenda (for example, paper presentations,
tutorials, demo sessions, etc.)
- potential invited speakers
- procedures for selecting papers and participants
- plans for dissemination, if any (for example, special issues of journals)
- duration (which may vary from one day to two days) and preferred period
The FLoC Organizing Committee will determine the final list of accepted
workshops based on the recommendations from the Workshop Chairs of the
hosting conferences and subject to the availability of space and facilities.
* FURTHER INFORMATION
See the FLoC 2014 Workshop Guide http://vsl2014.at/floc-ws/
* IMPORTANT DATES
Submission of workshop proposals: by September 30, 2013
Notification: by November, 2013
Pre-FLoC workshops: Saturday & Sunday, July 12-13
Mid-FLoC workshops: Thursday & Friday, July 17-18
Post-FLoC workshops: Wednesday & Thursday, July 23-24
* CONTACT INFORMATION
Questions regarding workshop proposals should be sent to the workshop
chairs of conferences that are supposed to host the workshop (see
above). General questions should be sent to floc14cfw@easychair.org
Please consult the FLoC 2014 Workshop Guide http://vsl2014.at/floc-ws/
* FLoC 2014 WORKSHOP CHAIR
Stefan Szeider
http://www.szeider.net
Vienna University of Technology
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.
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.
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)
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
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
ASSISTANT PROFESSOR (UD) POSITION IN LOGIC
* This message is to bring to your attention that the Institute for Logic,
Language and Computation at the University of Amsterdam currently has an
open Assistant Professor (UD) Position in Logic, see
http://www.uva.nl/over-de-uva/werken-bij-de-uva/vacatures/item/13-222.html
for the details.
Please note that the deadline for applications is September 10.
As you can read in the job advertisement, we are looking for excellent
candidates in mathematical logic, with a preference for a candidate with
a proven record in modal logic or related areas of nonclassical logic.
It is the explicit policy of the institute that (in principle) new staff
are hired through open application procedures. I would therefore like to
encourage you to bring this vacancy to the attention of as many colleagues
as possible.
ASSISTANT/ASSOCIATE PROFESSORS AT DTU
* DTU Applied Mathematics and Computer Science has a new opening for associate
and/or assistant professors with a focus on the modelling, analysis and
realisation of systems using language-based techniques and tools
– in particular, static analysis (including abstract interpretation and
type systems) and (qualitative and quantitative) model checking.
The successful candidate(s) will be part of an international research team
focusing on a broad portfolio of research projects using formal methods for
modeling and analysis of systems (MT-LAB, IDEA4CPS, TREsPASS, FutureID,
SESAMO, PaPP). The date for applications is on October 1st and full details
about the call and how to apply are available at
http://www.dtu.dk/english/career/7da12e65-dc28-42f6-ad11-6be53914b384.aspx
and more information about the Language Based Technology research team is
available at http://www.compute.dtu.dk/english/research/LBT
* CONTACT
Hanne Riis Nielson & Flemming Nielson
DTU Compute - Department of Applied Mathematics and Computer Science
POSTDOCTORAL SCHOLAR POSITIONS AT THE CENTER FOR SECURE AND DEPENDABLE SYSTEMS AT UNIVERSITY OF IDAHO
* We are looking for a sharp graduate(s) to join our team as postdoctoral
scholars, starting as early as fall 2013. The postdoc(s) would be a fellow
of the Center for Secure and Dependable Systems contingent on availability
of funding.
* The postdoc will be involved in our research on security & privacy for
critical infrastructure systems; working with an interdisciplinary group
of faculty (including faculty from computer science, electrical and computer
engineering, civil engineering, sociology, psychology and business). As such,
the postdoc would join an inter-disciplinary team working on funded projects,
be responsible for conducting research, managing a team of student
researchers, publishing and presenting papers and assisting in the writing
of grant proposals.
* The candidate must have finished his or her Ph.D in Computer Science or
Computer Engineering, have experience with security and/or privacy, have
experience writing and presenting research results, have experience
conducting experimental computer security research, and have strong
programming skills. Ideal candidates will also have experience with
embedded computing, formal methods, security policies and software engineering.
* The University of Idaho (http://www.uidaho.edu/), the state’s founding
doctoral and research-intensive land-grant institution, has its principal
campus in Moscow, Idaho, and regional centers in Boise, Coeur d’Alene, and
Idaho Falls. The University engages its statewide constituents in strategic
educational, research, and service programs to enhance the well-being of
the state, its communities, and its people, as well as to develop in students,
a sense of national and global citizenship.
* To enrich education through diversity, the University of Idaho is an Equal
Opportunity/Affirmative Action. Interested candidates should send their vita
(pdf, please), and also arrange to have three letters of reference sent
directly to Dr. Jim Alves-Foss by email to jimaf-at-uidaho.edu
Those applications arriving by September 1, 2013 will receive first consideration.
POST-DOC IN ICT AT TRENTO
* One post-doc position in ICT on the research project
"Advanced SMT Techniques for Word-level Formal Verification - (WOLF)"
is available in Trento, Italy, under the joint supervision of
- Alessandro Cimatti, FBK, Trento, and
- Roberto Sebastiani, DISI, University of Trento.
The research activity will be carried out jointly within the Embedded
Systems (ES) Research Unit of the Center for Scientific and
Technological Research of the Fondazione Bruno Kessler (FBK), Trento,
and the Software Engineering, Formal Methods & Security Research
Program, at Department of Information Engineering and Computer Science
(DISI) of University of Trento.
* AIM AND SCOPE
The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for Satisfiability Modulo
Theories (SMT) for the formal verification of systems. This work will
be part of the "Advanced SMT Techniques for Word-level Formal
Verification - (WOLF)" project, a three-year research project
supported by SRC/GRC (http://www.src.org/compete/s201113/), in
collaboration with major HW companies.
The ultimate goal of the WOLF project is to provide a comprehensive
SMT package to support effective formal verification of systems
ranging from RTL circuits all the way up to high-level hardware
description languages (e.g. SystemC) and software. The package will be
implemented on top of the MathSAT SMT platform
(http://mathsat.fbk.eu/), and provided as an API.
* CANDIDATE PROFILE
The ideal candidate should have an PhD in computer science or related
discipline, and combine solid theoretical background and excellent
software development skills (in particular C/C++).
A solid background knowledge and/or previous experience on one of the
following topics (in order of preference) is required:
Satisfiability Modulo Theory (SMT), Propositional Satisfiability (SAT),
Model Checking, Automated Reasoning.
Previous experience in the following areas will also be considered
favourably: Constraint Solving and Optimization, Embedded Systems
Design Languages (e.g. Verilog, VHDL).
The candidate should be able to work in a collaborative environment,
with a strong committment to reaching research excellence and achieving
assigned objectives.
Early availability will be considered with much favour.
* TERMS AND DATES
The position will start as soon as possible, and will have to be
renewed yearly, for a maximum of two years. The expected salary
will range from about 2200 to 2400 euros net income, and the gross
will include previdential (social security) contributions. Facilities
for meals at the local canteen can be provided.
* APPLICATIONS AND INQUIRIES
Interested candidates should inquire for further information and/or
apply by sending email to wolf-recruit@disi.unitn.it, with subject
'POSTDOC ON WOLF PROJECT'.
Applications should contain a statement of interest, with a Curriculum
Vitae, and the names of reference persons. PDF format is strongly
encouraged. It should also indicate an estimated starting date.
* CONTACT PERSONS
Dr. ALESSANDRO CIMATTI,
Embedded Systems Research Unit,
FBK-Irst,
via Sommarive 18, I-38123 Povo, Trento, Italy
http://sra.fbk.eu/people/cimatti/,
Prof. ROBERTO SEBASTIANI
Software Engineering, Formal Methods & Security Research Program
DISI, University of Trento,
via Sommarive 14, I-38123 Povo, Trento, Italy
http://disi.unitn.it/~rseba/.
11 PHD SCHOLARSHIPS IN COMPUTER SCIENCE AT VERONA
* 3-year PhD Program in Computer Science at the Universita di Verona, Italy
- Deadline for application: September 23, 2013. Applications must be received
by the deadline (with preliminary online submission by Sept. 13)
- Start of program: January 1, 2014
- Number of available positions with scholarship: 11
- The application instructions can be downloaded from the following link:
http://www.univr.it/documenti/Documento/allegati/allegati754351.pdf
* CONTACT
Prof. Luca Vigano
luca.vigano@univr.it
Back to the LICS web page.