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.