Newsletter 150 September 7, 2013 ******************************************************************* * Past issues of the newsletter are available at http://lics.siglog.org/newsletters/ * Instructions for submitting an announcement to the newsletter can be found at http://lics.siglog.org/newsletters/inst.html ******************************************************************* TABLE OF CONTENTS * LICS-RELATED NEWS CSL-LICS'14 * DEADLINES Forthcoming Deadlines * CALLS Kiel Declarative Programming Days 2013 - Call for Participation AVOCS 2013 - Call for Participation FroCoS 2013 - Last Call for Participation FMICS 2013 - Call for Participation FMCAD 2013 - Call for Participation ICFEM 2013 - Call for Participation SMC 2014 - Preliminary Announcement CIE 2014 - Preliminary Announcement STACS 2014 - Call for Papers FLOC 2014 - Call for Workshops LIX Colloquium - Call for Abstracts and Participation ETAPS 2014 - Call for Papers IWIL 2013 - Call for Contributions ISAIM 2014 - Call for Papers FVHMS 2014 - Call for Papers RAMiCS 2014 - Call for Papers I&C ICC - Call for Papers FM 2014 - Call for Papers, Workshops and DOC Symposium NASA FM SYMPOSIUM - Call for Papers FLOPS 2014 - Call for Papers QAPL 2014 - Call for Papers EAPLS PHD AWARD 2012 - Call for Nominations * JOB ANNOUNCEMENTS Assistant Professor (UD) Position in Logic at ILLC, Amsterdam Assistant/Associate Professors at DTU Postdoctoral Scholar Positions in Secure and Dependable Systems at Idaho Postdoc in SMT Techniques at Trento 11 PhD Scholarships in Computer Science at Verona CSL-LICS'14 * Next year LICS and CSL will hold a joint conference for the first time, as part of FLoC 2014. Tom Henzinger and Dale Miller are co-chairs of a joint PC of 38 members. The proceedings will be published by IEEE. A preliminary Call for Papers is available on the LICS website. http://lics.siglog.org/csl-lics14/ DEADLINES * STACS 2014 Paper submission: September 20, 2013 http://stacs2014.sciencesconf.org/ * FLOC 2014 Workshop proposal submission: September 30, 2013 http://vsl2014.at/floc-ws/ * LIX Colloquium Abstract submission deadline: October 1, 2013 http://www.lix.polytechnique.fr/colloquium2013/ * ETAPS 2014 Submission deadline (abstracts): October 4, 2013 Submission deadline (full papers): October 11, 2013 http://www.etaps.org/2014 * IWIL 2013 Submission of papers/abstracts: October 14, 2013 http://www.eprover.org/EVENTS/IWIL-2013.html * ISAIM 2014 Paper submission: October 15, 2013 http://www.cs.uic.edu/Isaim2014/ * FVHMS 2014 Submission deadline: October 18, 2013 http://faculty.cs.byu.edu/~mike/mikeg/WORKSHOP/ * RAMiCS 2014 Title and abstract submission: October 25, 2013 Submission of full papers: November 1, 2013 http://mathcs.chapman.edu/ramics2014 * INFORMATION AND COMPUTATION SPECIAL ISSUE ON ICC Submission deadline: November 1, 2013 http://dice2013.di.unito.it/ * FM 2014 Abstract due: November 7, 2013 Full papers due: November 14, 2013 http://www.comp.nus.edu.sg/~pat/FM2014/ * NASA Formal Methods Symposium Abstract Submission: November 14, 2013 Paper Submission: November 21, 2013 http://www.NASAFormalMethods.org/ * FLOPS 2014 Submission deadline: December 13, 2013 http://www.jaist.ac.jp/flops2014/ * QAPL 2014 Abstract (optional): December 24, 2013 Submission (regular paper): December 31, 2013 http://qapl14.inria.fr * EAPLS PhD AWARD 2012 Nomination deadline: December 31, 2013 http://eapls.org/pages/phd_award/ KIEL DECLARATIVE PROGRAMMING DAYS 2013 Call for Participation September 11-13, 2013 Kiel, Germany http://www-ps.informatik.uni-kiel.de/kdpd2013/ * EVENT The Kiel Declarative Programming Days 2013 unifies the following events: - 20th International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2013, http://www.dcc.fc.up.pt/INAP-2013/) - 22nd International Workshop on Functional and (Constraint) Logic Programming (WFLP 2013, http://www-ps.informatik.uni-kiel.de/wflp2013/) -27th Workshop on Logic Programming (WLP 2013, http://www-ps.informatik.uni-kiel.de/wflp2013/) All events will be jointly organized. Look at the web sites about detailed registration, accommodation, and travel information. 13TH AUTOMATED VERIFICATION OF CRITICAL SYSTEMS WORKSHOP (AVOCS 13) 11-13th September, 2013 University of Surrey, UK http://www.avocs2013.org.uk * REGISTRATION Registration via the conference website: Regular £220, PhD £170 * INVITED SPEAKERS - Marcio Roveri, Senior Researcher Fondazione Bruno Kessler, Italy. His talk will be on software model checking with explicit scheduler and symbolic threads. The talk will refer to the software model checker Kratos and its use in the railway domain. - Alessio Lomuscio, Professor in logic for multi-agent systems in the Department of Computing, Imperial College London. His talk will be on verification of multi-agent systems via model checking. - Sofia Guerra, Adelard. Partner in Adelard and responsible for Adelard¹s Quality Assurance System. Her industrial talk will be on software assessment of smart sensors. * PRESENTATIONS We have 14 regular papers and 2 short papers. Details of the programme are on the website. * OBJECTIVES OF WORKSHOP The aim of Automated Verification of Critical Systems (AVoCS) 2013 is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, business-critical, performance-critical, etc.). The workshop will be relatively informal, with an emphasis on discussion. * PC CHAIRS Steve Schneider (University of Surrey, UK, Co-Chair) Helen Treharne (University of Surrey, UK, Co-Chair) 9TH INTERNATIONAL SYMPOSIUM ON FRONTIERS OF COMBINING SYSTEMS (FROCOS 2013) Last Call for Participation Nancy, France September 18-20, 2013 http://frocos2013.loria.fr/ Co-located with TABLEAUX 2013 * ONLINE REGISTRATION Visit http://frocos2013.loria.fr/registration.html Please note the reduced fees for the joint registration FroCoS+TABLEAUX. Please refer to the conference website for registration, accommodation and travel information. * GENERAL INFORMATION The 9th International Symposium on Frontiers of Combining Systems will be held in Nancy, France, from 18-20 September 2013. The aim of the conference is to publish and promote progress in research areas requiring the development of general techniques and methods for the combination and integration of special, formally defined systems, as well as for the analysis and modularization of complex systems. * PROGRAMME The conferences features 4 invited talks and 20 contributed papers. The full programme is available at the conference website. * INVITED TALKS - Stephane Demri, New York University & LSV, CNRS Counter Systems: The Quest for Pushing the Decidability Borders (joint invited talk with TABLEAUX 2013) - Konstantin Korovin, The University of Manchester From Resolution and DPLL to Solving Arithmetic Constraints - Joel Ouaknine, University of Oxford Specification and Verification of Linear Dynamical Systems: Advances and Challenges - Lawrence C. Paulson, University of Cambridge MetiTarski's Menagerie of Cooperating Systems * CO-LOCATED EVENT FroCoS 2013 will be co-located with the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013) held 16-19 September 2013. Participation in the TABLEAUX sessions is open to FroCoS participants on the overlapping days. There is also an attractive option for joint registration to both FroCoS and TABLEAUX. * IMPORTANT DATES 16-19 Sep 2013 Tableaux Conference 18-20 Sep 2013 FroCoS Conference * ORGANIZATION - Pascal Fontaine (PC Co-Chair), LORIA, INRIA, University of Lorraine, France - Christophe Ringeissen (Conference Chair), LORIA, INRIA, France - Renate Schmidt (PC Co-Chair), The University of Manchester, UK 18TH INTERNATIONAL WORKSHOP ON FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2013) Call for Participation September 23-24, 2013 Madrid (Spain) Co-located with SEFM 2013 http://lvl.info.ucl.ac.be/Fmics2013 * INVITED TALKS - Alessandro Fantechi (Universit à degli Studi di Firenze): Twenty-Five Years of Formal Methods and Railways: What Next? - Benjamin Monate (TrustInSoft): TrustInSoft: Industrial Formal Methods to Protect Security-Sensitive Systems * SCOPE The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS workshop series also strives to promote research and development for the improvement of formal methods and tools for industrial applications. * REGISTRATION Registration proceeds via the SEFM conference http://madrid.nethotels.com/mice/english/sefm_2013 INTERNATIONAL CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2013) Call for Participation October 20-23, 2013 Portland, Oregon, USA http://www.fmcad.org/FMCAD13 * VENUE University Place Hotel and Conference Center 310 SW Lincoln St. Portland, Oregon 97201. USA * OVERVIEW FMCAD 2013 is the thirteenth in a series of conferences on the theory and application of formal methods in hardware and system design and verification. FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing novel methods, technologies, theoretical results, and tools for formal reasoning about computing systems, as well as open challenges therein. FMCAD 2013 is co-located with MEMOCODE 2013, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, and DIFTS 2013, the International Workshop on Design and Implementation of Formal Tools and Systems. DIFTS will be held on October 19. MEMOCODE will take place from October 18 to 19, followed by a joint FMCAD/MEMOCODE tutorial day on October 20. FMCAD will continue from October 21 to 23, 2013. * REGISTRATION Early Registration Deadline: September 30, 2013 Registration details are available from the conference Web page. See URL http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/registration.shtml. In addition to traditional full-conference (student and regular) registrations with discounts for ACM/IEEE members, FMCAD provides discounted registration to participants who register for FMCAD and DIFTS together. FMCAD also provides single-day registrations for participants who are already registered full-conference for MEMOCODE during the early registration period (no late single-day registration available). Furthermore, note that MEMOCODE provides single-day registration to MEMOCODE for full-conference registrants of FMCAD. * TECHNICAL PROGRAM The technical program is available at the conference Web page. It includes 2 invited keynotes, 4 invited tutorials (jointly with MEMOCODE 2013), 23 regular papers, 7 short papers, a special session for Student Forum, and a panel. * KEYNOTES - Pranav Ashar, Chief Technology Officer, Real Intent, "Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC" - Lori A. Clarke, Professor, University of Massachusetts, Amherst, "Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare" * TUTORIALS - Rajeev Alur, University of Pennsylvania: "Syntax-Guided Synthesis" - Nate Foster, Mark Reitblatt, Cole Schlesinger (Cornell University), and Arjun Guha (University of Massachussetts, Amherst): "Network Programming in Frenetic" - Jim Grundy, Intel Corporation: "Firmware Validation: Challenges and Opportunities" - Somesh Jha, Bill Harris, Tom Reps, University of Wisconsin-Madison: "Secure Programs via Game-Based Synthesis" * STUDENT FORUM FMCAD 2013 will feature a Student Forum that provides a platform for graduate students at any career stage to introduce their research to the wider Formal Methods community, and solicit feedback on it. The event will consist of 14 short presentation by student authors (selected from among 29 submissions), together with a poster corresponding to each presented topic that will be on display throughout the duration of the conference. All FMCAD participants are strongly encouraged to attend the student presentations and the subsequent poster session, and engage with the presenters throughout the duration of the conference. * VENUE The conference will be held at the University Place Hotel and Conference Center, Portland, Oregon. We have negotiated a special rate with the hotel for conference attendees, under group name "FMCAD". Please book early to secure the reduced rate. Please submit your individual reservation requests directly to the hotel, either by phone at +1-866-845-4647, or via an email to Bich-Hahn Le at bichhahn@pdx.edu The banquet will be held in Portland City Grill. For details, please see the conference web page. * CO-LOCATED EVENTS - MEMOCODE, the ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2013). See http://memocode.irisa.fr/2013/ - DIFTS, International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS 2013). See http://www.cmpe.boun.edu.tr/difts13/ - HWMCC, Hardware Model Checking Competition (HWMCC'13). See http://fmv.jku.at/hwmcc13/ * SPONSORS - Sponsored by: FMCAD, Inc. - Technical Co-sponsor: IEEE CEDA - In-cooperation with: ACM SIGDA - Industrial Financial Support: Galois, IBM, Intel, Jasper, Mentor Graphics, Microsoft, NEC, NVIDIA, Onespin Solutions, Oski Technology, Real Intent, Synopsys, Xpliant 15TH INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS (ICFEM 2013) Queenstown, New Zealand 29 October - 1 November 2013 http://www.cs.auckland.ac.nz/icfem2013/ * GENERAL The 15th International Conference on Formal Engineering Methods (ICFEM 2013) will be held at the Crowne Plaza Hotel in Queenstown, New Zealand from 29 October to 1 November 2013. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been dedicated to applying formal methods to practical computer systems. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, and to help advance the state of the art. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM 2013 is organized and sponsored by The University of Auckland and will be held in the world renowned travel destination - Queenstown. Around 1.9 million visitors are drawn to Queenstown each year to enjoy their own unforgettable travel experience. We are looking forward to your submissions and participation. * GENERAL CHAIRS Jin Song Dong, National University of Singapore, Singapore. Ian Hayes, The University of Queensland, Australia. Steve Reeves, The University of Waikato, New Zealand. * PC CHAIRS Lindsay Groves, Victoria University of Wellington, New Zealand. Jing Sun, The University of Auckland, New Zealand. * WORKSHOP AND TUTORIAL CHAIRS Yang Liu, Nanyang Technological University, Singapore. Jun Sun, Singapore University of Technology and Design, Singapore. * LOCAL ORGANIZATION CHAIR Gillian Dobbie, The University of Auckland, New Zealand. MATHEMATICAL STRUCTURES OF COMPUTATION (SMC 2014) Preliminary announcement January 13 - February 14 2014, Lyon, France http://smc2014.univ-lyon1.fr * We are pleased to announce the programme "Mathematical Structures of Computation" organised in Lyon, from January 13th to February 14th, 2014. * The programme proposes five consecutive workshops - Recent Developments in Type Theory, January 13-17. - Algebra and Computation, January 20-24. - Directed Algebraic Topology and Concurrency, January 27-31. - Formal Proof, Symbolic Computation and Computer Arithmetic, February 3-7. - Concurrency, Logic and Types, February 10-14. * Information on the programme can be found at http://smc2014.univ-lyon1.fr * Registration for the programme is free and will open in early September 2013. * The weeks Mathematical Structures of Computation are organised in Lyon with the support of the Labex MILYON - Mathematics and fundamental computer science in Lyon. Together with the trimester Semantics of proofs and certified mathematics organised at Institut Henri Poincare, Paris, (http://ihp2014.pps.univ-paris-diderot.fr) they constitute a French Semester on certified mathematics, programming languages and the mathematical structures of computation. * The organisers: Patrick Baillot, Yves Guiraud, Philippe Malbos. COMPUTABILITY IN EUROPE 2014: LANGUAGE, LIFE, LIMITS (CiE 2014) Preliminary Announcement Budapest, Hungary June 23 - 27, 2014 http://www.illc.uva.nl/CiE/index.php?page=22_8 * SCOPE CiE 2014 is the tenth conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world. Previous meetings have taken place in Amsterdam (2005), Swansea (2006), Siena (2007), Athens (2008), Heidelberg (2009), Ponte Dalgada (2010), Sofia (2011), Cambridge (2012), and Milan (2013). Please mark the conference dates in your agendas for 2014. * CONFIRMED TUTORIAL SPEAKER Wolfgang Thomas (RWTH Aachen) * CONFIRMED INVITED SPEAKERS Alessandra Carbone (Universite Pierre et Marie Curie and CNRS Paris) Maribel Fernandez (King's College London) Przemyslaw Prusinkiewicz (University of Calgary) Eva Tardos (Cornell University) Albert Visser (Utrecht University) * SPECIAL SESSIONS History and Philosophy of Computing organizers: Liesbeth de Mol, Giuseppe Primiero Computational Linguistics organizers: Maria Dolores Jimenez-Lopez, Gabor Proszeky Computability Theory organizers: Karen Lange, TBA Bio-inspired Computation organizers: Marian Gheorghe, Florin Manea Online Algorithms organizers: Joan Boyar, Csanad Imreh Complexity in Automata Theory organizers: Markus Lohrey, Giovanni Pighizzini * MOTTO The motto of CiE 2014 "Language, Life, Limits" intends to put a special focus on relations between computational linguistics, natural computing, and more traditional fields of computability theory. This is to be understood in its broadest sense including computational aspects of problems in linguistics, studying models of computation and algorithms inspired by physical and biological approaches as well as exhibiting limits (and non-limits) of computability when considering different models of computation arising from such approaches. As with previous CiE conferences, the allover glueing perspective is to strengthen the mutual benefits of analyzing traditional and new computational paradigms in their corresponding frameworks both with respect to practical applications and a deeper theoretical understanding. The conference will address these aspects besides the more established lines of research of Computational Complexity and the interplay between Proof Theory and Computation. Novel views that rely on physical and biological processes and models to find new ways of tackling computations and improving their efficiency are welcome. Also, massive data analysis and computations are a recent subject of attention, since the most recent technologies produce huge amounts of data, and managing such data requires some theoretical frameworks. In all cases we are looking for fundamental and theoretical submissions. In line with other conferences in this series, CiE 2014 has a broad scope and provides a forum for the discussion of theoretical and practical issues in Computability with an emphasis on new paradigms of computation and the development of their mathematical theory. We particularly invite papers that build bridges between different parts of the research community. * CALL In a Call for Papers to be sent out in October 2013, the PC will invite all researchers in the area of the conference to submit their papers for presentation at CiE 2014. The best of the accepted papers will be published in the conference proceedings within the Lecture Notes in Computer Science (LNCS) series of Springer, which will be available at the conference. 31ST INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2014) Call for Papers March 5 - March 8, 2014, Lyon, France Submission Deadline: Sep 20, 2013 (23:59:59 GMT/UTC) http://stacs2014.sciencesconf.org/ * SUBMISSIONS Authors are invited to submit papers presenting original and unpublished research on theoretical aspects of computer science. Typical areas include (but are not limited to): - algorithms and data structures, including: parallel, distributed, approximation, and randomized algorithms, computational geometry, cryptography, algorithmic learning theory, analysis of algorithms; - automata and formal languages, games; - computational complexity, parameterized complexity, randomness in computation; - logic in computer science, including: semantics, specification and verification, rewriting and deduction; - current challenges, for example: natural computing, quantum computing, mobile and net computing. * INVITED SPEAKERS - Javier Esparza, TUM - Technische Universitaet Muenchen - Peter Bro Miltersen, Aarhus University - Luc Segoufin, INRIA, Ecole Normale Superieure de Cachan * TUTORIAL Neeraj Kayal, Microsoft Research India: Arithmetic Circuit Complexity THE SIXTH FEDERATED LOGIC CONFERENCE (FLoC 2014) Call for Workshops Part of VIENNA SUMMER OF LOGIC (VSL 2014) July 2014, Vienna, Austria * FLOC 2014 The Sixth Federated Logic Conference (FLoC 2014) will be part of the Vienna Summer of Logic (VSL), the largest logic event in history, with over 2000 expected participants. FLoC 2014 will host eight conferences and many workshops. Each workshop will be affiliated with at least one of the eight conferences. - 26th International Conference on Computer Aided Verification (CAV) Workshop Chair: Martina Seidl http://fmv.jku.at/seidl/ - 27th IEEE Computer Security Foundations Symposium (CSF) Workshop Chair: Luca Vigano http://profs.sci.univr.it/~vigano/ - 30th International Conference on Logic Programming (ICLP) Workshop Chair: Haifeng Guo http://faculty.ist.unomaha.edu/hguo/ - 7th International Joint Conference on Automated Reasoning (IJCAR) Workshop Chair: Matthias Horbach http://www.mpi-inf.mpg.de/~horbach/ - 5th Conference on Interactive Theorem Proving (ITP) Workshop Chair: David Pichardie http://www.irisa.fr/celtique/pichardie/ - Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th ACM/IEEE Symposium on Logic in Computer Science (LICS) Workshop Chairs: Patricia Bouyer-Decitre http://www.lsv.ens-cachan.fr/~bouyer/ Georg Moser http://cl-informatik.uibk.ac.at/users/georg/ - 25th International Conference on Rewriting Techniques and Applications (RTA) joined with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA) Workshop Chair: Aleksy Schubert http://www.mimuw.edu.pl/~alx/ - 17th International Conference on Theory and Applications of Satisfiability Testing (SAT) Workshop Chair: Ines Lynce http://sat.inesc-id.pt/~ines/ * SUBMISSION OF WORKSHOP PROPOSALS Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense. Each workshop proposal must indicate at least one conference to be affiliated with, and among those exactly one primary hosting conference. It is suggested that prospective workshop organizers contact the relevant conference Workshop Chair(s) before submitting a proposal. Proposals should be submitted electronically to EasyChair at the following address: http://www.easychair.org/conferences/?conf=floc14cfw Proposals should consist of two parts. First, a short scientific justification of the proposed topic, its significance, and the particular benefits of the workshop to the community, as well as a list of previous or related workshops (if relevant). A second, organizational part should include: - contact information of the workshop organizers - proposed primary hosting conference (and possibly other affiliated conference(s)) - estimate of the audience size - proposed format and agenda (for example, paper presentations, tutorials, demo sessions, etc.) - potential invited speakers - procedures for selecting papers and participants - plans for dissemination, if any (for example, special issues of journals) - duration (which may vary from one day to two days) and preferred period The FLoC Organizing Committee will determine the final list of accepted workshops based on the recommendations from the Workshop Chairs of the hosting conferences and subject to the availability of space and facilities. * FURTHER INFORMATION See the FLoC 2014 Workshop Guide http://vsl2014.at/floc-ws/ * IMPORTANT DATES Submission of workshop proposals: by September 30, 2013 Notification: by November, 2013 Pre-FLoC workshops: Saturday & Sunday, July 12-13 Mid-FLoC workshops: Thursday & Friday, July 17-18 Post-FLoC workshops: Wednesday & Thursday, July 23-24 * CONTACT INFORMATION Questions regarding workshop proposals should be sent to the workshop chairs of conferences that are supposed to host the workshop (see above). General questions should be sent to floc14cfw@easychair.org Please consult the FLoC 2014 Workshop Guide http://vsl2014.at/floc-ws/ * FLoC 2014 WORKSHOP CHAIR Stefan Szeider http://www.szeider.net Vienna University of Technology LIX COLLOQUIUM ON THE THEORY AND APPLICATION OF FORMAL PROOFS http://www.lix.polytechnique.fr/colloquium2013/ 5-7 November 2013 Ecole Polytechnique, Palaiseau, France In association with: PSATTT, 8 Nov 2013. * EVENTS This three-day colloquium will be composed of a number of hour long talks by invited speakers and 30 minute talks based on contributed abstracts. It is meant as a venue for the exchange of ideas. No proceedings are planned apart from a simple collection of short abstracts of all talks. The colloquium will be followed by the workshop: Proof Search in Axiomatic Theories and Type Theories (PSATTT) 2013. * THEME Formal proofs are becoming increasingly important in a number of domains in computer science and mathematics. The topic of the colloquium is structural proof theory, broadly construed. The following are some examples of relevant topics: - STRUCTURE OF PROOFS sequential and parallel structures in proofs; sharing and duplication of subproofs; permutations of proof steps; canonical forms; focusing and polarities; graphical proof syntax; proof complexity - CHECKING PROOFS generating, transmitting, translating, and checking proof objects; universal proof languages; proof certificates; proof compression; cut-introduction; certification of high-performance systems (SMT, resolution, etc.) - PROOF SEARCH automated and interactive proof search in constrained logics (linear, temporal, bunched, probabilistic, etc.); combining deduction and computation in search; reasoning about inductive and co-inductive fixpoints; cyclic proofs; computational interpretations of proof search - COMPUTING WITH PROOFS cut-elimination strategies; cut-elimination by resolution (CERes); Curry-Howard correspondence These lists are not exhaustive. * INVITED SPEAKERS Chad E. Brown, Saarland University Agata Ciabattoni, TU Vienna David Delahaye, CNAM, invited by PSATTT Alessio Guglielmi, University of Bath Dominic Hughes, Stanford University Sara Negri, University of Helsinki Claudio Sacerdoti Coen, University of Bologna Alex Simpson, University of Edinburgh [More to be confirmed] * CALL FOR ABSTRACTS AND PARTICIPATION The colloquium is free and open to all, but registration is requested. If you would like to attend, please send a mail to Kaustuv Chaudhuri. If you would like to contribute a 30 minute presentation related to the themes of the colloquium, please submit a 1-2 page abstract (as PDF) via EasyChair at https://www.easychair.org/conferences/?conf=tafp2013 The deadline for submissions is 1 October 2013. Decisions on submissions will be made before 8 October 2013. * VENUE The colloquium and the PSATTT workshop will take place in the Laboratoire d'Informatique (LIX) of the Ecole Polytechnique. The Polytechnique is situated in the southern suburbs of Paris, about 40 minutes from central Paris by regional train. LIX is co-located with INRIA Saclay. * ORGANIZERS Dale Miller, Lutz Strassburger, Stephane Graham-Lengrand, Assia Mahboubi, Kaustuv Chaudhuri * SUPPORT - Laboratoire d’Informatique (LIX) of the Ecole Polytechnique http://www.lix.polytechnique.fr/ - ERC Advanced Grant ProofCert https://team.inria.fr/parsifal/proofcert/ * SEE ALSO - PSATTT Workshop 2013 http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT13/ - Travelling to LIX/Ecole Polytechnique https://team.inria.fr/parsifal/meetings/directions/ 17TH EUROPEAN JOINT CONFERENCES ON THEORY AND PRACTICE OF SOFTWARE (ETAPS 2014) Call for Papers Grenoble, France 5-13 April 2014 http://www.etaps.org/2014 * ABOUT ETAPS ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of six main annual conferences, accompanied by satellite workshops. ETAPS 2014 is the seventeenth event in the series. * MAIN CONFERENCES (7-11 April) - CC: Compiler Construction - ESOP: European Symposium on Programming - FASE: Fundamental Approaches to Software Engineering - FOSSACS: Foundations of Software Science and Computation Structures - POST: Principles of Security and Trust - TACAS: Tools and Algorithms for the Construction and Analysis of Systems TACAS '14 hosts the 3rd Competition on Software Verification (SV-COMP). * INVITED SPEAKERS - Robert Harper (Carnegie Mellon University, US) - John Launchbury (Galois, US) - Benoit Dupont de Dinechin (Kalray, France) - Maurice Herlihy (Brown University, US) - Christel Baier (Technical University of Dresden, Germany) - Petr Jancar (Technical Univ of Ostrava, Czech Republic) - David Mazieres (Stanford University, US) - Orna Kupferman (Hebrew University Jerusalem, Israel) * IMPORTANT DATES - 4 October 2013: Submission deadline for abstracts (strict) - 11 October 2013: Submission deadline for full papers (strict) - 20 December 2013: Notification of acceptance - 17 January 2014: Camera-ready versions due ESOP and FoSSaCS will use a rebuttal (author response) phase. * GENERAL SUBMISSION INFORMATION ETAPS conferences accept two types of contributions: research papers and tool demonstration papers. Both types will appear in the proceedings and have presentations during the conference. (TACAS has more categories, see below.) A condition of submission is that, if the submission is accepted, one of the authors attends the conference to give the presentation. Submitted papers must be in English presenting original research. They must be unpublished and not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of Springer's Lecture Notes in Computer Science series. Papers must follow the formatting guidelines specified by Springer at the URL http://www.springer.de/comp/lncs/authors.html and be submitted electronically in pdf through the Easychair author interface of the respective conference. Submissions not adhering to the specified format and length may be rejected immediately. * RESEARCH PAPERS Different ETAPS 2014 conferences have different page limits. Specifically, FASE, FOSSACS and TACAS have a page limit of 15 pages, whereas CC, ESOP and POST allow at most 20 pages. Additional material intended for the referees but not for publication in the final version - for example, details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. ETAPS referees are at liberty to ignore appendices and papers must be understandable without them. TACAS solicits not only regular research papers, but also case study papers. * TOOL DEMONSTRATION PAPERS Submissions should consist of two parts: - The first part, at most 4 pages, should describe the tool presented. Please include the URL of the tool (if available) and provide information that illustrates the maturity and robustness of the tool. (This part will be included in the proceedings.) - The second part, at most 6 pages, should explain how the demonstration will be carried out and what it will show, including screen dumps and examples. (This part will be not be included in the proceedings, but will be evaluated.) ESOP and FOSSACS do not accept tool demonstration papers. In addition to tool demonstration papers (max 6 pages in their case), TACAS solicits also regular tool papers (max 15 pages) adhering to specific instructions about content and organization. * SATELLITE EVENTS (5-6 April, 12-13 April) Around 20 satellite workshops will take place before and after the main conferences. In addition, on 6 April, some tutorials on topics of wide interest will be offered. * HOST CITY Located in the southeastern part of France, Grenoble is considered as the capital of the Alps. Grenoble is surrounded by nature and high mountains: down the Alps, Grenoble is the meeting point of two important rivers, Drac and Isere. Grenoble has important historical and gastronomic heritages. Leisure activities in breathtaking nature are easily organizable and within short-distance. Grenoble is also a major scientific center in Europe dedicated to high-tech technologies, e.g., nano, micro, bio, and information technologies. * HOST INSTITUTION The event is organized by Universite Joseph Fourier. Located at the heart of the Alps, in outstanding scientific and natural surroundings, the Universite Joseph Fourier in Grenoble is a leading University of Science, Technology and Health. * ORGANIZERS - General chair: Saddek Bensalem - Conferences chair: Yassine Lakhnech - Workshops chair: Axel Legay - Publicity chair: Ylies Falcone - Finance chair: Nicolas Halbwachs - Web site chair: Marius Bozga * FURTHER INFORMATION Please do not hesitate to contact the organizers at etaps2014.organization@imag.fr. 10TH INTERNATIONAL WORKSHOP ON THE IMPLEMENTATION OF LOGICS (IWIL 2013) Call for Contributions December 14th, 2013 Stellenbosch, South Africa http://www.eprover.org/EVENTS/IWIL-2013.html * The 10th International Workshop on the Implementation of Logics will be held on December 14th, 2013, colocated with the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning in Stellenbosch, South Africa. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, and non-monotonic logics + Formal foundations for efficient implementation of logics + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Practical constraint handling + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. * CONTRIBUTIONS Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full papers (up to 15 pages). Submissions should be made via EasyChair at http://www.easychair.org/conferences/?conf=iwil2012 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. Proceedings will be published as EasyChair Proceedings. If number and quality of the submissions warrant it, we plan to produce a special issue of a recognized journal on the topic of the workshop. * IMPORTANT DATES Submission of papers/abstracts: October 14th, 2013 Notification of acceptance: November 11th, 2013 Camera ready versions due: December 2nd, 2013 Workshop: December 14th, 2013 * CHAIRS Stephan Schulz (Co-Chair) TU Muenchen Geoff Sutcliffe (Co-Chair) University of Miami Boris Konev (Co-Chair) University of Liverpool 13TH INTERNATIONAL SYMPOSIUM ON ARTIFICIAL INTELLIGENCE AND MATHEMATICS (ISAIM 2014) Call for Papers January 6-8, 2014, Fort Lauderdale FL, USA http://www.cs.uic.edu/Isaim2014/ * The International Symposium on Artificial Intelligence and Mathematics (ISAIM) is a biennial meeting that fosters interactions between mathematics, theoretical computer science, and artificial intelligence. This is the thirteenth Symposium in the series, which is sponsored by Annals of Mathematics and Artificial Intelligence. We seek submissions of recent results with particular emphasis on the foundations of AI and mathematical methods used in AI. Papers describing applications are also encouraged, but the focus should be on principled lessons learned from the development of the application. Traditionally, the Symposium attracts participants from a variety of disciplines, thereby providing a unique forum for scientific exchange. The three-day Symposium includes invited speakers, presentations of technical papers, and special topic sessions. * Special Topic Invited Sessions: - Boolean and pseudo-Boolean Functions, organized by Endre Boros, Rutgers University, and Yves Crama, University of Liège - Mathematical Theories of Natural Language Processing, organized by András Kornai, Hungarian Academy of Sciences - Theory of Machine Learning, organized by Lev Reyzin, University of Illinois at Chicago - Proposals for organizing additional special sessions can be sent to the chairs for consideration by September 15, 2013 * Important Dates: - Paper submission: October 15, 2013 - Notification: November 15, 2013 - Final version due: December 15, 2013 - Workshop: January 6-8, 2014, Ft. Lauderdale, Florida * Send inquiries and requests to isaim2014 at cs DOT uic DOT edu. * Visit http://www.cs.uic.edu/Isaim2014/. * Join isaim@googlegroups.com to receive announcements related to ISAIM. FORMAL VERIFICATION AND MODELING IN HUMAN-MACHINE SYSTEMS (AAAI 2014 SPRING SYMPOSIUM, FVHMS 2014) Call for Papers March 24-26, 2014 Palo Alto, USA http://faculty.cs.byu.edu/~mike/mikeg/WORKSHOP/ * OVERVIEW The goal of the workshop is to bring together the fields of formal verification, cognitive modeling, and task analysis to study the design and verification of real human-machine systems. Recent papers in each of these communities discuss modeling challenges and the application of basic formal verification in human-machine interaction; however, there is little communication between researchers in these different areas and there are many open questions that require cross-disciplinary collaboration. The workshop is to bring together experts from many communities in an environment where it is possible to explore key research areas, common solutions, near-term research problems, and advantages in combining the best of the different communities. * SUBMISSIONS We solicit papers describing original work either in-progress or finished, position papers or extended abstracts describing research or positions. Papers should follow the AAAI formatting, with a page-limit of 6 pages. Proceedings of the symposium will be published by AAAI as a CD, distributed at the symposium. Selected papers will be invited to submit extended versions of their contributions for review in a follow-on special issue of the IEEE Transactions on Human-Machine Systems dedicated to the same topic. * TOPICS - What model classes, methodologies, and constructs are appropriate for modeling human and machine activities in a way that is amenable to formal verification? Examples include - Programming languages - State Machines - Activity models (e.g. Brahms) - Cognitive models (SOAR, ACT-R, DIARC, etc.) - Task analyses-based models (GDTA, CWA, etc.) - Probabilistic models - Behavioral game theory - What levels of abstraction are appropriate for such modeling, and what information is lost in using abstraction? - What are the contexts, if any, for which the trade offs between authority between humans, autonomy, and model-based reasoning can be specified? - What is the impact on design for including explicit (meta-) reasoning models in the human-machine interaction loop? - What types of model-checkers are appropriate, and what other lessons from formal verification apply to human-machine systems? - What are the ethical considerations of using verified models to allocate responsibility and authority between humans and machines? - What organizational structures are appropriate for human-machine collaborative work? + Master-slave + Teammates + Principal-agent - How can dynamic models evolve in the presence of learning agents, both human and machine, and in the presence of inaccurate mental models. * IMPORTANT DATES Oct 18, 2013: Submission deadline Dec 10, 2013: Notification of acceptance/rejection Jan 10, 2014: Camera-ready papers due Mar 1, 2014: Registration deadline March 24-26, 2014: Symposium * ORGANIZERS Michael Goodrich, Brigham Young University, USA Eric Mercer, Brigham Young University, USA Neha Rungta, NASA Ames Research Center, USA Ellen Bass, Drexel University, USA * INVITED SPEAKERS Amy Pritchett, Georgia Tech, USA Philippe Palanque, IRIT, University Paul Sabatier, France Christian Lebiere, CMU, USA 14TH INTERNATIONAL CONFERENCE ON RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMiCS 2014) Call for Papers 27 April - 1 May 2014 Marienstatt im Westerwald, Germany http://mathcs.chapman.edu/ramics2014 * SCOPE We invite submissions in the general area of Relational and Algebraic Methods in Computer Science. Special focus will lie on formal methods for software engineering, logics of programs and links with neighbouring disciplines. * HISTORY Since 1994, the RelMiCS meetings on Relational Methods in Computer Science have been a main forum for researchers who use the calculus of relations and similar algebraic formalisms as methodological and conceptual tools. The AKA workshop series on Applications of Kleene algebra started with a Dagstuhl seminar in 2001 and was co-organised with the RelMiCS conference until 2009. Since 2011, joint RAMiCS conferences continue to encompass the scope of both RelMiCS and AKA. * STUDENT PROGRAM The conference will be accompanied by a PhD training program. Details will be published in due time in a special call and on the conference website. * PROCEEDINGS AND SUBMISSION All papers will be formally reviewed. We plan to publish the proceedings in the series Lecture Notes in Computer Science ready at the conference. Submissions must be in English, in Postscript or PDF format, and provide sufficient information to judge their merits. They must be unpublished and not submitted for publication elsewhere. Submission is via EasyChair at the following address: https://www.easychair.org/conferences/?conf=ramics2014 * IMPORTANT DATES Title and abstract submission: October 25, 2013 Submission of full papers: November 1, 2013 Notification: December 13, 2014 Final versions due (firm deadline): January 17, 2014 Conference April 27 - May 1, 2014 INFORMATION & COMPUTATION SPECIAL ISSUE ON IMPLICIT COMPUTATIONAL COMPLEXITY Call for Papers http://dice2013.di.unito.it * GUEST EDITORS Simona Ronchi Della Rocca (ronchi@di.unito.it) Virgile Mogbil (virgile.mogbil@lipn.univ-paris13.fr) * DATES Deadline: November 1st 2013 Notification: May 15th 2013 * SCOPE The area of Implicit Computational Complexity (ICC) has grown out from several proposals to use logic and formal methods to delineate complexity-bounded computation (e.g. polynomial time, polynomial space or logspace computation). It aims at studying computational complexity without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical/computational principles implying complexity properties. * TOPICS Contributions on various aspects of ICC including (but not exclusively) are welcome : - types for controlling complexity, - logical systems for implicit computational complexity, - linear logic, - semantics of complexity-bounded computation, - complexity analysis, - rewriting and termination orderings, - interpretation-based methods for implicit complexity, - programming languages for complexity bounded computation, - application of implicit complexity to other programming paradigms (e.g. imperative or object-oriented languages). This post-conference publication of DICE 2013 (http://dice2013.di.unito.it/) is open to everyone, also those who did not participate in the conference. It follows a series of annual workshop as satellite events of ETAPS : DICE 2010 in Paphos, DICE 2011 in Saarbrucken, DICE 2012 in Tallinn and DICE 2013 in Rome. * SUBMISSIONS Submissions must be sent to us no later than NOVEMBER 1st 2013. Papers will be processed as soon as they are submitted. I&C solicits high quality papers reporting research results related to the topics mentioned above. All papers must be original, unpublished, and not submitted for publication elsewhere. Contributions should be submitted electronically as PDF, using Elsevier's elsarticle.cls latex macro package, that can be retrieved from http://www.elsevier.com/wps/find/authorsview.authors/elsarticle We encourage authors to look at http://www.elsevier.com/journals/information-and-computation/0890-5401/guide-for-authors * ADDITIONAL INFORMATION See http://dice2013.di.unito.it/ or email inquiries to us (ronchi@di.unito.it or virgile.mogbil@lipn.univ-paris13.fr) 19TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS (FM 2014) Call for Papers/Workshops/DOC Symposium Singapore, May 14-16, 2014 http://www.comp.nus.edu.sg/~pat/FM2014/ * SERIES FM 2014 is the nineteenth in a series of symposia organized by Formal Methods Europe, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The symposia have been notably successful in bringing together innovators and practitioners in precise mathematical methods for software and systems development, industrial users, as well as researchers. Submissions are welcomed in the form of original papers on research and industrial experience, proposals for workshops and tutorials, entries for the exhibition of software tools and projects, and reports on ongoing doctoral work. * SCOPE AND TOPICS It will have the goal of highlighting the development and application of formal methods in connection with a variety of disciplines such as medicine, biology, human cognitive modeling, human automation interactions and aeronautics, among others. FM 2014 particularly welcomes papers on techniques, tools and experiences in interdisciplinary frameworks, as well as on experience with practical applications of formal methods in industrial and research settings, experimental validation of tools and methods as well as construction and evolution of formal methods tools. The broad topics of interest for FM 2014 include but are not limited to: - Interdisciplinary formal methods: techniques, tools and experiences demonstrating formal methods in interdisciplinary frameworks. - Formal methods in practice: industrial applications of formal methods, experience with introducing formal methods in industry, tool usage reports, experiments with challenge problems. Authors are encouraged to explain how the use of formal methods has overcome problems, lead to improvements in design or provided new insights. - Tools for formal methods: advances in automated verification and model-checking, integration of tools, environments for formal methods, experimental validation of tools. Authors are encouraged to demonstrate empirically that the new tool or environment advances the state of the art. - Role of formal methods in software and systems engineering: development processes with formal methods, usage guidelines for formal methods, method integration. Authors are encouraged to demonstrate that process innovations lead to qualitative or quantitative improvements. - Theoretical foundations: all aspects of theory related to specification, verification, refinement, and static and dynamic analysis. Authors are encouraged to explain how their results contribute to the solution of practical problems. * PAPER SUBMISSION Papers will be evaluated by at least three members of the Program Committee. They should be in Springer LNCS format and describe, in English, original work that has not been published or submitted elsewhere. Papers should be submitted through the FM 2014 EasyChair web site at: http://www.easychair.org/conferences/?conf=fm2014 Accepted papers will be published in the Symposium Proceedings, to appear in Springer's Lecture Notes in Computer Science. * IMPORTANT DATES Abstract due: November 7, 2013 Full papers due: November 14, 2013 Acceptance / Rejection Notification: February 1, 2014 Industry Track Submission: January 16, 2014 Industry Track Notification: February 16, 2014 Camera-ready: February 25, 2014 Main Conference Date: May 14-16, 2014 Tutorial / Workshops Date: May 12-13, 2014 * CALL FOR TUTORIALS, WORKSHOPS and DOC SYMPOSIUM The organizing committee of FM 2014 thus invites proposals for half- or full-day tutorials in the broad area of formal methods. Proposals from industry practitioners or academics are very welcome; proposals for tutorials on applications of formal methods to challenging problems are particularly welcome. All tutorials should focus on providing participants with the opportunity to learn new techniques, new application domains, and insightful uses of formal methods. Details on the call for tutorials can be found at http://www.comp.nus.edu.sg/~pat/FM2014/cft.html We are also inviting people to submit proposals for workshops. The purpose of the workshops is to provide an informal setting for workshop participants to discuss technical issues, exchange research ideas, and to discuss and/or demonstrate applications. These workshops may be driven by fundamental academic interests or by needs from specific application domains. We encourage a diversity of workshops relating to different varieties of formal models. Details on the call for workshops can be found at http://www.comp.nus.edu.sg/~pat/FM2014/cfp4w.html * DOC SYMPOSIUM A Doctoral Symposium will be held on 12-13th May in conjunction with the FME Symposium FM2014. This aims to provide a helpful environment in which selected doctoral students can present and discuss their ongoing work, meet other students working on similar topics and receive helpful advice and feedback from a panel of researchers and academics. Details on the call for doctoral sympisum can be found at http://www.comp.nus.edu.sg/~pat/FM2014/cfd.html * GENERAL CHAIR Jin Song Dong, National University of Singapore, Singapore. * PC CHAIRS Cliff B Jones, Newcastle University, United Kindom. Pekka Pihlajasaari, Data Abstraction (Pty) Ltd, South Africa. Jun Sun, Singapore University of Technology and Design, Singapore. * DOC SYMPOSIUM Annabelle McIver, Macquarie University, Australia. * WORKSHOP CHAIR Shengchao Qin, University of Teesside, United Kindom. * TUTORIAL CHAIR Richard Paige, University of York, United Kindom. SIXTH NASA FORMAL METHODS SYMPOSIUM Call for Papers 29 April - 1 May 2014 NASA Johnson Space Center Houston, Texas, USA http://www.NASAFormalMethods.org/ * THEME The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in safety-critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages carrying throughout system development. * TOPICS - Model checking - Theorem proving - Static analysis - Model-based development - Runtime monitoring - Formal approaches to fault tolerance - Applications of formal methods to aerospace systems - Formal analysis of cyber-physical systems, including hybrid and embedded systems - Formal methods in systems engineering, modeling, requirements, and specifications - Requirements generation, specification debugging, formal validation of specifications - Use of formal methods in safety cases - Use of formal methods in human-machine interaction analysis - Formal methods for parallel hardware implementations - Use of formal methods in automated software engineering and testing - Correct-by-design, design for verification, and property-based design techniques - Techniques and algorithms for scaling formal methods; e.g. abstraction and symbolic methods, compositional techniques, parallel and distributed techniques - Application of formal methods to emerging technologies * IMPORTANT DATES Abstract Submission: 14 Nov 2013 Paper Submission: 21 Nov 2013 Paper Notifications: 14 Jan 2014 Camera-ready Papers: 11 Feb 2014 Symposium: 29 April - 1 May 2014 * LOCATION The symposium will take place at the Gilruth Center, NASA Johnson Space Center, Houston, Texas, USA, 29 April to 1 May 2013. There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to attend, to listen to the talks, and to participate in discussions; however, all attendees must register. * SUBMISSION DETAILS There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (15 pages) 2. Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results (6 pages) All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer's Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format. * KEYNOTES SPEAKERS - Larry Paulson, University of Cambridge, UK - Moshe Y. Vardi, Rice University, USA - Special Guest Talk: "NASA Future Challenges in Formal Methods" * ORGANIZERS Mike Hinchey (General Chair) Julia Badger (PC Chair) Kristin Yvonne Rozier (PC Chair) 12TH INTERNATIONAL SYMPOSIUM ON FUNCTIONAL AND LOGIC PROGRAMMING (FLOPS 2014) Call for Papers June 4-6, 2014 Kanazawa, Japan http://www.jaist.ac.jp/flops2014/ * GENERAL FLOPS is a forum for research on all issues concerning declarative programming, including functional programming and logic programming, and aims to promote cross-fertilization and integration between the two paradigms. Previous FLOPS meetings were held at Fuji Susono (1995), Shonan Village (1996), Kyoto (1998), Tsukuba (1999), Tokyo (2001), Aizu (2002), Nara (2004), Fuji Susono (2006), Ise (2008), Sendai (2010), and Kobe (2012). * TOPICS FLOPS solicits original papers in all areas of functional and logic programming, including (but not limited to): - Language issues: language design and constructs, programming methodology, integration of paradigms, interfacing with other languages, type systems, constraints, concurrency and distributed computing. - Foundations: logic and semantics, rewrite systems and narrowing, type theory, proof systems. - Implementation issues: compilation techniques, memory management, program analysis and transformation, partial evaluation, parallelism. - Applications: case studies, real-world applications, graphical user interfaces, Internet applications, XML, databases, formal methods and model checking. The proceedings will be published as an LNCS volume. The proceedings of the previous meetings (FLOPS 1999, 2001, 2002, 2004, 2006, 2008, 2010, and 2012) were published as LNCS 1722, 2024, 2441, 2998, 3945, 4989, 6009, and 7294. * PC CO-CHAIRS Michael Codish (Ben-Gurion University of the Negev) Eijiro Sumii (Tohoku University) * LOCAL CHAIR Yuki Chiba (JAIST) * SUBMISSION Submissions must be unpublished and not submitted for publication elsewhere. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. See also ACM SIGPLAN Republication Policy: http://www.sigplan.org/Resources/Policies/Republication Submissions should fall into one of the following categories: - Regular research papers: they should describe new results and will be judged on originality, correctness, and significance. - System descriptions: they should contain a link to a working system and will be judged on originality, usefulness, and design. - Declarative pearls: new and excellent declarative programs or theories with illustrative applications. System descriptions and declarative pearls must be explicitly marked as such in the title. * SUBMISSIONS Submissions must be written in English and can be up to 15 pages long including references, though pearls are typically shorter. Authors are required to use LaTeX2e and the Springer llncs class file, available at: http://www.springer.de/comp/lncs/authors.html Regular research papers should be supported by proofs and/or experimental results. In case of lack of space, this supporting information should be made accessible otherwise (e.g., a link to a Web page, or an appendix). Papers should be submitted electronically at: https://www.easychair.org/conferences/?conf=flops2014 * IMPORTANT DATES Submission deadline: December 13, 2013 Author notification: February 10, 2014 Camera-ready copy: March 7, 2014 12TH WORKSHOP ON QUANTITATIVE ASPECTS OF PROGRAMMING LANGUAGES AND SYSTEMS (QAPL 2014) Affiliated with ETAPS 2014 April 12 - 13, 2014, Grenoble, France http://qapl14.inria.fr * SCOPE Quantitative aspects of computation are important and sometimes essential in characterising the behaviour and determining the properties of systems. They are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust). Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems. In particular, the workshop focuses on: - the design of probabilistic, real-time, quantum languages and the definition of semantical models for such languages - the discussion of methodologies for the quantitative analysis of systems, for instance probabilistic and timing properties (e.g. security, safety, schedulability) and other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g., worst-case memory/stack/cache requirements); - the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis) - applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues * TOPICS Topics include (but are not limited to) probabilistic, timing and general quantitative aspects in: Language design, Information systems, Asynchronous HW analysis, Language extension, Multi-tasking systems, Automated reasoning, Language expressiveness, Logic, Verification, Quantum languages, Semantics, Testing, Time-critical systems, Performance analysis, Safety, Embedded systems, Program analysis, Risk and hazard analysis, Coordination models, Protocol analysis, Scheduling theory, Distributed systems, Model-checking, Security, Biological systems, Cyber-physical systems, Concurrent systems, and Resource analysis. * INVITED SPEAKERS - Stephen Gilmore, University of Edinburgh, UK - Oded Maler, Verimag, France - Nicolas Markey, LSV, CNRS and ENS Cachan, France - Enrico Vicario, University of Firenze, Italy * SUBMISSIONS In order to encourage participation and discussion, this workshop solicits two types of submissions - regular papers and presentation reports: 1. Regular paper submissions must be original work, and must not have been previously published, nor be under consideration for publication elsewhere. Regular paper submission must not exceed 15 pages, possibly followed by a clearly marked appendix which will be removed for the proceedings and contains technical material for the reviewers. 2. Presentation reports concern recent or ongoing work on relevant topics and ideas, for timely discussion and feedback at the workshop. There is no restriction as for previous/future publication of the contents of a presentation. Typically, a presentation is based on a paper which recently appeared (or which is going to appear) in the proceedings of another recognized conference, or which has not yet been submitted. The (extended) abstract of presentation submissions should not exceed 4 pages. All submissions must be in PDF format and use the EPTCS latex style, see http://style.eptcs.org/. Submissions can be made on the following website: http://www.easychair.org/conferences/?conf=qapl14 The workshop PC will review all regular paper submissions to select appropriate ones, ones for acceptance in each category, based on their relevance, merit, originality, and technical content. Presentation reports will receive a light weight review to establish their relevance for the workshop. The authors of accepted submissions of both types are expected to present and discuss their work at the workshop. Accepted regular papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). A special issue concerning the QAPL editions of 2011 and 2012 is in preparation and a further special issues related to the QAPL editions of 2013 and 2014 will be considered. * IMPORTANT DATES For regular papers: Abstract (optional): December 24, 2013 Submission (regular paper): December 31, 2013 Notification: February 7, 2014 Final version (ETAPS proceedings): February 14, 2014 Workshop: March 23 - 24, 2013 Final version (EPTCS post proceedings): TBA For presentation reports: Submission: February 5, 2014 Notification: February 7, 2014 * PC CHAIRS - Nathalie Bertrand, INRIA Rennes, France - Luca Bortolussi, University of Trieste, Italy EAPLS PHD AWARD 2012 Call for Nominations http://eapls.org/pages/phd_award/ * AWARD The European Association for Programming Languages and Systems has established a Best Dissertation Award in the international research area of programming languages and systems. The award will go to the PhD student who in the previous period has made the most original and influential contribution to the area. The purpose of the award is to draw attention to excellent work, to help the career of the student in question, and to promote the research field as a whole. * ELIGIBILITY Eligible for the award are those who successfully defended their PhD - at an academic institution in Europe - in the field of Programming Languages and Systems - in the period from 1 November 2012 – 1 November 2013 * NOMINATIONS Candidates for the award must be nominated by their supervisor. Nominating a candidate consists of submitting the thesis to https://www.easychair.org/conferences/?conf=eaplsphd2013. The nomination must be accompanied by (a zip file containing) - a letter from the supervisor describing why the thesis should be considered for the award; - a report from an independent researcher who has acted as examiner of the thesis at its defense. The theses will be evaluated with respect to originality, influence, relevance to the field and (to a lesser degree) quality of writing. * PROCEDURE The nominations will be evaluated and compared by an international committee of experts from across Europe. The procedure to be followed is analogous to the review phase of a conference. The justification by the supervisor and the external report will play an important role in the evaluation. Members of the expert committee are barred from nominating their own PhD students for the award. The award consists of a certificate announcing the winner to have received the EAPLS PhD award 2011. The supervisor will receive a copy of this certificate. If possible, the certificate will be handed out ceremonially at a suitable occasion, as for instance the ETAPS conference. Apart from the winner, no further ranking of nominees will be published. The decision of the expert committee is final and binding, and will not be subject to discussion. * IMPORTANT DATES 31 December 2013: Deadline for nominations 10 April 2014: Announcement of the award winner * EXPERT COMMITTEE The Expert committee includes: - Gilles Barthe, IMDEA Software Institute, Spain - Eerke Boiten, University of Kent, U.K. - Mark van den Brand, Universiteit Eindhoven, The Netherlands - Paolo Ciancarini, Universita di Bologna, Italy - Stefano Crespi Reghizzi, Politecnico di Milano, Italy - Kei Davis, Los Alamos National Laboratory, U.S.A. - Mariangiola Dezani, Universita di Torino, Italy - Josuka Díaz-Labrador, Universidad de Duesto, Spain - Marko van Eekelen, Radboud Universiteit Nijmegen, The Netherlands - Giorgio Ghelli, University of Pisa, Italy - Stefan Gruner, University of Pretoria, South Africa - Kevin Hammond, University of St Andrews, U.K. - Martin Hofmann, Ludwig-Maximilians-Universität München, Germany - Paul Klint, CWI and University of Amsterdam, The Netherlands - Jens Knoop, Technische Universität Wien, Austria - Ralf Lämmel, University of Koblenz-Landau, Germany - Rita Loogen, Philipps-Universität Marburg, Germany - Tiziana Margaria, University of Potsdam, Germany - Greg Michaelson, Heriot-Watt University , Edinburgh, U.K. - Alan Mycroft, University of Cambridge, U.K. - Catuscia Palamidessi, LIX, France - Ricardo Peña, Universidad Complutense de Madrid, Spain - Arnd Poetzsch-Heffter, Technische Universität Kaiserslautern, Germany - Arend Rensink, Universiteit Twente, The Netherlands - Bernhard Steffen, Technische Universität Dortmund, Germany - Peter Van Roy, Université Catholique de Louvain, Belgium ASSISTANT PROFESSOR (UD) POSITION IN LOGIC * This message is to bring to your attention that the Institute for Logic, Language and Computation at the University of Amsterdam currently has an open Assistant Professor (UD) Position in Logic, see http://www.uva.nl/over-de-uva/werken-bij-de-uva/vacatures/item/13-222.html for the details. Please note that the deadline for applications is September 10. As you can read in the job advertisement, we are looking for excellent candidates in mathematical logic, with a preference for a candidate with a proven record in modal logic or related areas of nonclassical logic. It is the explicit policy of the institute that (in principle) new staff are hired through open application procedures. I would therefore like to encourage you to bring this vacancy to the attention of as many colleagues as possible. ASSISTANT/ASSOCIATE PROFESSORS AT DTU * DTU Applied Mathematics and Computer Science has a new opening for associate and/or assistant professors with a focus on the modelling, analysis and realisation of systems using language-based techniques and tools – in particular, static analysis (including abstract interpretation and type systems) and (qualitative and quantitative) model checking. The successful candidate(s) will be part of an international research team focusing on a broad portfolio of research projects using formal methods for modeling and analysis of systems (MT-LAB, IDEA4CPS, TREsPASS, FutureID, SESAMO, PaPP). The date for applications is on October 1st and full details about the call and how to apply are available at http://www.dtu.dk/english/career/7da12e65-dc28-42f6-ad11-6be53914b384.aspx and more information about the Language Based Technology research team is available at http://www.compute.dtu.dk/english/research/LBT * CONTACT Hanne Riis Nielson & Flemming Nielson DTU Compute - Department of Applied Mathematics and Computer Science POSTDOCTORAL SCHOLAR POSITIONS AT THE CENTER FOR SECURE AND DEPENDABLE SYSTEMS AT UNIVERSITY OF IDAHO * We are looking for a sharp graduate(s) to join our team as postdoctoral scholars, starting as early as fall 2013. The postdoc(s) would be a fellow of the Center for Secure and Dependable Systems contingent on availability of funding. * The postdoc will be involved in our research on security & privacy for critical infrastructure systems; working with an interdisciplinary group of faculty (including faculty from computer science, electrical and computer engineering, civil engineering, sociology, psychology and business). As such, the postdoc would join an inter-disciplinary team working on funded projects, be responsible for conducting research, managing a team of student researchers, publishing and presenting papers and assisting in the writing of grant proposals. * The candidate must have finished his or her Ph.D in Computer Science or Computer Engineering, have experience with security and/or privacy, have experience writing and presenting research results, have experience conducting experimental computer security research, and have strong programming skills. Ideal candidates will also have experience with embedded computing, formal methods, security policies and software engineering. * The University of Idaho (http://www.uidaho.edu/), the state’s founding doctoral and research-intensive land-grant institution, has its principal campus in Moscow, Idaho, and regional centers in Boise, Coeur d’Alene, and Idaho Falls. The University engages its statewide constituents in strategic educational, research, and service programs to enhance the well-being of the state, its communities, and its people, as well as to develop in students, a sense of national and global citizenship. * To enrich education through diversity, the University of Idaho is an Equal Opportunity/Affirmative Action. Interested candidates should send their vita (pdf, please), and also arrange to have three letters of reference sent directly to Dr. Jim Alves-Foss by email to jimaf-at-uidaho.edu Those applications arriving by September 1, 2013 will receive first consideration. POST-DOC IN ICT AT TRENTO * One post-doc position in ICT on the research project "Advanced SMT Techniques for Word-level Formal Verification - (WOLF)" is available in Trento, Italy, under the joint supervision of - Alessandro Cimatti, FBK, Trento, and - Roberto Sebastiani, DISI, University of Trento. The research activity will be carried out jointly within the Embedded Systems (ES) Research Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler (FBK), Trento, and the Software Engineering, Formal Methods & Security Research Program, at Department of Information Engineering and Computer Science (DISI) of University of Trento. * AIM AND SCOPE The research activity will aim at investigating and developing novel techniques, methodologies and support tools for Satisfiability Modulo Theories (SMT) for the formal verification of systems. This work will be part of the "Advanced SMT Techniques for Word-level Formal Verification - (WOLF)" project, a three-year research project supported by SRC/GRC (http://www.src.org/compete/s201113/), in collaboration with major HW companies. The ultimate goal of the WOLF project is to provide a comprehensive SMT package to support effective formal verification of systems ranging from RTL circuits all the way up to high-level hardware description languages (e.g. SystemC) and software. The package will be implemented on top of the MathSAT SMT platform (http://mathsat.fbk.eu/), and provided as an API. * CANDIDATE PROFILE The ideal candidate should have an PhD in computer science or related discipline, and combine solid theoretical background and excellent software development skills (in particular C/C++). A solid background knowledge and/or previous experience on one of the following topics (in order of preference) is required: Satisfiability Modulo Theory (SMT), Propositional Satisfiability (SAT), Model Checking, Automated Reasoning. Previous experience in the following areas will also be considered favourably: Constraint Solving and Optimization, Embedded Systems Design Languages (e.g. Verilog, VHDL). The candidate should be able to work in a collaborative environment, with a strong committment to reaching research excellence and achieving assigned objectives. Early availability will be considered with much favour. * TERMS AND DATES The position will start as soon as possible, and will have to be renewed yearly, for a maximum of two years. The expected salary will range from about 2200 to 2400 euros net income, and the gross will include previdential (social security) contributions. Facilities for meals at the local canteen can be provided. * APPLICATIONS AND INQUIRIES Interested candidates should inquire for further information and/or apply by sending email to wolf-recruit@disi.unitn.it, with subject 'POSTDOC ON WOLF PROJECT'. Applications should contain a statement of interest, with a Curriculum Vitae, and the names of reference persons. PDF format is strongly encouraged. It should also indicate an estimated starting date. * CONTACT PERSONS Dr. ALESSANDRO CIMATTI, Embedded Systems Research Unit, FBK-Irst, via Sommarive 18, I-38123 Povo, Trento, Italy http://sra.fbk.eu/people/cimatti/, Prof. ROBERTO SEBASTIANI Software Engineering, Formal Methods & Security Research Program DISI, University of Trento, via Sommarive 14, I-38123 Povo, Trento, Italy http://disi.unitn.it/~rseba/. 11 PHD SCHOLARSHIPS IN COMPUTER SCIENCE AT VERONA * 3-year PhD Program in Computer Science at the Universita di Verona, Italy - Deadline for application: September 23, 2013. Applications must be received by the deadline (with preliminary online submission by Sept. 13) - Start of program: January 1, 2014 - Number of available positions with scholarship: 11 - The application instructions can be downloaded from the following link: http://www.univr.it/documenti/Documento/allegati/allegati754351.pdf * CONTACT Prof. Luca Vigano luca.vigano@univr.it
Back to the LICS web page.