Newsletter 138
September 1, 2012
*******************************************************************
* Past issues of the newsletter are available at
http://www.informatik.hu-berlin.de/lics/newsletters/
* Instructions for submitting an announcement to the newsletter
can be found at
http://www.informatik.hu-berlin.de/lics/newsletters/inst.html
*******************************************************************
TABLE OF CONTENTS
* LICS MATTERS
LICS 2012 - Report
LICS 2013 - Test-of-Time Award
* DEADLINES
Deadlines in the coming weeks
* CALLS FOR PAPERS
EJMT Special Issue on Theorem-Prover Based Systems for Education
PLPV 2013
ETAPS 2013
FSEN 2013
LATA 2013
SVTR Special Issue on Tests and Proofs
* CALLS FOR PARTICIPATION
ICLP 2012
GANDALF 2012
LFMTP 2012
FACS 2012
RAMiCS 2012
LOPSTR 2012
PPDP 2012
ICTAC 2012
JELIA 2012
TCS 2012
ICFEM 2012
* SCHOOLS
FSFLA 2012 - Call for Participation
* AWARDS
2012 CAV Award Announcement
* BOOKS
A Computable Universe
Graph Structure and Monadic Second-Order Logic
* JOB ANNOUNCEMENTS
Positions at ETH Zurich
Lectureships at Queen Mary, University of London
Professorship in Security at Graz
PhD Position in Formal Methods/Security at Trier
PhD Opportunities at Darmstadt
LOGIC IN COMPUTER SCIENCE (LICS) 2012 REPORT
* This year's LICS was hosted by the University of Dubrovnik in Dubrovnik, Croatia.
For the first time it was sponsored by both ACM and IEEE. 135 people registered for
the main conference (40 students), and 170 overall including the workshop-only participants.
* For the second time LICS was preceded by a tutorial day featuring tutorials on
term rewriting systems (Jan Willem Klop and Joerg Endrullis) and logics of
dynamical systems (Andre Platzer).
* The 2012 Kleene Award for the Best Student Paper went to Christoph Berkholz
for his paper "Lower Bounds for Existential Pebble Games and k-Consistency Tests".
* The following papers won the 2012 Test-Of-Time Awards.
- Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine
"Symbolic model checking for real-time systems",
- Jean-Pierre Talpin, Pierre Jouvelot
"The type and effect discipline".
* We thank the local organiser Vlatko Lipovac and his team, the Conference Chair,
Andre Scedrov, the PC Chair, Nachum Dershowitz, and the PC for their hard work!
* Rajeev Alur has completed his term as LICS General Chair. We are very grateful
for his commitment and leadership over the last three years. The next General Chair
is Luke Ong.
* Next year's LICS will be held 25-28 June 2013 in New Orleans on the campus of
Tulane University, and will be collocated with MFPS and CSF.
LOGIC IN COMPUTER SCIENCE (LICS) - TEST OF TIME AWARD
* The LICS Test-of-Time Award recognizes a small number of papers from the LICS proceedings
from 20 years prior that have best met the "test of time".
* The LICS 2013 ToT Award committee consists of Martin Grohe, Tom Henzinger,
Jean-Pierre Jouannaud and Prakash Panangaden (chair).
* The committee will select between 0 to 3 papers that appeared in LICS 1993 proceedings.
All papers are nominated by default, but the committee welcomes input from our community:
please send your comments to Prakash Panangaden (prakash@cs.mcgill.ca), which will be
shared only among the committee members.
* LICS 2013 ToT award will be presented during the business meeting at LICS 2013,
to be held in New Orleans from June 23 to 28, 2013.
* The list of papers from LICS 1993 is available at
http://www2.informatik.hu-berlin.de/lics/archive/1993/index.html
* The information about LICS ToT award and the list of past winners is available at
http://www2.informatik.hu-berlin.de/lics/archive/test-of-time-award.html
DEADLINES
* EJMT Special Issue on Theorem-Prover Based Systems for Education
Paper Submission: September 15, 2012
http://www.easychair.org/conferences/?conf=cadgme12-edutps
* ETAPS 2013
Abstract Submission: October 7, 2012
http://www.etaps.org/2013
* PLPV 2013
Paper Submission: October 8, 2012
http://plpv.tcs.ifi.lmu.de/
* FSEN 2013
Abstract Submission: October 19, 2012
http://fsen.ir/2013
* LATA 2013
Paper Submission: November 9, 2012
http://grammars.grlmc.com/LATA2013/
* STVR Special Issue on Tests and Proofs
Paper submission: December 17, 2012
http://lifc.univ-fcomte.fr/tap2012/stvr/
SPECIAL ISSUE OF eJMT on THEOREM-PROVER BASED SYSTEMS FOR EDUCATION
* AIMS
CADGME, the Conference on Computer Algebra and Dynamic Geometry Sy-
stems in Mathematics Education, has a working group on Theorem-Prover
(TP) based Systems since 2009. This year's conference held in Novi Sad,
Serbia, leads to a special issue with this scope. Recently and largely unnoticed
in public, applications in science and technology drove the development of
automated and interactive theorem proving technologies, which have become
of major importance for mathematics and computer science in academia and
in industry. However, their potential for a wide-spread education technology
is unexplored, in spite of the fact, that TP exhibits features relevant for
educational systems:
- TP supports automated checks of user-input: since input states a
lemma to be proved within the logical context of a proof, a cal-
culation or a geometric construction, TP checks user-input without
specific code for large classes of input. Such automation brings
systems for step-wise problem solving within reach.
- TP covers the whole problem solving process: since TP implements
reasoning -- the core of mathematical thinking, it supports all steps
in problem solving (mathematising, comparing specifications, reason-
ing and arguing, trying various strategies, until a solution can be
verified).
- TP has underlying knowledge in a human readable format (following
the LCF-paradigm): mathematics knowledge is mechanized down to
"first principles" beginning from basic axioms and definitions; so
presenting explanations to learners is not an issue of implementa-
tion but an issue of filtering off details.
These features are distinguished from present educational mathematics
software, from CAS, DGS, Spreadsheets etc. such that they promote a
new generation of educational math assistants. Several prototypes are
under construction in academic R&D for geometry, algebra and appli-
cations in engineering disciplines. So it seems in time to publish
TP's potential and expected impact on educational practice in a
special issue.
* IMPORTANT DATES
- Deadline: September 15, 2012
- Expected publication: Spring 2013
* GUIDELINES
https://php.radford.edu/~ejmt/SubmissionGuidelines.php
* SUBMISSION SITE
http://www.easychair.org/conferences/?conf=cadgme12-edutps
* PROGRAM COMMITTEE
Roman Hasek, University of South Bohemia
Zlatan Magajna, University of Ljubljana
Filip Maric, University of Belgrade
Walther Neuper, Graz University of Technology
Pavel Pech, University of South Bohemia
Rein Prank, University of Tartu
to be completed
EUROPEAN JOINT CONFERENCES ON THEORY AND PRACTICE OF SOFTWARE (ETAPS 2013)
Call for Papers
Rome, Italy, March 16-24, 2013
http://www.etaps.org/2013
* 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 2013 is already the sixteenth
event in the series.
* MAIN CONFERENCES
- 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
* INVITED SPEAKERS
- Gilles Barthe (Fundaci—n IMDEA Software, Madrid, Spain)
- Emily Berger (Univ. of Mussachusetts, Amherst, USA)
- Krzysztof Czarnecki (Univ. of Waterloo, Canada)
- Cedric Fournet (Microsoft Research, Cambridge, UK)
- Orna Grumberg (Technion, Haifa, Israel)
- Martin Hofmann (Univ. of Munich, Germany)
- Jean-Pierre Hubaux (EPFL, Losanna, Switzerland)
- Mark S. Miller (Google Research, USA)
* IMPORTANT DATES
- 7 October 2012: Submission deadline for abstracts (strict)
- 14 October 2012: Submission deadline for full papers (strict)
- 14 December 2012: Notification of acceptance
- 8 January 2013: Camera-ready versions due
Some conferences will use a rebuttal (author response) phase.
* SATELLITE EVENTS
Around 20 satellite workshops will take place before or after ETAPS
2013. In addition, on the first Sunday of ETAPS 2013 a number of
tutorials on highly modern research topics will take place.
* HOST CITY
Rome is the capital of Italy and the country's largest and most
populated municipality. The city is located in the central-western
portion of the Italian Peninsula, on the Tiber river. Rome's history
spans over two and a half thousand years. It was the capital city of the
Roman Kingdom, of the Roman Republic and of the Roman Empire, which was
a major political and cultural influence in the lands bordering the
Mediterranean Sea. Since the 2nd century AD, Rome has been the seat of
the Papacy and, after the end of the Byzantine domination, in the eighth
century it became the capital of the Papal States. In 1871, Rome became
the capital of the Kingdom of Italy, and in 1946 that of the Italian
Republic. Rome's influence on western Civilisation can hardly be
overstated, and the city is still recognised as a centre of the arts and
education. Due to this centrality on many levels, and much of the city's
past power and influence, Rome has been nicknamed "Caput Mundi" (Latin
for "Capital of the World") and "The Eternal City".
* ORGANIZERS
The event is organized in Sapienza Universitˆ di Roma. Sapienza has a
very long and prestigious history, it is the largest university in
Europe and the second-largest in the world, with more than 150,000 students.
* CHAIRS
- General chair: Daniele Gorla
- Conferences Chair: Francesco Parisi Presicce
- Workshops Chairs: Paolo Bottoni and Pietro Cenciarelli
- Publicity Chair: Ivano Salvo
- Finance Chairs: Enrico Tronci and Federico Mari
- Web Site Chair: Igor Melatti
7TH ACM SIGPLAN WORKSHOP ON PROGRAMMING LANGUAGES MEETS PROGRAM VERIFICATION (PLPV 2013)
Call for Papers
Rome, Italy, January 22, 2013 (Affiliated with POPL 2013)
http://plpv.tcs.ifi.lmu.de/
* OVERVIEW
The goal of PLPV is to foster and stimulate research at the
intersection of programming languages and program verification, by
bringing together experts from diverse areas like types, contracts,
interactive theorem proving, model checking and program analysis. Work
in this area typically attempts to reduce the burden of program
verification by taking advantage of particular semantic or structural
properties of the programming language. One example are dependently
typed programming languages, which leverage a language's type system
to specify and check rich specifications. Another example are
extended static checking systems which incorporate contracts with
either static or dynamic contract checking.
* SUBMISSIONS
We invite submissions on all aspects, both theoretical and practical,
of the integration of programming language and program verification
technology. To encourage interaction between different
communities, we seek a broad scope for PLPV. In particular,
submissions may have diverse foundations for verification (based on
types, Hoare-logic, abstract interpretation, etc), target
different kinds of programming languages (functional, imperative,
object-oriented, etc), and apply to diverse kinds of program
properties (data structure invariants, security properties, temporal
protocols, resource constraints, etc).
* IMPORTANT DATES
- Submission 8th October, 2012 (Monday)
- Notification 1st November, 2012 (Thursday)
- Final Version 8th November, 2012 (Thursday)
- Workshop 22nd January, 2013 (Tuesday)
* PUBLICATION
Accepted papers will be published by the ACM and will appear in the ACM Digital library.
* PROGRAM COMMITTEE
Andreas Abel Ludwig-Maximilians-University Munich (co-chair)
Robert Atkey University of Strathclyde
Harley Eades The University of Iowa
Chung-Kil Hur Max Planck Institute for Software Systems
Brigitte Pientka McGill University
Andrew Pitts University of Cambridge
Franois Pottier INRIA
Tim Sheard Portland State University (co-chair)
Makoto Takeyama Advanced Industrial Science and Technology
5TH INTERNATIONAL CONFERENCE ON FUNDAMENTALS OF SOFTWARE ENGINEERING (FSEN 2013)
Call for Papers
Tehran, Iran, April 24-26, 2013
http://fsen.ir/2013
* AIM
FSEN is an international conference that aims to bring together
researchers, engineers, developers, and practitioners from the
academia and the industry, who work in every area of formal
methods. This conference seeks to facilitate the transfer of
experience, adaptation of methods, and where possible, foster
collaboration among different groups. The topics of interest cover all
aspects of formal methods, especially those related to advancing the
application of formal methods in the software industry and promoting
their integration with practical engineering techniques. Following the
success of the previous FSEN events in 2005, 2007, 2009, and 2011, the
next event in the FSEN series will take place in Tehran, Iran, April
24-26, 2013.
* IMPORTANT DATES
Abstract Submission: October 19, 2012
Paper Submission: October 26, 2012
Notification: December 14, 2012
Camera Ready: January 11, 2013
Conference: April 24-26, 2013
* TOPICS
The topics of this conference include, but are not restricted to, the
following:
- Models of programs and systems
- Software specification, validation, and verification
- Software architectures and their description languages
- Object and multi-agent systems
- Coordination and feature interaction
- Integration of formal and informal methods
- Integration of different formal methods
- Component-based development
- Service-oriented development
- Model checking and theorem proving
- Software and hardware verification
- CASE tools and tool integration
- Application to industrial cases
* PROCEEDINGS
The post-proceedings of FSEN'13 will be published by Springer Verlag
in the LNCS series (to be confirmed). There will also be a
pre-proceeding for the accepted papers, printed locally by IPM. This
pre-proceeding will be made available at the conference.
* CHAIRS
- General Chair
Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran
- Program Chairs
Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
Marjan Sirjani - Reykjavik University, Iceland; University of Tehran, Iran
7th INTERNATIONAL CONFERENCE ON LANGUAGE AND AUTOMATA, THEORY AND APPLICATIONS (LATA 2013)
Call for Papers
Bilbao, Spain, April 2-5, 2013
http://grammars.grlmc.com/LATA2013/
* AIMS
LATA is a yearly conference in theoretical computer science and its applications.
Following the tradition of the International Schools in Formal Languages and
Applications developed at Rovira i Virgili University in Tarragona since 2002, LATA
2013 will reserve significant room for young scholars at the beginning of their
career. It will aim at attracting contributions from both classical theory fields
and application areas (bioinformatics, systems biology, language technology,
artificial intelligence, etc.).
* VENUE
LATA 2013 will take place in Bilbao, at the Basque Country in Northern Spain. The
venue will be the Basque Center for Applied Mathematics (BCAM).
* SCOPE
Topics of either theoretical or applied interest include, but are not limited to:
- algebraic language theory
- algorithms for semi-structured data mining
- algorithms on automata and words
- automata and logic
- automata for system analysis and programme verification
- automata, concurrency and Petri nets
- automatic structures
- cellular automata
- combinatorics on words
- computability
- computational complexity
- computational linguistics
- data and image compression
- decidability questions on words and languages
- descriptional complexity
- DNA and other models of bio-inspired computing
- document engineering
- foundations of finite state technology
- foundations of XML
- fuzzy and rough languages
- grammars (Chomsky hierarchy, contextual, multidimensional, unification, categorial, etc.)
- grammars and automata architectures
- grammatical inference and algorithmic learning
- graphs and graph transformation
- language varieties and semigroups
- language-based cryptography
- language-theoretic foundations of artificial intelligence and artificial life
- parallel and regulated rewriting
- parsing
- pattern recognition
- patterns and codes
- power series
- quantum, chemical and optical computing
- semantics
- string and combinatorial issues in computational biology and bioinformatics
- string processing algorithms
- symbolic dynamics
- symbolic neural networks
- term rewriting
- transducers
- trees, tree languages and tree automata
- weighted automata
* STRUCTURE
LATA 2013 will consist of
- 3 invited talks
- 2 invited tutorials
- peer-reviewed contributions
* PROGRAMME COMMITTEE
Parosh Aziz Abdulla (Uppsala)
Franz Baader (Dresden)
Jos Baeten (CWI, Amsterdam)
Christel Baier (Dresden)
Gerth Stolting Brodal (Aarhus)
John Case (Delaware)
Marek Chrobak (Riverside)
Mariangiola Dezani (Torino)
Rod Downey (Wellington)
Ding-Zhu Du (Dallas)
Ivo Duentsch (Brock)
E. Allen Emerson (Austin)
Javier Esparza (Technical University Munich)
Michael R. Fellows (Darwin)
Alain Finkel (ENS Cachan)
Dov M. Gabbay (King's, London)
Juergen Giesl (Aachen)
Rob van Glabbeek (NICTA, Sydney)
Georg Gottlob (Oxford)
Annegret Habel (Oldenburg)
Reiko Heckel (Leicester)
Sanjay Jain (Singapore)
Charanjit S. Jutla (IBM Thomas J. Watson)
Ming-Yang Kao (Northwestern)
Deepak Kapur (Albuquerque)
Joost-Pieter Katoen (Aachen)
S. Rao Kosaraju (Johns Hopkins)
Evangelos Kranakis (Carleton)
Hans-Joerg Kreowski (Bremen)
Tak-Wah Lam (Hong Kong)
Gad M. Landau (Haifa)
Kim G. Larsen (Aalborg)
Richard Lipton (Georgia Tech)
Jack Lutz (Iowa State)
Ian Mackie (Ecole Polytechnique, Palaiseau)
Rupak Majumdar (Max Planck, Kaiserslautern)
Carlos Martin-Vide (Tarragona, chair)
Paliath Narendran (Albany)
Tobias Nipkow (Technical University Munich)
David A. Plaisted (Chapel Hill)
Jean-Francois Raskin (Brussels)
Wolfgang Reisig (Humboldt Berlin)
Michael Rusinowitch (LORIA, Nancy)
Davide Sangiorgi (Bologna)
Bernhard Steffen (Dortmund)
Colin Stirling (Edinburgh)
Alfonso Valencia (CNIO, Madrid)
Helmut Veith (Vienna Tech)
Heribert Vollmer (Hannover)
Osamu Watanabe (Tokyo Tech)
Pierre Wolper (Liege)
Louxin Zhang (Singapore)
* PUBLICATION
A volume of proceedings published by Springer in the LNCS series will be available
by the time of the conference.
* DEADLINES
Paper submission: November 9, 2012 (23:59 CET)
Notification of paper acceptance or rejection: December 16, 2012
Final version of the paper for the LNCS proceedings: December 25, 2012
STVR SPECIAL ISSUE ON TESTS AND PROOFS
Call for Papers
http://lifc.univ-fcomte.fr/tap2012/stvr/
* The Software Testing, Verification & Reliability (STVR) journal
(http://www3.interscience.wiley.com/journal/13635/home) invites
authors to submit papers to a Special Issue on Tests and Proofs.
* The increasing use of software and the growing system complexity make
focused software testing a challenging task. Recent years have seen an
increasing industrial and academic interest in the use of static and
dynamic analysis techniques together. Success has been reported
combining different test techniques such as model-based testing,
structural testing, or concolic testing with static techniques such as
program slicing, dependencies analysis, model-checking, abstract
interpretation, predicate abstraction, or verification. This special
issue serves as a platform for researchers and practitioners to
present theory, results, experience and advances in Tests and Proofs
(TAP).
* SUBMISSION INFORMATION
All submissions must contain original unpublished work not being
considered for publication elsewhere. Original extensions to
conference papers - identifing clearly additional contributions - are
also encouraged unless prohibited by copyright. Submissions will be
refereed according to standard procedures for Software Testing,
Verification and Reliability. Please submit your paper electronically
using the Software Testing, Verification & Reliability manuscript
submission site. Select "Special Issue Paper" and enter "Tests and
Proofs" as title.
* IMPORTANT DATES
- Paper submission: December 17, 2012
- Notification: April 15, 2013
* GUEST EDITORS
- Achim D. Brucker, SAP Research, Germany
http://www.brucker.ch/
- Wolfgang Grieskamp, Google, U.S.A.
http://www.linkedin.com/in/wgrieskamp
- Jacques Julliand, University of Franche-ComtŽ, France
http://lifc.univ-fcomte.fr/page_personnelle/accueil/8
28TH INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING (ICLP2012)
Call for Participation
Budapest, Hungary, September 4-8, 2012
http://www.cs.bme.hu/iclp2012/
* CONFERENCE SCOPE
Since the first conference held in Marseille in 1982, ICLP has been
the premier international conference for presenting research in logic
programming. This year conference will offer invited talks and
tutorials, as well as technical presentations on the broad spectrum of
most recent research topics in the field. The conference will also
host Doctoral Consortium, several workshops, and a Prolog programming
contest.
* WORKSHOPS
- Answer Set Programming and Other Computing Paradigms (ASPOCP 2012),
September 4
- 9th International Workshop on Constraint Handling Rules (CHR 2012),
September 4
- 12th International Colloquium on Implementation of Constraint and
LOgic Programming Systems (CICLOPS 2012), September 4
- WG17, September 4-5
- 22nd Workshop on Logic-based methods in Programming Environments
(WLPE 2012), September 8
- Constraint Based Methods for Bioinformatics (WCB'12), September 8
- Coinductive Logic Programming (Co-LP), September 8
* DOCTORAL CONSORTIUM
The 8th Doctoral Consortium (DC) on Logic Programming provides
research students with the opportunity to present and discuss their
research directions, and to obtain feedback from both peers and
world-renown experts in the field.
* INVITED TALKS
- Ferenc Darvas (http://www.thalesnano.com/board_of_directors)
"Several Applications of Logic Programming in Hungary"
- Jan Wielemaker (http://www.cs.vu.nl/~janw/)
"25 years of SWI Prolog"
- Mike Elston (http://www.securitease.com/)
"Applications of Prolog and CHR to stock brokering tools"
- Invited author(s) of the most influencial paper of ICLP/ILPS 1992
- Invited author(s) of the most influencial paper of ICLP 2002
* TUTORIAL
- Viviana Mascardi (http://www.disi.unige.it/person/MascardiV/)
"Logic-based Agents and the Semantic Web"
* CONFERENCE VENUE
The Conference will be located in Tulip Inn Budapest Millennium. Budapest
is in the center of Hungary, in the heart of Central Europe. Hungary is
member of the European Union and belongs to the Schengen area.
3RD INTERNATIONAL SYMPOSIUM ON GAMES, AUTOMATA, LOGICS AND FORMAL VERIFICATION (GANDALF 2012)
Call for Participation
Napoli, Italy, September 6-8, 2012
http://www.gandalf.unina.it
* OBJECTIVES
The aim of the symposium is to bring together researchers from academia
and industry which are actively working in the fields of Games, Automata,
Logics, and Formal Verification. The idea is to cover an ample spectrum of
themes, ranging from theory to applications, and stimulate
cross-fertilization.
* PROGRAMME
Programme of GandALF 2012 consists of 19 contributed talks (for the list of
accepted papers, please have a look at http://www.gandalf.unina.it//accepted.php)
that have been selected by the programme committee on the basis of submitted papers.
For the detailed program of GandALF 2010, please have a look at
http://www.gandalf.unina.it//program.php
* REGISTRATION
On site registration fee can be paid only in cash. Since September is considered
high season in Napoli, we suggest to book your hotel as soon as possible.
Registration fee: 350 euros (normal registration)
* CO-LOCATED EVENT
GAMES 2012, Annual Workshop of the ESF Networking Programme on Games for
Design and Verification (http://www.games.unina.it/).
* INVITED SPEAKERS
Alberto Policriti (University of Udine, Italy).
Moreover, we have the following three joint invited speakers with the
co-located GAMES meeting:
- Joseph Halpern, Cornell University, USA
- Damian Niwinski, Warsaw University, Poland
- Jean-Franois Raskin, UniversitŽ Libre de Bruxelles, Belgium
7TH INTERNATIONAL WORKSHOP ON LOGICAL FRAMEWORKS AND META-LANGUAGES: THEORY AND PRACTICE (LFMTP 2012)
Call for Participation
Copenhagen, Denmark, September 9, 2012
Affiliated with ICFP 2012
http://people.csail.mit.edu/adamc/lfmtp12/
* AIMS
Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science. Their
design and implementation on the one hand and their use in reasoning
tasks ranging from the correctness of software to the properties of
formal computational systems on the other hand have been the focus of
considerable research over the last two decades. This workshop will
bring together designers, implementors, and practitioners to discuss
various aspects impinging on the structure and utility of logical
frameworks, including the treatment of variable binding, inductive and
co-inductive reasoning techniques and the expressivity and lucidity of
the reasoning process.
* INVITED TALKS
Brigitte Pientka, Beluga^mu: Programming Proofs in Context
Nicolas Pouillard, From de Bruijn to nowadays: The evolution of
libraries for binding representation.
Robert J. Simmons, A Walk in the Substructural Park.
Stephanie Weirich, A POPLmark retrospective: Using proof assistants in
programming language research.
* FURTHER INFO
Other details concerning the workshop can be found on its website at
http://people.csail.mit.edu/adamc/lfmtp12
9TH INTERNATIONAL SYMPOSIUM ON FORMAL ASPECTS OF COMPONENT SOFTWARE (FACS 2012)
Call for Participation
Mountain View, USA, September 12-14, 2012
http://www.cmu.edu/silicon-valley/facs12/
* SCOPE
The component-based software development approach has emerged as a
promising paradigm to cope with the complexity of present-day software
systems by bringing sound engineering principles into software
engineering. However, many challenging conceptual and technological
issues still remain in component-based software development theory and
practice. Moreover, the advent of service-oriented computing has
brought to the fore new dimensions, such as quality of service and
robustness to withstand inevitable faults, that require revisiting
established component-based concepts in order to meet the new
requirements of the service-oriented paradigm.
FACS 2012 is concerned with how formal methods can be used to make
component-based and service-oriented software development
succeed. Formal methods have provided a foundation for component-based
software by successfully addressing challenging issues such as
mathematical models for components, composition and adaptation, or
rigorous approaches to verification, deployment, testing, and
certification.
* INVITED SPEAKERS
- Tevfik Bultan, UC Santa Barbara
"Analyzing Interactions of Asynchronously Communicating Software Components"
- Shaz Qadeer, Microsoft
"Safe programming of asynchronous interaction: Can we do it for real?"
* REGISTRATION
Standard Registration will conclude on Friday, September 7th at 5:00 p.m. (EST)
13TH INTERNATIONAL CONFERENCE ON RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMiCS 2012)
Call for Participation
Cambridge, UK, September 17-20, 2012
http://www.cl.cam.ac.uk/conference/ramics13/
* FOCUS
The RAMiCS Conference is the main forum for Relational and Algebraic Methods
in Computer Science. Special focus lies on formal methods for software
engineering, logics of programs and links with neighbouring disciplines.
* HIGHLIGHTS
The conference features 2 tutorials, 3 invites talks, and 23
reviewed papers. There will also be five student papers
(see the call-for-student-papers on the conference web site).
* TUTORIALS
- Dexter Kozen (Cornell University, USA)
Kleene Algebra with Tests
- Lawrence C. Paulson (Cambridge University, UK)
Tutorial on the Isabelle Theorem Prover.
* INVITED TALKS
- Alexander Kraus (TU Munich, Germany)
Formalized Regular Expression Equivalence and Relation Algebra in Isabelle.
- Peter O'Hearn (University College London, UK)
Towards an Axiomatic Approach to Concurrency.
- Damien Pous (CNRS Grenoble, France)
Using Relation Algebraic Methods in the Coq Proof Assistant
* REGISTRATION
Registration closes 10 September 2012.
22ND INTERNATIONAL SYMPOSIUM ON LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2012)
Call for Participation
Leuven, Belgium, September 18-20, 2012
http://costa.ls.fi.upm.es/lopstr12
* REGISTRATION LINK
There is a significant discount if you register for both PPDP and LOPSTR.
http://dtai.cs.kuleuven.be/events/PPDP2012/reg.html
14TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2012)
Call for Participation
Leuven, Belgium, September 19-21, 2012
http://dtai.cs.kuleuven.be/events/PPDP2012/
* REGISTRATION LINK
There is a significant discount if you register for both PPDP and LOPSTR.
http://dtai.cs.kuleuven.be/events/PPDP2012/reg.html
9TH INTERNATIONAL COLLOQUIUM ON THEORETICAL ASPECTS OF COMPUTING (ICTAC 2012)
Call for Participation
Bangalore, India, September 24-27, 2012
http://www.iiitb.ac.in/ictac/
* GENERAL
ICTAC 2012 will be the 9th version of the International Colloquium on
Theoretical Aspects of Computing, a series founded by the
International Institute for Software Technology of the United Nations
University (UNU-IIST). ICTAC 2012 will bring together researchers
from academia and industry who are working on challenges in
theoretical aspects of computing, including using of theory for
devising and developing systems. The conference will also act as a
forum for interaction and cooperation in education and research
between participants and their institutions, from developing and
industrial countries, as in the mandate of the United Nations
University.
* EVENTS
Plans for events as a part of ICTAC 2012 include a school on Software
Engineering, involving extensive participation from students and
researchers from academia and industry, tutorials and workshops, along
with invited and research paper presentations.
* INDUSTRY DAY
ICTAC 2012 will feature an Industry Day, a special feature being
introduced to the ICTAC colloquium for the first time. One of the
days of the conference has been marked as Industry Day.
* REGISTRATION
http://www.iiitb.ac.in/ictac/registration.html
* KEYNOTES
ICTAC 2012 will feature three invited talks. These are by
Luke Ong (University of Oxford) - Day 1
Gernot Heiser (UNSW and NICTA Australia) - Day 2
G. Ramalingam (MSR India) - Day 3
* PROGRAM
Monday September 24 : School on Software Engineering
Tuesday September 25 - Day 1 of Main Conference
Wednesday September 26 - Day 2 of conference [Industry Day]
Thursday September 27 - Day 3 of conference
Conference program appears at http://www.iiitb.ac.in/ictac/program
Details about School on Software Engineering appear at
http://www.iiitb.ac.in/ictac/School-on-Software-Engineering.html
12TH EUROPEAN CONFERENCE ON LOGICS IN ARTIFICIAL INTELLIGENCE (JELIA 2012)
Call for Participation
Toulouse, France, September 26-28, 2012
http://www.irit.fr/jelia2012
* Logics provide a formal basis and key descriptive notation for the study
and development of applications and systems in Artificial Intelligence
(AI). With the depth and maturity of formalisms, methodologies, and
systems today, such logics are increasingly important. The European
Conference on Logics in Artificial Intelligence (or Journees Europeennes
sur la Logique en Intelligence Artificielle --- JELIA) began back in
1988, as a workshop, in response to the need for a European forum for
the discussion of emerging work in this field. Since then, JELIA has
been organized biennially, with English as the official language, and
with proceedings published in Springer-Verlag's Lecture Notes in
Artificial Intelligence series. In 2012 the conference is organized in
Toulouse, France. The increasing interest in this forum, its
international level with growing participation from researchers outside
Europe, and the overall technical quality, has turned JELIA into a major
forum for the discussion of logic-based approaches to AI.
* SCIENTIFIC PROGRAM
The scientific program consists of three invited talks, 36 regular
papers, and 5 system descriptions. See the list of accepted papers at
http://www.irit.fr/jelia2012/acc_papers.html.
* INVITED SPEAKERS
Leila Amgoud (http://www.irit.fr/~Leila.Amgoud) and Philippe Besnard
(http://www.irit.fr/~Philippe.Besnard)
Ulrich Furbach (http://www.furbach.de/Uni)
Wiebe van der Hoek (http://www.csc.liv.ac.uk/~wiebe)
* VENUE
The conference will be held in the auditorium Jacques Herbrand of the
Institut de recherche en informatique de Toulouse (IRIT), reachable from
downtown via the underground. Toulouse Blagnac airport has connections
to many European cities, including London, Manchester, Bristol, Leeds,
Edinburgh, Dublin, Amsterdam, Brussels, Geneva, Frankfurt, Munich,
Hamburg, Oslo, Rome, Milan, Lisbon, Madrid and Athens, as well as an
intercontinental connection to Montreal. Toulouse Matabiau train station
has TGV connections to Paris, Lyons, Lille and Marseille; you may search
for other connections on http://www.bahn.de. More information can be
found on http://www.irit.fr/jelia2012/location.html.
7TH IFIP CONFERENCE ON THEORETICAL COMPUTER SCIENCE (TCS 2012)
Call for Participation
Amsterdam, The Netherlands, September 26-28, 2012
http://tcs.project.cwi.nl
* The conference Theoretical Computer Science, which is held every two
years, either in conjunction with or in the framework of the IFIP World
Computing Congress, is the meeting place of the TC1 community where
new results of computation theory are presented and more broadly experts
in theoretical computer science meet to share insights and ask questions
about the future directions of the field.
* TCS 2012 is associated with The Alan Turing Year 2012
(http://www.mathcomp.leeds.ac.uk/turing2012).
* TCS 2012 will be held at the Centrum Wiskunde & Informatica (CWI),
Amsterdam (http://www.cwi.nl), The Netherlands.
* INVITED SPEAKERS
Rajeev Alur
Yuri Gurevich
Jiri Wiedermann
* CHAIRS
- General Chair
Jos Baeten (http://www.cwi.nl/people/630)
* PC Co-Chairs:
Tom Ball (http://research.microsoft.com/en-us/people/tball/) and
Frank de Boer (http://homepages.cwi.nl/~frb/)
* PROGRAM COMMITTEE
Ahmed Bouajjani
Ana Cavalcanti
Peter GrŸnwald
Joseph Kiniry
Peter Mueller
David Naumann
Susanne Graf
Juraj Hromkovic
Martin Kutrib
Aart Middeldorp
Jan Juerjens
Ugo Montanari
Catuscia Palamidessi
Jeff Shallit
Jan Rutten
Davide Sangiorgi
Igor Walukiewicz
Jim Woodcock
Leen Torenvliet
* LOCAL ORGANIZATION
Susanne van Dam
Michiel Helvensteijn
Hans Hidskes
Joost Winter
14TH INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS (ICFEM 2012)
Call for Participation
Kyoto Research Park, Kyoto, Japan, November 12-16, 2012
http://www.jaist.ac.jp/icfem2012
* REGISTRATION
http://www.jaist.ac.jp/icfem2012/registration/index.html.
We encourage you to reserve your hotel rooms ASAP, since it is a peak season
in Kyoto for brilliant autumn leaves! This year's ICFEM has four affiliated workshops
and a tutorial, and three prominent invited speakers.
* CO-LOCATED EVENTS
- FTSCS 2012 : First International Workshop on Formal Techniques for
Safety-Critical Systems, http://www.ftscs12.org/
- WSOFL 2012 : 2nd Workshop on SOFL, http://icfem-fema.org/sofl/
- Event-B 2012 : DS-Event-B-2012: Workshop on the experience of and advances in
developing dependable systems in Event-B, http://research.nii.ac.jp/eventb2012/
- Japanese Workshop on Industrial Applications of Formal Methods
- CbC-Depend: Correct-by-Construction Development of Dependable Systems,
Tutorial, http://www.rodintools.org/tutorial.html
* INVITED SPEAKERS
- Darren Cofer (Rockwell Collins, USA), "Formal Methods in the Aerospace
Industry: Follow the Money"
- Robert Shostak (Vocera Communications, Inc., USA), "Applying Term Rewriting
to Speech Recognition of Numbers"
- Mario Tokoro (Sony Computer Science Laboratories, Inc., Japan), "Toward
Practical Application of Formal Methods in Software Lifecycle Processes"
* ACCEPTED PAPERS
The list of accepted papers may be found at:
http://www.jaist.ac.jp/icfem2012/acceptedPapers/index.html
* ORGANIZATION COMMITTEE
- General Chairs:
Kokichi Futatsugi, JAIST, Japan
Shaoying Liu, Hosei Uni., Japan
- Conference Chair:
Hitoshi Ohsaki, AIST, Japan
- Program Chairs:
Kenji Taguchi, AIST, Japan
Toshiaki Aoki, JAIST, Japan
INTERNATIONAL FALL SCHOOL IN FORMAL LANGUAGES AND APPLICATIONS (FSFLA 2012)
Call for Participation
Tarragona, Spain, October 29 - November 2, 2012
http://grammars.grlmc.com/fsfla2012/
* ORGANIZATION
Research Group on Mathematical Linguistics (GRLMC)
Rovira i Virgili University
* AIM
FSFLA 2012 offers a broad and intensive series of lectures at different
levels on selected topics in language and automata theory and their
applications. The students choose their preferred courses according to their
interests and background. Instructors are top names in their respective
fields. The School intends to help students initiate and foster their
research career. The previous event in this series was FSFLA 2011
(http://grammars.grlmc.com/fsfla2011/).
* AUDIENCE
Graduate (and advanced undergraduate) students from around the world. Most
appropriate degrees include: Computer Science and Mathematics. Other
students (for instance, from Linguistics, Electrical Engineering, Molecular
Biology or Logic) are welcome too provided they have a good background in
discrete mathematics. The School is appropriate also for people more advanced
in their career who want to keep themselves updated on developments in the field.
There is no overlap in the class schedule.
* COURSES AND PROFESSORS
- Eric Allender (Rutgers), Circuit Complexity: Recent Progress in Lower
Bounds [introductory/advanced, 8 hours]
- Amihood Amir (Bar-Ilan), Periodicity and Approximate Periodicity in
Pattern Matching [introductory, 6 hours]
- Ahmed Bouajjani (Paris 7), Automated Verification of Concurrent Boolean
Programs [introductory/advanced, 8 hours]
- Bruno Courcelle (Bordeaux), Automata for Monadic Second-order Model
Checking [intermediate, 8 hours]
- Jšrg Flum (Freiburg), The Halting Problem for Turing Machines
[introductory/advanced, 6 hours]
- Aart Middeldorp (Innsbruck), Termination of Rewrite Systems
[introductory/intermediate, 8 hours]
* REGISTRATION
http://grammars.grlmc.com/fsfla2012/Registration.php
* FEES
People registering on site at the beginning of the School must pay in cash.
For the sake of local organization, however, it is much recommended to do it
earlier.
* ACCOMMODATION:
Information about accommodation is available on the website of the School.
2012 CAV AWARD ANNOUNCEMENT
* The 2012 CAV (Computer-Aided Verification) Award was presented on
July 11, 2012, at the 24th annual CAV conference in Berkeley, California,
to Sam Owre, John Rushby, and Natarajan Shankar of SRI International.
The annual award, which recognizes a specific fundamental contribution
or a series of outstanding contributions to the CAV field includes a $10,000 award.
The award was presented with the citation: "for developing PVS (Prototype
Verification System) which, due to its early emphasis on integrated decision
procedures and user friendliness, significantly accelerated the application
of proof assistants to real-world verification problems."
A COMPUTABLE UNIVERSE
A Computable Universe
Understanding and Exploring Nature as Computation
edited by Hector Zenil (University of Sheffield, UK)
World Scientific
http://www.worldscientific.com/worldscibooks/10.1142/8306
* For a limited period, you can pre-order your copy at an Introductory Offer
from our online bookstore. This offer is valid from now till 31 December, 2012.
We hope you could consider recommending this title to your institutional library
and colleagues.
* This volume, with a foreword by Sir Roger Penrose, discusses the
foundations of computation in relation to nature. It focuses on two main questions:
- What is computation?
- How does nature compute?
The contributors are world-renowned experts who have helped shape a
cutting-edge computational understanding of the universe. They discuss
computation in the world from a variety of perspectives, ranging from
foundational concepts to pragmatic models to ontological conceptions and
philosophical implications.
* The volume provides a state-of-the-art collection of technical papers
and non-technical essays, representing a field that assumes information
and computation to be key in understanding and explaining the basic
structure underpinning physical reality. It also includes a new edition
of Konrad Zuse's "Calculating Space" (the MIT translation), and a panel
discussion transcription on the topic, featuring worldwide experts in
quantum mechanics, physics, cognition, computation and algorithmic
complexity.
* The volume is dedicated to the memory of Alan M Turing --- the inventor
of universal computation, on the 100th anniversary of his birth, and is
part of the Turing Centenary celebrations.
GRAPH STRUCTURE AND MONADIC SECOND-ORDER LOGIC
Graph Structure and Monadic Second-Order Logic (A Language-Theoretic Approach)
by Bruno Courcelle (UniversitŽ de Bordeaux) and Joost Engelfriet (Universiteit Leiden),
Cambridge University Press,
Volume 138 of Encyclopedia of Mathematics and its Applications,
ISBN: 9780521898331, 730 pages
http://www.cambridge.org/gb/knowledge/isbn/item5758776
* Finite graphs and relational structures can be described algebraically, enabling
them to be constructed out of more basic elements. Separately the properties of
graphs can be studied in Monadic Second-order Logic. These two features are
brought together for the first time in a presentation that unifies and synthesizes
research over the last 25 years.
* The authors not only provide a thorough description of the theory, but also detail
its applications, on the one hand to the construction of FPT graph algorithms, and,
on the other to the extension of Formal Language Theory to finite graphs
(context-free grammars, recognizability and transductions). The book will be of
interest to graduate students and researchers in Graph Theory, Finite Model
Theory, Formal Languages, and Complexity Theory.
* Further information: courcell@labri.fr, engelfri@liacs.nl
POSITIONS AT ETH ZURICH
* Positions are available in Bertrand Meyer's group at ETH Zurich, the Chair
of Software Engineering in connection with a recent Advanced Investigator
Grant from the European Research Council (5 years, 2.5 million euros);
the project description is at http://se.inf.ethz.ch/research/scoop/CME.pdf.
In addition to this project (Concurrency Made Easy) we are recruiting for
our effort of building an advanced verification environment around Eiffel,
"Verification As a Matter of Course" (see e.g. the slides at
http://se.ethz.ch/~meyer/publications/methodology/programming-10years-sierre.pdf,
although the details are no longer up to date).
* REQUIREMENTS
- Good knowledge of software verification techniques
- For the concurrency project, excellent background in concurrency
- Good publications on relevant topics (particularly for the postdoc positions)
- Excellent mastery of object-oriented programming, including Eiffel concepts & Design by Contract
- Mix of theoretical and practical (software development) talents
- Passion for research and determination to advance the state of software engineering
The positions are available immediately.
* Please send a CV to se-open-positions@lists.inf.ethz.ch; also include a position
statement describing (briefly, half a page to two
pages) on what topics you would like to work and what you think you can contribute.
Obviously you should take some time to become
familiar with our work at http://se.ethz.ch, especially the Research pages.
LECTURESHIPS AT QUEEN MARY, UNIVERSITY OF LONDON
* The School of Electronic Engineering and Computer Science (EECS) is looking to
recruit up to three Lecturers within the research area of Theoretical Computer
Science as part of the on-going strategic investment by Queen Mary, University of
London.
* The Theoretical Computer Science group has a reputation for work that combines
leading research on fundamental mathematical and logical techniques for reasoning
about computational systems with the ability to apply those techniques to practical
problems, particularly in the software domain. We seek to appoint staff whose
research fits with the current remit of the group and who will complement our
existing expertise in areas such as verification, programming languages, program
analysis, security and wide-area systems or extend it by introducing new
mathematical expertise.
* The posts are full time and permanent and are available from October 2012. Starting
salary will be in the range £37,819 - £47,088 per annum. Benefits include 30 days
annual leave, defined benefits pension scheme and an interest-free season ticket
loan. The closing date for applications is Tuesday 4th September 2012. Applications
received after this time will not be considered. Interviews are expected to be held on
Monday 8th and Tuesday 9th October 2012.
* FURTHER INFO
http://webapps.qmul.ac.uk/hr/vacancies/jobs.php?id=3218
PROFESSOR POSITION IN SECURITY AT GRAZ
* POST
The institute of Applied Information Processing, Department of Computer
Science at Graz University of Technology is inviting applications for a
Professor position in IT Security / Cloud Security. The contract will initially
be for a 6-year period with an optional extension to a tenured position.
The basic salary is set down in the collective bargaining agreement for
university employees. Professors are in the remuneration group A1.
For the position the monthly salary is 4.571,20 Euro per month (14x).
Depending on qualification and experience a higher salary can be a topic
in the negotiations with the rector.
* DETAILS
We are looking for an excellent researcher who focuses on promising areas
such as Security and Privacy in the Cloud or Security in the Internet of Things.
The research area should reinforce or complement existing research strengths
in RFID Security, Secure Implementations, Cryptography, e-Government, Trusted
Computing, and Formal Methods. Graz University of Technology is committed
to increasing the percentage of female scientists in teaching and research.
Given applicants with equal qualifications, we give priority to women.
* MORE DETAILS
http://tinyurl.com/itsecurit
* DEADLINE
Application Deadline: 15 October 2012
FULLY FUNDED PH.D. POSITION IN FORMAL METHODS/SECURITY AT UNIVERSITY OF TRIER
* The Chair for Information Security and Cryptography at
University of Trier, Germany, offers a full-time PhD
position. The PhD candidate will contribute to the research
in the project "Implementation-Level Analysis of E-Voting
Systems", which is funded by the German Research Foundation
(DFG) and is part of the DFG priority programme "Reliably
Secure Software Systems - RS3". The goal of this project is
to develop general methods and techniques for the security
analysis of Java systems that use cryptography, with
e-voting systems being one of the motivating examples. The
project combines techniques from program
analysis/verification with techniques from cryptography and
cryptographic protocol analysis.
* The position is fully funded. There are no teaching
obligations. The starting date is negotiable. Subject to
the final decision of the DFG, the position will be
available from October 1st, 2012. Contracts are initially
offered for two years, with the perspective of an
extension by another two years.
* The successful candidate should have a Master's degree (or
should be very close to completion thereof) in Computer
Science, Mathematics, Information Security, or a related
field, with a strong background in Theoretical Computer
Science. Knowledge in program analysis/verification, logic, or
cryptography is an asset. Good English skills are
expected; knowledge of German is not required.
* Please send your application by e-mail to Ralf Kuesters
(kuesters@uni-trier.de), with relevant documents attached
in pdf format. The deadline for applications is September
30th, 2012. However, late applications will be considered until the
position is filled.
* For details see
http://infsec.uni-trier.de/job-openings/a-full-time-phd-position.html
PHD OPPORTUNITIES AT DARMSTADT
* Applications are invited for PhD opportunities in Finite & Algorithmic
Model Theory in the Logic Group, TU Darmstadt, Germany. Available
positions offer the opportunity to work towards a PhD in mathematics
under the scientific direction of Prof Martin Otto, primarily but not exclusively
in the framework of a new DFG funded research project on the algorithmic
and finite model theory of hypergraphs and of modal and guarded logics
over graphs and hypergraphs.
* See http://www3.mathematik.tu-darmstadt.de/index.php?id=2220&L=1
for further information.
* Informal preliminary inquiries by email are welcome and should be
directed to otto@mathematik.tu-darmstadt.de
Back to the LICS web page.