[TYPES/announce] CfP - 3rd International Conference on Microservices (Microservices 2020)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] International Conference on Microservices: Call for Papers == Third International Conference on Microservices September 8th-10th 2020, Bologna, Italy https://www.conf-micro.services/2020/ Important dates --- - Submission deadline: May 15th, 2020 (AoE) - Notification to authors: June 26th, 2020 (AoE) - Camera-ready due: August 7th, 2020 (AoE) - Early bird registration until: August 7th, 2020 Theme and Topics The theme of this edition is the interplay between microservices and the cyber security. - On the one hand, the adoption of microservices is fostering the adoption of new architectural patterns and software construction practices; understanding the security properties (or the emerging vulnerabilities) of the resulting constructs calls for the development of a fresh mindset in analysts, designers and testers alike. In addition, the additional middleware and infrastructure typically proposed for the management of microservice-based architectures could expand the attack surface of the systems. - On the other hand, the same frameworks could instead prove valuable allies to collect security-relevant information and to coordinate defenses. The above considerations concern the intrinsic interplay between the fields of microservices and security. The broader application context is peculiarly sensitive to them: microservices are often adopted as an accelerator of digital transformations as the successful past edition(s) of the conference have shown. In this light, security issues should be a primary concern for microservices researchers and practitioners, as they provide an opportunity to integrate security-by-design into the recent advances in software development - triggered and amplified by microservices principles, patterns, and technologies. Topics of interest are not limited to our cyber security theme. We are interested in all aspects and phases of the design and implementation of microservice architectures: - Software engineering methods for microservices, specifically (but not limited to) agile service design practices, behavior- and domain-driven design - Identification, specification, and realization of candidate services - Patterns for IDEAL cloud-native application architectures; service API design and management - Microservices infrastructure components: API gateways, side cars, and service meshes; reactive messaging brokers; service registries; service containers and cluster managers; infrastructure as code - Function-as-a-service and serverless cloud offerings; service-based event sourcing and data streaming architectures - Security and other service quality concerns (consistency, availability, recoverability) in microservices; dealing with General Data Protection Regulation (GDPR) compliance and other data privacy requirements - Testing for microservices: unit tests, system tests, acceptance and regression tests, test-driven service development - Formal models for microservices - Verification (both static and runtime) of microservice systems - DevOps for microservices, in particular (but not limited to) continuous deployment and distributed monitoring - Microservice management: fault, configuration, accounting, performance, security - Discovery/recovery and reverse engineering of microservices solutions - Microservice evolution - Programming languages, notations, and techniques for microservices - Empirical studies of microservices adoption We solicit contributed talks based work in progress, scientific work published or submitted for publication, or practical experience reports. Authors wishing to present their work are invited to submit extended abstracts following the submission guidelines. Abstracts and presentations must be in English. Submissions Guidelines -- A submission should describe a talk to be given at the conference in the form of extended abstracts with a maximum of two pages. Submissions can be based on work in progress, scientific work published or submitted for publication, practical experience reports, or practical tool demonstrations. They must further be prepared using the EasyChair template (LaTeX, MS Word), be in PDF format, printable in black and white on A4 paper, and interpretable by common PDF tools. Submissions must be in English. Contributions will be reviewed and selected by the Program Committee. Extended abstracts of accepted contributions will be available electronically before the conference. Organisation General Chair: Maurizio Gabbrielli, University of Bologna (IT) Program Chairs: Marco Prandini, University of Bologna (IT) Gianluigi Zavattaro, University of Bologna (IT) Olaf Zimmermann, University of Applied Sciences of Eastern Switzerland, Rapperswil (HSR OST) (CH)
[TYPES/announce] 2 new postdoc positions on Frama-C at CEA Paris Saclay
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Hello, The Software Security and Reliability Lab (LSL) at CEA Paris Saclay (France) is hiring 2 postdoc researchers who will work on Frama-C, its code analysis framework for C programs, in the context on the recently accepted H2020 European project Ensuresec. The research topics are: - Advanced Runtime Assertion Checking of C Programs: http://julien.signoles.free.fr/positions/postdoc-ensuresec-eacsl.pdf - Extensive Code Security Analyses for Frama-C: http://julien.signoles.free.fr/positions/postdoc-ensuresec-security.pdf Best regards, Julien Signoles -- Researcher-engineer | Scientific advisor CEA LIST, Software Reliability and Security Lab | Department of Software and System Engineering tel:(+33)1.69.08.00.18 julien.signo...@cea.fr
[TYPES/announce] Applied Category Theory 2020 - Second Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] SECOND CALL FOR PAPERS 3rd Annual International Conference on Applied Category Theory (ACT2020) July 6 – 10, 2020 http://act2020.mit.edu * * * Applied category theory is a topic of interest for a growing community of researchers interested in studying many different kinds of systems using category-theoretic tools. These systems are found across computer science, mathematics, and physics, as well as in social science, linguistics, cognition, and neuroscience. The background and experience of our members is as varied as the systems being studied. The goal of the Applied Category Theory conference is to provide a platform for researchers in the area to discuss recent progress. We seek submissions of both original research papers and extended abstracts of work that's been submitted, accepted, or published elsewhere. Original research papers we accept will be invited for publication in a proceedings volume. Some contributions will be invited to become keynote addresses, and best paper award(s) may also be given. ACT2020 will be held entirely online, with all the attendant advantages: no registration fee, no need to travel, etc. It will consist of three 2-hour sessions per day, spaced the clock to accommodate the different time zones of our speakers. All the talks will be both live streamed and recorded on YouTube. Our goal is a conference that provides high quality, interactive talk sessions; generative, high bitrate discussions; and serendipitous interactions with new people. The conference will include a business showcase, and it will be preceded by a tutorial day. This event follows ACT2018 in Leiden, and ACT2019 in Oxford. ** IMPORTANT DATES (all in 2020)** Submission of contributed papers: Sunday May 10 Success notification: Sunday June 7 Tutorial day: July 5 Main conference: July 6 – 10 ** SUBMISSIONS ** Two types of submissions are accepted, both of which will be reviewed using the same standards: - Proceedings Track. Original contributions of high-quality work consisting of a 5 – 12 page extended abstract that provides evidence of results of genuine interest, and with enough detail to allow the program committee to assess the merits of the work. Submission of a work-in-progress is encouraged, but it must be more substantial than a research proposal. - Non-Proceedings Track. Descriptions of high-quality work submitted or published elsewhere will also be considered, provided the work is recent and relevant to the conference. The work may be of any length, but the program committee members may only look at the first 3 pages of the submission, so you should ensure that these pages contain sufficient evidence of the quality and rigor of your work. Submissions should be prepared using LaTeX, and must be submitted in PDF format. The submission link is available on the ACT2020 web page. ** PROGRAM COMMITTEE ** Mathieu Anel, Carnegie Mellon University Miriam Backens, University of Birmingham John Baez, Centre for Quantum Technologies Richard Blute, University of Ottawa Tai-Danae Bradley, City University of New York Andrea Censi, ETH Zurich Corina Cirstea, ETC Zurich Bob Coecke, University of Oxford Valeria de Paiva, Samsung Research America and University of Birmingham Ross Duncan, University of Strathclyde Eric Finster, University of Birmingham Brendan Fong, Massachusetts Institute of Technology Tobias Fritz, Perimeter Institute for Theoretical Physics Richard Garner, Macquarie University Fabrizio Romano Genovese, Statebox Jeremy Gibbons, University of Oxford Amar Hadzihasanovic, IRIF, Université de Paris Helle Hvid Hansen, Delft University of Technology Jules Hedges, Max Planck Institute for Mathematics in the Sciences Kathryn Hess Bellwald, Ecole Polytechnique Fédérale de Lausanne Chris Heunen, The University of Edinburgh Alex Hoffnung, Bridgewater Joachim Kock, Universitat Autònoma de Barcelona Alexander Kurz, Chapman University Tom Leinster, The University of Edinburgh Martha Lewis, University of Amsterdam Daniel R. Licata, Wesleyan University David Jaz Myers, Johns Hopkins University Paolo Perrone, Massachusetts Institute of Technology Daniela Petrisan, University of Paris, IRIF Vaughan Pratt, Stanford University Peter Selinger, Dalhousie University Michael Shulman, University of San Diego David I. Spivak, Massachusetts Institute of Technology (co-chair) John Terilla, Tunnel Technologies Walter Tholen, York University Todd Trimble, Western Connecticut State University Christina Vasilakopoulou, University of Patras Jamie Vicary, University of Birmingham (co-chair) Maaike Zwart, University of Oxford
[TYPES/announce] International Workshop on Confluence [IWC 2020] - 2nd CFP
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] --//////////////////////////-- Second Call For Papers 9th International Workshop on Confluence http://iwc2020.cic.unb.br June 30, 2020 Collocated with FSCD-IJCAR 2020, June 29 - July 5, 2020 --//////////////////////////-- The 9th International Workshop on Confluence (IWC 2020) aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications. ## IMPORTANT INFORMATION Due to current travel restrictions in various countries, the meeting will be held **virtually** this year. The technical details will be given in due time. ## TOPICS - confluence and related properties (unique normal forms, commutation, ground confluence) - completion - critical pair criteria - decidability issues - complexity issues - system descriptions - certification - applications of confluence The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2020 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research. IWC 2020 is a satellite workshop of Formal Structures for Computation and Deduction (FSCD'20, co-located with IJCAR). IWC 2020 is part of Paris Nord Summer of LoVe 2020, a joint event on LOgic and VErification at University Paris 13, made of Petri Nets 2020, IJCAR 2020, FSCD 2020, and over 20 satellite events. Previous editions took place in Dortmund (2019), Oxford (2018 and 2017), Obergurgl (2016), Berlin (2015), Vienna (2014), Eindhoven (2013) and Nagoya (2012). More information about the workshop can be found in the homepage of IWC. ## SUBMISSIONS We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at: https://easychair.org/conferences/?conf=iwc20200 EasyChair style: http://easychair.org/publications/for_authors ## IMPORTANT DATES - Title and Abstract: April 17, 2020 - Paper Submission: April 22, 2020 - Notification to authors: May 22, 2020 - Workshop date: June 30, 2020 ## INVITED SPEAKERS - TBD - TBD ## PROGRAM COMMITTEE - Beniamino Accattoli (Inria & LIX, École Polytechnique) - Mauricio Ayala-Rincón (Universidade de Brasília) - co-chair - Cyrille Chenavier (Centre Inria Lille) - Alejandro Díaz-Caro (Universidad Nacional de Quilmes & ICC/UBA-CONICET) - Maribel Fernández (King's College London) - Mario Florido (Universidade de Porto) - Makoto Hamana (Gunma University) - Philippe Malbos (Université Claude Bernard Lyon 1) - Samuel Mimram (LIX École Polytechnique) - co-chair - Camilo Rocha (Pontificia Universidad Javeriana - Cali) - Daniel Lima Ventura (Universidade Federal de Goiás) - Femke van Raamsdonk (VU University Amsterdam) - Johannes Waldmann (Hochschule für Technik, Wirtschaft und Kultur Leipzig) - Sarah Winkler (Universität Innsbruck) ## FSCD 2020 ORGANISING COMMITTEE - FSCD/IJCAR Conference Chairs: Stefano Guerrini (University Paris 13) Kaustuv Chaudhuri (Inria & Ecole polytechnique, France) - FSCD/IJCAR Workshop Chairs: Giulio Manzonetto (Université Paris-Nord, France) Andrew Reynolds (University of Iowa, USA) ## CONTACT Mauricio Ayala-Rincón: ayala(at)unb.br Samuel Mimram: samuel.mimram(at)lix.polytechnique.fr
[TYPES/announce] Update on Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'20) on July 5-6, 2020
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] UPDATE: - HoTT/UF 2020 will take place online - Submission deadline: May 20, 2020 Details below. Best, Benedikt * Workshop on Homotopy Type Theory and Univalent Foundations July 5-6, 2020, The Internet https://hott-uf.github.io/2020 Abstract submission deadline: May 20, 2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Invited talks * Carlo Angiuli (Carnegie Mellon University) * Liron Cohen (Ben-Gurion University) * Pierre-Louis Curien (Université de Paris) # Submissions * Abstract submission deadline: May 20, 2020 * Author notification: June 05, 2020 Submissions should consist of a title and an abstract, in pdf format, of no more than 2 pages, submitted via https://easychair.org/conferences/?conf=hottuf2020 Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (Technische Universität Darmstadt) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders Mörtberg (Stockholm University) * Paige Randall North (Ohio State University) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario)
[TYPES/announce] Example of running a conference online BCTCS starting now
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear type theoretits, if you want to see a conference in theoretical computer science which is running fully online, you can just have a look at it, it is free via Zoom http://cs.swansea.ac.uk/bctcs2020/ you might enjoy some talks or just check out how this works out. Best wishes, Anton Setzer From: Types-announce on behalf of Andrzej Murawski Sent: 05 April 2020 11:33 To: types-announce@lists.seas.upenn.edu Subject: [TYPES/announce] 4th Workshop on Program Equivalence and Relational Reasoning (PERR 2020) [ The Types Forum (announcements only), https://eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Flists.seas.upenn.edu%2Fmailman%2Flistinfo%2Ftypes-announcedata=02%7C01%7CA.G.Setzer%40Swansea.ac.uk%7C404bc4758a274f94557108d7d9841280%7Cbbcab52e9fbe43d6a2f39f66c43df268%7C0%7C1%7C637217033576540851sdata=0WZWSQNbFL2f6VX1aPJUW5e2kP7SWfwISZ%2B%2Bad46mDY%3Dreserved=0 ] PERR 2020: 4TH WORKSHOP ON PROGRAM EQUIVALENCE AND RELATIONAL REASONING Associated with the 32nd International Conference on Computer-Aided Verification (CAV 2020) Los Angeles, CA, United States, July 19, 2020 Submission link: https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Feasychair.org%2Fconferences%2F%3Fconf%3Dperr2020data=02%7C01%7CA.G.Setzer%40Swansea.ac.uk%7C404bc4758a274f94557108d7d9841280%7Cbbcab52e9fbe43d6a2f39f66c43df268%7C0%7C1%7C637217033576540851sdata=v0GgYJ%2FNvCo0aPPITGFF7AbgccvNo%2BUSihPHYXKhaFA%3Dreserved=0 Submission deadline: April 24, 2020 Given the rapidly evolving situation regarding COVID-19, the date of the workshop may change. Please follow the CAV webpage for details. WORKSHOP PERR is an annual international workshop dedicated to the formal verification of program equivalence and related relational problems. It is the 4th in a series of meetings that bring together researchers from different areas interested in equivalence and related questions. Last year's PERR was held as a satellite workshop of ETAPS. PERR 2020 is affiliated with CAV. Program equivalence is arguably one of the most interesting and at the same time important problems in formal verification. It is a cross-cutting topic that has attracted the interest of several research communities: denotational semantics, deductive software verification, bounded model checking, specification inference, software evolution and regression testing, etc. The goal of the workshop is to stimulate an exchange of ideas to forge a community working on Program Equivalence and Relational Reasoning (PERR). The workshop welcomes contributions on the topics mentioned below but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyperproperties, in particular of secure information flow. AREAS OF INTEREST - regression verification - program equivalence - equivalence of higher order programs - product programs, relational calculi - verification of hyperproperties - program refinement, refinement calculus - specification of differences between programs - inferring semantic differences between programs - transformation validation - correct compiler transformations - automata bisimulation - code equivalence checking in teaching and marking This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tool presentations. The workshop will have informal online proceedings. SUBMISSION GUIDELINES Please submit a short abstract (1-2 pages) of your proposed talk via EasyChair. - Submission deadline: Friday 24th April 2020 - Submission link: https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Feasychair.org%2Fconferences%2F%3Fconf%3Dperr20data=02%7C01%7CA.G.Setzer%40Swansea.ac.uk%7C404bc4758a274f94557108d7d9841280%7Cbbcab52e9fbe43d6a2f39f66c43df268%7C0%7C1%7C637217033576540851sdata=8gvLlAa%2BOE%2FnV1wymQF4j%2FN9FopG5IW%2BLoUhN22WrRk%3Dreserved=0 PROGRAM COMMITTEE - Vincent Cheval (INRIA Nancy) - Constantin Enea (Université de Paris, co-chair) - Guilhem Jaber (Université de Nantes) - Nuno Lopes (Microsoft Research Cambridge) - Andrzej Murawski (University of Oxford, co-chair) - Damien Pous (CNRS & ENS Lyon) - Ofer Strichman (Technion) - Nikos Tzevelekos (Queen Mary University of London) - Mattias Ulbrich (KIT)
[TYPES/announce] Two PhD positions in Utrecht
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == Two PhD positions in functional programming == The Department of Information and Computing Sciences at Utrecht University is currently advertising two PhD positions in Functional Programming. The candidates will join the Intelligent Systems group, working with Johan Jeuring, Gabriele Keller, and Wouter Swierstra. Besides research, the successful candidate will be expected to help supervise MSc students and assist in the teaching of courses. The positions should be filled by September 2020, although the exact starting date is negotiable. - Research topics - These two positions are tied to two specific topics. * Programming tutors for Functional Languages (Johan Jeuring) The focus of the position is on designing new technologies to support students working in an intelligent tutoring system for functional programming. We expect to use techniques from dependently typed programming, refinement types, program synthesis, automated theorem proving, and more to analyse student programs, and to help students in taking the next step when developing a program. The candidate will investigate the design and use of multiple technologies for this purpose, add them to Ask-Elle, our intelligent tutoring system, perform experiments with the system, and improve the technologies based on the outcome of the experiments. * Compiler verification for a smart contract language (Wouter Swierstra & Gabriele Keller) This project aims to develop a certifying compiler for Plutus Tx, a subset of the purely functional language Haskell that is used to implement smart contracts for the Cardano blockchain. The Plutus smart contract framework is being developed by IOHK for Cardano and the present project is a joint effort of IOHK and Utrecht University. The Plutus Tx compiler is based on the GHC Haskell compiler and adds a translation step from GHC Core to a minimal lambda calculus. Programs in this lambda calculus are executed during transaction validation in a sandboxed execution environment in a manner that is crucial to the security of the blockchain. This project aims to formalise the semantics of the languages involved, to reason about the transformation and optimisation steps that the compiler performs, and finally, to generate a proof object certifying the correctness of the generated code together with that code. - What we are looking for - The ideal candidates should have a degree in Computer Science, be highly motivated, speak and write English well, and be proficient in producing scientific reports. Furthermore, candidates should be able to demonstrate experience with functional programming languages, such as Haskell, OCaml, ML, Agda, Idris, or Coq. - What we offer - The candidates are offered a full-time position for four or five years, depending on the teaching load. The gross salary ranges between €2,325 in the first year and €2,972 in the fourth year per month for full-time employment. A part-time position of at least 0.8 fte may also be possible. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8.3% per year. The position also includes a generous allocation of fully-paid vacation days. In addition we offer: a pension scheme, partially paid parental leave, and flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. The research group will provide the candidate with necessary support on all aspects of the project. More information is available on the website: Terms and employment: http://bit.ly/1elqpM7 Utrecht is consistently ranked as one of the best places in the world to live. - How to apply - To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, such as your master thesis. It is possible to apply for this position if you are close to obtaining your Master's. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. The application deadline for the first position closes on April 29th. You can apply through the University's website:
[TYPES/announce] The Coq Workshop 2020: Second Call for Talk Proposals + COVID-19 update
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] *** The Coq Workshop 2020: Second Call for Talk Proposals *** Find this call online at: https://coq-workshop.gitlab.io/2020 COVID-19 notice: Due to the COVID-19 outbreak and containment measures in France and in most other countries, the FSCD-IJCAR conferences to which the Coq workshop is affiliated will be held as a virtual event, and so will the Coq workshop. Since the COVID-19 crisis is affecting everyone's life and since attending a virtual event requires less planning ahead than attending a physical one, we have extended the submission deadline. We invite you to submit talk proposals for the Coq workshop 2020, which will be held as a virtual event online on July 5-6 2020. The Coq workshop is part of IJCAR 2020 (https://ijcar2020.org/). The Coq workshop 2020 is the 11th Coq Workshop. The Coq Workshop series (https://coq-workshop.gitlab.io/) brings together Coq (https://coq.inria.fr/) users, developers, and contributors. While conferences usually provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around contributed talks and discussions, supplemented with invited talks, seizing the opportunity of the 35th birthday of the first release of Coq to spread this year's edition over two days. Important dates (UPDATED): - April 27th 2020 (AoE): Deadline for abstract submission - May 20th 2020: Notification to authors - July 5-6th 2020: Workshop Submission Instructions: Authors should submit short proposals through EasyChair (https://easychair.org/conferences/?conf=coq2020) in the form of a PDF extended abstract of at most 2 pages, in full-page single-column style (using the EasyChair template available at https://easychair.org/publications/easychair.zip). Relevant subject matter includes but is not limited to: - Theory and implementation of the Calculus of Inductive Constructions - Language or tactic features - Plugins and libraries for Coq - Techniques for formalization programming languages and mathematics - Applications and experience in education and industry - Tools and platforms built on Coq (including interfaces) - Formalization tricks and pearls Program Committee: - Andrew Appel (Princeton University, USA) - Sylvie Boldo (Inria Saclay, Université Paris-Saclay, France) - Zaynah Dargaye (Nomadic Labs, Paris, France) - Stefania Dumbrava (ENSIEE Paris-Evry, France) - Karl Palmskog (KTH Royal Institute of Technology, Stockholm, Sweden) - Gert Smolka (Saarland University, Germany) - Laurent Théry (Inria Sophia-Antipolis, France) Organizing Committee (co-chairs): - Emilio J. Gallego Arias - Hugo Herbelin - Théo Zimmermann (Inria Paris, Université de Paris, France) [mail: coq2...@easychair.org]
[TYPES/announce] CFP SEFM - International Conference on Software Engineering and Formal Methods
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Papers SEFM 2020 18th International Conference on Software Engineering and Formal Methods Amsterdam, The Netherlands, 14-18 September 2020 https://event.cwi.nl/sefm2020/ IMPORTANT DATES Abstract submission deadline: Monday 27 April 2020 (AoE) Paper submission deadline: Monday 4 May 2020 (AoE) Paper notification:Friday 26 June 2020 Camera ready: Tuesday 7 July 2020 (AoE) Concerning COVID-19 The Program Chairs and the Steering Committee of SEFM 2020 are fully aware that the COVID-19 crisis may require the organisation of alternatives to the scheduled physical conference events, following the recommendations of relevant national and international bodies, such as the World Health Organization. Such possible alternative scenarios include the possibility of remote paper presentations or a full electronic organisation of the conference. Any measures taken will be communicated via the SEFM website and via emails to the authors and the PC. OVERVIEW AND SCOPE SEFM aims to bring together leading researchers and practitioners from academia, industry, and government, to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools. Topics of interest include, but are not limited to, the following aspects of software engineering and formal methods: # Software Development Methods - Formal modeling, specification, and design - Software evolution, maintenance, re-engineering, and reuse # Design Principles - Programming languages - Domain-specific languages - Type theory - Abstraction and refinement # Software Testing, Validation, and Verification - Model checking, theorem proving, and decision procedures - Testing and runtime verification - Statistical and probabilistic analysis - Synthesis - Performance estimation and analysis of other non-functional properties - Other light-weight and scalable formal methods # Security and Safety - Security, privacy, and trust - Safety-critical, fault-tolerant, and secure systems - Software certification # Applications and Technology Transfer - Service-oriented and cloud computing systems, Internet of Things - Component, object, multi-agent and self-adaptive systems - Real-time, hybrid, and cyber-physical systems - Intelligent systems and machine learning - HCI, interactive systems, and human error analysis - Education # Case studies, best practices, and experience reports PAPER SUBMISSION We solicit two categories of papers: - Regular papers describing original research results, case studies, or surveys. Regular papers should not exceed 15 pages, excluding bibliography. - Tool papers that describe an operational tool and its contributions. Tool papers should not exceed 6 pages (including bibliography) and should include the URL of the tool. All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Paper submission is done via EasyChair at https://easychair.org/conferences/?conf=sefm2020 Papers must be formatted according to the guidelines for Springer LNCS papers (see http://www.springer.com/lncs). PUBLICATION All accepted papers will appear in the proceedings of the conference that will be published as a volume in the Formal Methods sublime of the Springer's LNCS series. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to a journal special issue. CONFIRMED KEYNOTE LECTURES Paola Inverardi University of L'Aquila, Italy Website: http://people.disim.univaq.it/inverard/ Eelco Visser Delft University of Technology, Neteherlands Website: https://eelcovisser.org/ PROGRAM COMMITTEE Erika Abraham, RWTH Aachen University, Germany Wolfgang Ahrendt, Chalmers University of Technology, Sweden Alessandro Aldini, University of Urbino, Italy Luís Soares Barbosa, University of Minho, Portugal Maurice H. ter Beek, ISTI-CNR, Italy Dirk Beyer, LMU, Germany Frank de Boer (Co-chair), CWI, Netherlands Ana Cavalcanti, University of York, United Kingdom Antonio Cerone (Co-chair), Nazarbayev University, Kazakhstan Alessandro Cimatti, FBK, Italy Marieke Huisman, University of Twente, Netherlands Alexander Knapp, Universität Augsburg, Germany Jacopo Mauro, University of Southern Denmark, Denmark Paolo Masci, National Institute of Aerospace, USA Tiziana Margaria, Lero, Ireland Peter Müller, ETH Zurich, Switzerland Hans de Nivelle, Nazarbayev University,
[TYPES/announce] Postdoctoral position on verification of concurrent systems via model learning, Royal Holloway University of London, Deadline: 4 May 2020
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] - Application deadline: Midnight, 04 May 2020 - Interview Date: To be confirmed - Starting date: as soon as possible, flexible due to COVID-19; remote working options can be explored. - Salary: £35,931-£37,979, including London allowance (grade 7, pay scales 31-33) - Duration: 33 months Applications are invited for the post of Post-Doctoral Research Assistant in the Computer Science Department at Royal Holloway, University of London. Successful applicants will be working on the EPSRC-funded "Verification of Hardware Concurrency via Model Learning" (CLeVer) project (EP/S028641/1), led by Alexandra Silva (UCL) and Matteo Sammartino (Royal Holloway, University of London). This is a joint research endeavour involving Royal Holloway University of London, University College London, and ARM, world-leading designer of multi-core chips. For an informal discussion about the post, please contact Dr. Matteo Sammartino on matteo.sammart...@rhul.ac.uk. # Project Description Digital devices increasingly rely on multi-threaded computation, with sophisticated concurrent behaviour becoming prevalent at any scale. As the complexity of these systems increases, there is a pressing need to automate the assessment of their correctness, especially with respect to concurrency-related aspects. Formal verification provides highly effective techniques to assess the correctness of systems. However, formal models are usually built by humans, and as such can be error-prone and inaccurate. The CLeVer project aims to: - develop a novel verification framework that relies on learning techniques to automatically build and verify models of concurrency, with a particular focus on multi-core systems. - apply the framework to real-world verification tasks, in collaboration with ARM. # The ideal candidate We are looking for candidates with a PhD in one of the following areas: model-based testing and verification, formal methods for concurrency, automated analysis of hardware systems. Experience in multiple areas will be valued. Candidates ideally should also have strong programming skills. # Where to apply https://jobs.royalholloway.ac.uk/vacancy.aspx?ref=0420-101
