[TYPES/announce] Tenth (Virtual) Summer School on Formal Techniques, May 22-28, 2021
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Tenth Summer School on Formal Techniques , May 22 - May 28, 2020 (http://fm.csl.sri.com/SSFT21) [Due to the pandemic, the Tenth Summer School on Formal Techniques that was postponed from 2020 will be virtual this year.] Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the tenth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions. = The lecturers at the school include: * Thomas Reps (University of Wisconsin) Algebraic Program Analysis: Automating Abstract Interpretation * Natasha Sharygina (University of Lugano, Switzerland) SMT-streamlined Software Model Checking * Warren A. Hunt, Jr. and J Strother Moore (University of Texas) Proving Properties of Algorithms, Hardware, and Software with ACL2 * Jose Meseguer (University of Illinois at Urbana-Champaign) Executable Formal Specification and Verification in Maude The main lectures in the summer school start on Monday May 24 and will be preceded by a background course on logic on Saturday May 22 and Sunday May 23: * Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole Polytechnique) Speaking Logic = The summer school also include several distinguished invited talks. Information about previous Summer Schools on Formal Techniques can be found at http://fm.csl.sri.com/SSFT11 http://fm.csl.sri.com/SSFT12 http://fm.csl.sri.com/SSFT13 http://fm.csl.sri.com/SSFT14 http://fm.csl.sri.com/SSFT15 http://fm.csl.sri.com/SSFT16 http://fm.csl.sri.com/SSFT17 http://fm.csl.sri.com/SSFT18 http://fm.csl.sri.com/SSFT19 Jay Bosamiya of CMU has blogged about the 2018 Summer School at https://www.jaybosamiya.com/blog/2018/05/31/ssft/ === Registration is at the URL: http://fm.csl.sri.com/SSFT21 Those who already registered for the 2020 event need not re-register, and you will be contacted to check if you would like your registration to be processed. Although the summer school is virtual and there is no registration fee, attendance is restricted to registered participants. Attendees who complete the summer school will receive a certificate by mail. Applications should be submitted together with names of two references (preferably advisors, professors, or senior colleagues). Applicants are urged to submit their applications before April 30, 2021, since there are only a limited number of spaces available. We strongly encourage the participation of women and under-represented minorities in the summer school.
[TYPES/announce] Deadline Extension: April 5th, 20201, 14th Conference on Intelligent Computer Mathematics (CICM 2021)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] (Deadline Extension: April 5, 2021) Call for Papers formal papers - informal papers - doctoral programme 14th Conference on Intelligent Computer Mathematics - CICM 2021 - July 26-31, 2020 Timisoara, Romania http://www.cicm-conference.org/2021 -- Invited Speakers * Alessandro Cimatti (Fondazione Bruno Kessler, Trento, IT) * Michael Kohlhase (FAU Erlangen-Nürnberg, Germany) * Laura Kovacs (TU Vienna, Austria) * Angus McIntyre (London/Edinburgh, UK) -- Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. CICM 2021 Programme committee: see https://www.cicm-conference.org/2021/cicm.php?event==pc CICM 2021 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to * theorem proving and computer algebra * mathematical knowledge management * digital mathematical libraries CICM appreciates the varying nature of the relevant research in this area and invites submissions of different forms: 1) Formal submissions will be reviewed rigorously and accepted papers will be published in a volume of Springer LNCS: * regular papers (up to 15 pages including references) present novel research results * project and survey papers (up to 15 pages + bibliography) summarize existing results * system and dataset descriptions (up to 5 pages including references) present digital artifacts * system entry (1 page according to the given LaTeX template) provides metadata and a quick overview of a new tool or a new release of an existent tool 2) Informal submissions will be reviewed with a positive bias and selected for presentation based on their relevance for the community. * informal papersmay presentwork-in-progress, project announcements, position statements, etc. * posters and system demos will be presented in parallel in special sessions 3) The doctoral programme provides PhD students with a forum to present early results and receive constructive feedback and mentoring. *** Important Dates *** - Abstract deadline: As soon as possible before the fullpaper submission deadline. - Full paper deadline:April 5, 2021 (extended deadline) - Reviews sent to authors:May 9, 2021 (extended deadline) - Rebuttals due: May 13, 2021 (extended deadline) - Notification of acceptance: May 18, 2021 (extended deadline) - Camera-ready copies due:May 31, 2021 (extended deadline) - Conference: July 26-31, 2021 Informal submissions and doctoral programme - Submission deadline:May 15, 2021 - Notification of acceptance: June 1, 2021 All submissions should be made via easychair at https://easychair.org/conferences/?conf=cicm2021 As in previous years, we will publish the CICM 2021 proceedings with Springer LNCS.
[TYPES/announce] 2nd CfP: SCSS 2021
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] = SCSS 2021 The 9th International Symposium on Symbolic Computation in Software Science -- In the era of Computational and Artificial Intelligence -- September 8--10, 2021, virtual Organized by RISC, Johannes Kepler University Linz, Austria https://www.risc.jku.at/conferences/scss2021/ = Overview Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects, etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis. Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems that interact with humans naturally by reasoning, aiming at learning at scale. The purpose of SCSS 2021 is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques. Scope -- SCSS 2021 solicits submissions on all aspects of symbolic computation and their applications in software science, in combination with artificial intelligence and cognitive computing techniques. The topics of the symposium include, but are not limited to the following: - automated reasoning, knowledge reasoning, common-sense reasoning and reasoning in science - algorithm (program) synthesis and/or verification, alignment and joint processing of formal, semi-formal, and informal libraries. - formal methods for the analysis of network and system security - termination analysis and complexity analysis of algorithms (programs) - extraction of specifications from algorithms (programs) - theorem proving methods and techniques, collaboration between automated and interactive theorem proving - proof carrying code - generation of inductive assertion for algorithm (programs) - algorithm (program) transformations - combinations of linguistic/learning-based and semantic/reasoning methods - formalization and computerization of knowledge (maths, medicine, economy, etc.) - methods for large-scale computer understanding of mathematics and science - artificial intelligence, machine learning and big-data methods in theorem proving and mathematics - formal verification of artificial intelligence and machine learning algorithms, explainable artificial intelligence, symbolic artificial intelligence - cognitive computing, cognitive vision, perception systems and artificial reasoners for robotics - component-based programming - computational origami - query languages (in particular for XML documents) - semantic web and cloud computing Important Dates --- May 18: title and single-paragraph abstract submission deadline. May 25: paper submission deadline. July 12: notification deadline. July 30: final paper submission deadline. September 8-10, 2021: the symposium dates (virtual). Keynote speaker --- Bruno Buchberger (RISC, Johannes Kepler University Linz, Austria) Invited Speakers -- Tateaki Sasaki (University of Tsukuba, Japan) Martina Seidl (Johannes Kepler University Linz, Austria) Stephen M. Watt (University of Waterloo, Canada) General Chairs - Adel Bouhoula (Arabian Gulf University, Bahrain) Tetsuo Ida (University of Tsukuba, Japan) Program Chair - Temur Kutsia (Johannes Kepler University, Austria) Program Committee - David Cerna (Czech Academy of Sciences, Czech Republic, and Johannes Kepler University Linz, Austria) Changbo Chen (Chinese Academy of Sciences, China) Rachid Echahed (CNRS, Grenoble, France) Seyed Hossein Haeri (UC Louvain, Belgium) Mohamed-Bécha Kaâniche (Sup'Com, Carthage University, Tunisia) Cezary Kaliszyk (University of Innsbruck, Austria) Yukiyoshi Kameyama (University of Tsukuba, Japan) Michael Kohlhase (University of Erlangen-Nuremberg, Germany) Laura Kovacs (Vienna University of Technology, Austria) Temur Kutsia (Johannes Kepler University Linz, Austria) (Chair) Zied Lachiri (ENIT, University of Tunis El Manar, Tunisia) Christopher Lynch (Clarkson University, USA) Mircea Marin (West University of Timisoara, Romania) Yasuhiko Minamide (Tokyo Institute of Technology, Japan) Yoshihiro Mizoguchi (Kyushu University, Japan) Julien Narboux (Strasbourg University, France) Michaël Rusinowitch (INRIA, France) Wolfgang Schreiner (Johannes Kepler University Linz,
[TYPES/announce] Call for Nominations: EiC of ACM TOCL journal
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Nominations Editor-In-Chief ACM Transactions on Computational Logic The term of the current Editor-in-Chief (EiC) of the ACM Transactions on Computational Logic (TOCL http://tocl.acm.org/) is coming to an end, and the ACM Publications Board has set up a nominating committee to assist the Board in selecting the next EiC. Nominations, including self-nominations, are invited for a three-year term as TOCL EiC, beginning on July 1, 2021. The EiC appointment may be renewed at most one time. This is an entirely voluntary position, but ACM will provide appropriate administrative support. Appointed by the ACM Publications Board, Editors-in-Chief (EiCs) of ACM journals are delegated full responsibility for the editorial management of the journal consistent with the journal's charter and general ACM policies. The Board relies on EiCs to ensure that the content of the journal is of high quality and that the editorial review process is both timely and fair. He/she has the final say on acceptance of papers, size of the Editorial Board, and appointment of Associate Editors. A complete list of responsibilities is found in the ACM Volunteer Editors Position Descriptions (http://www.acm.org/publications/policies/position_descriptions). Additional information can be found in the following documents: - Roles and Responsibilities in ACM Publishing https://www.acm.org/publications/policies/roles-and-responsibilities - ACM's Evaluation Criteria for Editors-in-Chief http://www.acm.org/publications/policies/evaluation/ Nominations should include a vita along with a brief statement of why the nominee should be considered. Self-nominations are encouraged and should include a statement of the candidate's vision for the future development of TOCL. The deadline for submitting nominations is May 7, 2021, although nominations will continue to be accepted until the position is filled. Please send all nominations to the search committee chair, Dale Miller (dale.mil...@inria.fr). The search committee members are: - Dale Miller (Inria & LIX/IPP, France), Chair - Christel Baier (TU Dresden, Germany) - Prakash Panangaden (McGill University, Canada) - Andrew Pitts (University of Cambridge, UK) - Simona Ronchi Della Rocca (University of Turin, Italy) - Adelinde Uhrmacher (University of Rostock, Germany) ACM Pubs Board Liaison
[TYPES/announce] 2nd CfP: 14th Interaction and Concurrency Experience (ICE 2021)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ICE 2021 14th Interaction and Concurrency Experience June 18, 2021 University of Malta, Valletta and/or online Satellite workshop of DisCoTec 2021 https://www.discotec.org/2021/ice Submission link: https://openreview.net/group?id=DisCoTec.org/2021/Workshop/ICE Interaction and Concurrency Experience (ICE) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions. === HIGHLIGHTS === * Distinctive selection procedure * ICE welcomes full papers to be included in the proceedings * ICE also welcomes oral communications of already published or preliminary work * Publication in EPTCS * Special issue in the Journal of Logical and Algebraic Methods in Programming (Elsevier) (to be confirmed) * Invited speakers: TBA === IMPORTANT DATES === * 15 April 2021: abstract submission * 19 April 2021: paper submission * 18 May 2021: notification * 18 June 2021: ICE workshop * 12 July 2021: camera-ready for EPTCS post-proceedings === SCOPE === The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. We solicit contributions relevant to Interaction and Concurrency, including but not limited to: * Formal semantics * Process algebras and calculi * Models and languages * Protocols * Logics and types * Expressiveness * Model transformations * Tools, implementations, and experiments * Specification and verification * Coinductive techniques * Tools and techniques for automation * Synthesis techniques === SELECTION PROCEDURE === Since its first edition in 2008, the distinguishing feature of ICE has been an innovative paper selection mechanism based on an interactive, friendly, and constructive discussion amongst authors and PC members in an online forum. During the review phase, each submission is published in a dedicated discussion forum. The discussion forum can be accessed by the authors of the submission and by all PC members not in conflict with the submission (the forum preserves anonymity). The forum is used by reviewers to ask questions, clarifications, and modifications from the authors, allowing them better to explain and to improve all aspects of their submission. The evaluation of the submission will take into account not only the reviews, but also the outcome of the discussion. As witnessed by the past editions of ICE, this procedure considerably improves the accuracy of the reviews, the fairness of the selection, the quality of camera-ready papers, and the discussion during the workshop. ICE adopts a light double-blind reviewing process, detailed below. === SUBMISSION GUIDELINES === Submissions must be made electronically in PDF format via OpenReview: https://openreview.net/group?id=DisCoTec.org/2021/Workshop/ICE We invite two types of submissions: * Research papers, original contributions that will be published in the workshop post-proceedings. Research papers must not be simultaneously submitted to other conferences/workshops with refereed proceedings. Research papers should be 3-16 pages plus at most 2 pages of references. Short research papers are welcome; for example a 5 page short paper fits this category perfectly. The submitted PDF can use any LaTeX style (but the post-proceedings will use the EPTCS style). * Oral communications will be presented at the workshop, but will not appear in the post-proceedings. This type of contribution includes e.g. previously published contributions, preliminary work, and position papers. There is no strict page limit for this kind of submission but papers of 1-5 pages would be appreciated. For example, a one page summary of previously published work is welcome in this category. Authors of research papers must omit their names and institutions from the title page, they should refer to their other work in the third person and omit acknowledgements that could reveal their identity or affiliation. The purpose is to avoid any bias based on authors’ identity characteristics, such as gender, seniority, or nationality, in the review process. Our goal is to facilitate an unbiased approach to reviewing by supporting reviewers’ access to works that do not carry obvious references to
[TYPES/announce] Morello: Edinburgh research posts on capability-based security technologies
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Morello: Digital Security by Design Technology Platform Prototype Laboratory for Foundations of Computer Science School of Informatics The University of Edinburgh https://www.jobs.ac.uk/job/CEO974/research-associate *** Applications close 2 April 2021 at 1600 UTC *** We are recruiting two postdoctoral researchers to join the Innovate UK project "Digital Security by Design: Technology Platform Prototype". This is a research collaboration between Arm and the Universities of Cambridge and Edinburgh to develop the Morello platform, applying a novel capability-based architecture to a mainstream high-performance processor and software stack. Further information below: for full details and how to apply please follow the link above. If you would like to discuss informally then please contact ian.st...@ed.ac.uk, the project lead for Edinburgh. The University of Edinburgh only take formal references after appointment: if you have individual letters of support then please submit these as part of your initial application. Follow these links for more about the wider project. Morello Platform: https://www.morello-project.org CHERI Architecture: http://www.cheri-cpu.org Sail Language: https://www.cl.cam.ac.uk/~pes20/sail/ Detailed developer information from Arm https://developer.arm.com/architectures/cpu-architecture/a-profile/morello Video presentation of CHERI security architecture and Morello platform https://vimeo.com/486754830 The only essential requirement for these positions is that a PhD or equivalent research experience in computer science, informatics, mathematics, or a related discipline. This includes being close to PhD completion and submission. We are particularly interested to hear from candidates with any of the following. There is no requirement to demonstrate all of these together: this project crosses domains and the precise tasks followed will depend on each researcher's individual skills, experience, and interests. - Experience with machine-assisted reasoning tools and automated provers: such as Coq, Isabelle, HOL4; or SAT/SMT solvers - Experience with functional programming in OCaml - Knowledge of instruction-set architectures; specifically Arm A64, but RISC-V also relevant - Knowledge of programming-language semantics and type systems - Knowledge of program logics, program analysis, and specification -- Ian Stark Laboratory for Foundations of Computer Science http://homepages.ed.ac.uk/stark School of Informatics, University of Edinburgh -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
