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.