[TYPES/announce] MPLR 2019 - Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Apologies if you receive multiple copies of this CFP. The 16th International Conference on Managed Programming Languages & Runtimes (MPLR, formerly ManLang) is a premier forum for presenting and discussing novel results in all aspects of managed programming languages and runtime systems, which serve as building blocks for some of the most important computing systems around, ranging from small-scale (embedded and real-time systems) to large-scale (cloud-computing and big-data platforms) and anything in between (mobile, IoT, and wearable applications). This year, MPLR is co-located with SPLASH 2019 and sponsored by ACM. For more information, check out the conference website: https://conf.researchr.org/home/mplr-2019 # Topics Topics of interest include but are not limited to: * Languages and Compilers - Managed languages (e.g., Java, Scala, JavaScript, Python, Ruby, C#, F#, Clojure, Groovy, Kotlin, R, Smalltalk, Racket, Rust, Go, etc.) - Domain-specific languages - Language design - Compilers and interpreters - Type systems and program logics - Language interoperability - Parallelism, distribution, and concurrency * Virtual Machines - Managed runtime systems (e.g., JVM, Dalvik VM, Android Runtime (ART), LLVM, .NET CLR, RPython, etc.) - VM design and optimization - VMs for mobile and embedded devices - VMs for real-time applications - Memory management - Hardware/software co-design * Techniques, Tools, and Applications - Static and dynamic program analysis - Testing and debugging - Refactoring - Program understanding - Program synthesis - Security and privacy - Performance analysis and monitoring - Compiler and program verification # Submission Categories MPLR accepts four types of submissions: 1. Regular research papers, which describe novel contributions involving managed language platforms (up to 12 pages excluding bibliography and appendix). Research papers will be evaluated based on their relevance, novelty, technical rigor, and contribution to the state-of-the-art. 2. Work-in-progress research papers, which describe promising new ideas but yet have less maturity than full papers (up to 6 pages excluding bibliography and appendix). When evaluating work-in-progress papers, more emphasis will be placed on novelty and the potential of the new ideas than on technical rigor and experimental results. 3. Industry and tool papers, which present technical challenges and solutions for managed language platforms in the context of deployed applications and systems (up to 6 pages excluding bibliography and appendix). Industry and tool papers will be evaluated on their relevance, usefulness, and results. Suitability for demonstration and availability will also be considered for tool papers. 4. Posters, which can be accompanied by a one-page abstract and will be evaluated on similar criteria as Work-in-progress papers. Posters can accompany any submission as a way to provide additional demonstration and discussion opportunities. MPLR 2019 submissions must conform to the ACM Policy on Prior Publication and Simultaneous Submissions and to the SIGPLAN Republication Policy. # Important Dates and Organization Submission Deadline: ***Jul 8, 2019*** Author Notification: Aug 24, 2019 Camera Ready: Sep 12, 2019 Conference Dates: Oct 20-25, 2019 General Chair: Tony Hosking, Australian National University / Data61, Australia Program Chair: Irene Finocchi, Sapienza University of Rome, Italy Program Committee: * Edd Barrett, King's College London, United Kingdom * Steve Blackburn, Australian National University, Australia * Lubomír Bulej, Charles University, Czech Republic * Shigeru Chiba, University of Tokyo, Japan * Daniele Cono D'Elia, Sapienza University of Rome, Italy * Ana Lúcia de Moura, Pontifical Catholic University of Rio de Janeiro, Brazil * Erik Ernst, Google, Denmark * Matthew Hertz, University at Buffalo, United States * Vivek Kumar, Indraprastha Institute of Information Technology, Delhi * Doug Lea, State University of New York (SUNY) Oswego, United States * Magnus Madsen, Aarhus University, Denmark * Hidehiko Masuhara, Tokyo Institute of Technology, Japan * Ana Milanova, Rensselaer Polytechnic Institute, United States * Matthew Parkinson, Microsoft Research, United Kingdom * Gregor Richards, University of Waterloo, Canada * Manuel Rigger, ETH Zurich, Switzerland * Andrea Rosà, University of Lugano, Switzerland * Guido Salvaneschi, TU Darmstadt, Germany * Lukas Stadler, Oracle Labs, Austria * Ben L. Titzer, Google, Germany
[TYPES/announce] Research Position in Verified Confidentiality for Weak Memory Concurrency
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Research Position in Verified Confidentiality for Weak Memory Concurrency https://people.eng.unimelb.edu.au/tobym/researcher19-weak-memory.html I am seeking an exceptional researcher (either a graduate or a postdoc) to research methods for verifying information flow security for shared-memory concurrent programs executing on weak memory consistency models. The methods will be applied to verify the security of seL4-based critical embedded devices. The position is for two years in the first instance, based at the University of Melbourne under Dr Toby Murray (https://people.eng.unimelb.edu.au/tobym/). This project will provide the opportunity to collaborate with researchers at Australian National University (ANU), Canberra; Data61's Trustworthy Systems Group (the "seL4 team"), Sydney; and Australia's Defence Science and Technology (DST) Group, Brisbane. Candidates should have experience in at least one of the following: - program verification (e.g. Hoare logic), - information flow security, - interactive proof assistants (e.g. Isabelle, Coq, etc.), - concurrent program verification methods (e.g. Owicki-Gries, Rely-Guarantee, Concurrent Separation Logic, etc.), - weak memory consistency models (e.g. x86 TSO, etc.) The following are indicative, entry-level salary figures: Research Assistant (Bachelor's graduate): $65K (AUD) Research Assistant (Master's graduate): $71K (AUD) Postdoctoral Research Fellow: $90K (AUD) Besides salary, total remuneration also includes 9.5% employer superannuation contribution. Applications close on April 30, 11:55pm Australian Eastern Standard Time (GMT +10) Further details, including how to apply, are available here: https://people.eng.unimelb.edu.au/tobym/researcher19-weak-memory.html Informal enquiries should be directed to Toby Murray toby.mur...@unimelb.edu.au https://people.eng.unimelb.edu.au/tobym/
[TYPES/announce] CFP: 2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS 2019), New York City, 14 June 2019
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] 2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS 2019) A satellite event of the CAV conference New York City July 14, 2019 https://fomlas2019.wixsite.com/fomlas2019 = SCOPE In recent years, machine learning has emerged as a highly effective way for creating real-world software, and is revolutionizing the way complex systems are being designed all across the board. In particular, this new approach is being applied to autonomous systems (e.g., autonomous cars, aircraft), achieving exciting results that are beyond the reach of manually created software. However, these significant changes have created new challenges when it comes to explainability, predictability and correctness: Can I explain why my drone turned right at that angle? Can I predict what it will do next? Can I know for sure that my autonomous car will never accelerate towards a pedestrian? These are questions with far-reaching consequences for safety, accountability and public adoption of ML-enabled autonomous systems. One promising avenue for tackling these difficulties is by developing formal methods capable of analyzing and verifying these new kinds of systems. The goal of this workshop is to facilitate discussion regarding how formal methods can be used to increase predictability, explainability, and accountability of ML-enabled autonomous systems. The workshop welcomes results ranging from concept formulation (by connecting these concepts with existing research topics in verification, logic and game theory), through algorithms, methods and tools for analyzing ML-enabled systems, to concrete case studies and examples. Topics of interest include, but are not limited to: Formal specifications for systems with ML components SAT-based and SMT-based methods for analyzing systems with ML components Mixed-integer Linear Programming and optimization-based methods for the verification of systems with ML components Testing approaches to ML components Statistical approaches to the verification of systems with ML components Approaches for enhancing the explainability of ML-based systems Techniques for analyzing hybrid systems with ML components = IMPORTANT DATES (all dates are AOE) Abstract submission April 22, 2019 Full paper submissionApril 27, 2019 Author notification June 10, 2019 Workshop July 14, 2019 = COMMITTEE Conference Chairs: Guy Katz (The Hebrew University of Jerusalem, Israel) Nina Narodytska (VMWare Research, USA) Program Committee: Clark Barrett (Stanford University, USA) Chih-Hong Cheng(Fortiss - Research Institute of the Free State of Bavaria, Germany) Suman Jana (Columbia University, USA) Jean-Baptiste Jeannin (University of Michigan, USA) Susmit Jha (SRI, USA) Taylor T. Johnson (Vanderbilt University, USA) Temesghen Kahsai (Groq Inc., USA) Marta Kwiatkowskaa(University of Oxford, UK) Alessio Lomuscio (Imperial College London, UK) Luca Pulina (University of Sassari, Italy) Armando Solar-Lezama (MIT, USA) Martin Vechev (ETH Zurich, Switzerland) = SUBMISSIONS Three categories of submissions are invited: Original papers: papers that contain original research and sufficient detail to assess the merits and relevance of the submission. For papers reporting experimental results, authors are strongly encouraged to make their data available. Presentation-only papers: papers that describe work recently published or submitted. We see this as a way to provide additional access to important developments that the workshop attendees may be unaware of. Extended abstracts: given the informal style of the workshop, we strongly encourage the submission of preliminary reports of work in progress. They may range in length from very short (a couple of pages) to the full 10 pages and they will be judged based on the expected level of interest for the community. All accepted papers will be posted online as part of informal proceedings on the day of the conference. At least one author of each accepted paper is expected to attend the workshop and present the work. Papers in all categories will be peer-reviewed. Papers should not exceed 10 pages and should be in standard-conforming PDF. Technical details may be included in an appendix to be read at the reviewers' discretion. Final versions should be prepared in LaTeX using the LNCS style. (The 10 page does not include references.) To submit a paper, use EasyChair:
[TYPES/announce] SecDev 2019 submission deadline extended: April 22
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The submission deadline for SecDev 2019 has been extended to Monday April 22 (with abstracts due Monday April 15). See below for details of the Call for Papers and Tutorials. - Monday April 15: Abstracts due - Monday April 22: Submissions due - Monday June 10: Author notification # IEEE Secure Development Conference (SecDev) 2019 Call for Papers and Tutorials https://secdev.ieee.org/ *Sponsored by the IEEE Computer Society Technical Committee on Security and Privacy* *September 25-September 27, 2019 at the Hilton Tysons Corner, McLean, VA, USA* ## Overview SecDev is a venue for presenting ideas, research, and experience about how to develop secure systems. It focuses on theory, techniques, and tools to "build security in" to existing and new computing systems, and does not focus on simply discovering the absence of security. The goal of SecDev is to encourage and disseminate ideas for secure system development among academia, industry, and government. It aims to bridge the gap between constructive security research and practice and to enable real-world impact of security research in the long run. Developers have valuable experiences and ideas that can inform academic research, and researchers have concepts, studies, and even code and tools that could benefit developers. Great SecDev contributions could come from attendees of industrial conferences like AppSec and RSA; from attendees of academic conferences like IEEE S, IEEE CSF, USENIX Security, CCS, NDSS, PLDI, ICSE, FSE, ISSTA, SOUPS, HOST, and others; and from newcomers. Examples of topics that are in scope include: development libraries, tools, or processes to produce systems resilient to certain attacks; formal foundations that underpin a language, tool, or testing strategy that improves security; techniques that drastically improve the scalability of security solutions for practical deployment; and experience, designs, or applications showing how to apply cryptographic techniques effectively to secure systems. We solicit **research papers, position papers, systematization of knowledge papers**, and **"best practice" papers**. All submissions should present novel results, provide novel perspectives and insights, or present new evidence about existing insights or techniques. SecDev also seeks **hands-on and interactive tutorials** on processes, frameworks, languages, and tools for building security in. The goal is to share knowledge on the art and science of secure systems development. (SecDev also seeks posters and tool demos, and abstracts from practitioners to share their practical experiences and challenges in security development. Information on these solicitations are available on the SecDev website https://secdev.ieee.org/.) Areas of interest include (but are not limited to): - Security-focused system designs (HW/SW/architecture) - Tools and methodology for secure code development - Risk management and testing strategies to improve security - Security engineering processes, from requirements to maintenance - Programming languages, development tools, and ecosystems supporting security - Static program analysis for software security - Dynamic analysis and runtime approaches for software security - Automation of programming, deployment, and maintenance tasks for security - Distributed systems design and implementation for security - Privacy by design - Human-centered design for systems security - Formal verification and other high-assurance methods for security - Code reviews, red teams, and other human-centered assurance ## Submission Details The website for submissions is https://hotcrp.ctisl.gtri.gatech.edu/. Submissions must use the two-column IEEE Proceedings style: https://www.ieee.org/conferences/publishing/templates.html. Submissions must be one of two categories: - **Papers**, up to 12 pages, excluding references and well-marked appendices. These must be well-argued and worthy of publication and citation, on the topics above. Research papers must present new work, evidence, or ideas. Position papers with exceptional visions will also be considered. Also welcome are systematization of knowledge papers and "best practice" papers, which should provide an integration and clarification of ideas on an established, major research area, support or challenge long-held beliefs in such an area with compelling evidence, or present a convincing, comprehensive new taxonomy of some aspect of secure development. Authors of accepted papers will present their work at the conference (likely in a 30-minute slot) and their papers will appear in the conference's formal IEEE proceedings. To improve the fairness of the reviewing process, SecDev will follow a light-weight **double-blind reviewing** process. Submitted papers must (a) omit any reference to the
[TYPES/announce] CfP: Trends in Linear Logic and Applications (TLLA 2019)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] === 1st Call for Papers TLLA 2019 3rd International Workshop on Trends in Linear Logic and Applications Dortmund, 29-30 June 2019 Affiliated with FSCD 2019 http://tlla.linear-logic.org/2019/ == Linear Logic is not only a proof theoretical tool to analyse or control the use of ressources in logic and computation. It is also a corpus of tools, approaches, and methodologies (proof nets, exponential decomposition, geometry of interaction, coherent spaces, relational models, etc.) that, even if developed for studying Linear Logic syntax and semantics, have been applied in several other fields (analysis of lambda-calculus computations, game semantics, computational complexity, program verification, etc.). The TLLA international workshop aims at bringing together researchers working on Linear Logic or applying it or its tools. The main goal is to present and discuss trends in the research on Linear Logic and its applications by means of tutorials, invited talks, open discussions, and contributed talks. The purpose is to gather researchers interested in the connections between Linear Logic and various topics such as * theory of programming languages * implicit computational complexity * parallelism and concurrency * games and languages * proof theory * philosophy * categories and algebra * possible connections with combinatorics * linguistics * functional analysis and operator algebras -- ** Submission Guidelines -- Contributions are not restricted to talks presenting an original results, but open to tutorials, open discussions, and position papers. For this reason, we strongly encourage contributions presenting work in progress, open questions, and research projects. Contributions presenting the application of linear logic results, techniques, or tools to other fields, or vice versa, are most welcome. To propose a contributed talk submit a short abstract whose length is between 2 and 5 pages on https://easychair.org/conferences/?conf=tlla19 -- ** Young Researchers Grants -- A limited number of grants for students or young researches are available. Grants can fully or partially cover registration fees, accommodation and transport. To apply for a grant send a message to the organizers of the workshop with: * Affiliation and contact details * A short CV * A letter of motivation explaining the interest of the applicant on one or more topics of the workshop * If the applicant has submitted an abstract * (Optional) One or two support letters. A letter from the supervisor is mandatory for PhD students. For more details and to apply for a grant see http://tlla.linear-logic.org/2019/#grants -- ** Important dates -- * Submission deadline: 1 May 2019 * Notification to authors:15 May 2019 * Final versions due: 24 May 2019 * YR Grant submission deadline: 31 May 2019 * YR Grant notification: 7 June 2019 * Workshop date: 29-30 June 2019 -- ** Publication -- The abstracts of the contributed and invited talks will be published on the site of the conference. -- ** Committees -- ** Program Committee * Thomas Ehrhard, CNRS - University Paris Diderot * Claudia Faggian, CNRS - University Paris Diderot * Giulio Guerrieri, University of Bath * Stefano Guerrini, University of Paris 13 * Esfandiar Haghverdi, Indiana University Bloomington * Naohiko Hoshino, Kyoto University * Marie Kerjean, INRIA Bretagne Atlantique * Olivier Laurent, CNRS - ENS Lyon (chair) * Paolo Pistone, University of Tubingen * Lorenzo Tortora de Falco, University Roma Tre ** Organizing committee --- * Thomas Ehrhard, CNRS - University Paris Diderot * Stefano Guerrini, University of Paris 13 * Lorenzo Tortora de Falco, University Roma Tre
[TYPES/announce] Open Positions in Tokyo: Formal Methods, Learning and Cyber-Physical Systems
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Thanks a lot for disseminating among potentially interested candidates. Apologies for multiple copies] Dear colleagues, For our research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for senior researchers and postdocs (10+ positions in total and some are still open), together with research assistants (PhD students) and internship students. The project runs until March 2022. http://group-mmm.org/eratommsd This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application esp. in automotive industry. In order to deal with the complexity of real-world cyber-physical systems, we need to rely on empirical, learning-based and data-driven measures for quality assurance (such as search-based testing). At the same time, we are finding logical and automata-theoretic methods---the bedrock of formal verification and synthesis--playing pivotal roles also in those empirical quality assurance measures. This way, our project offers an exciting scientific environment that mixes formal methods, software engineering and machine learning. We also collaborate closely with https://www.autonomoose.net/, an automated driving project at Waterloo, Canada. The following are prerequisites for application. - Your background in one of the following fields: formal methods, programming languages, control theory, control engineering, software science, software engineering, machine learning, numerical optimization, user interface, mathematical logic or category theory - Your willingness to dive into the heterogeneous (and thus exciting!) scientific environment as described in the above For more about the project, including our recent activities and output, please visit http://group-mmm.org/eratommsd About the open positions, the page http://group-mmm.org/eratommsd/openpositions.html has more information (esp. how to apply/inquire). Best regards, Ichiro == Ichiro Hasuo Associate Professor, National Institute of Informatics i.ha...@acm.org Secretaries: hasuolab-s...@nii.ac.jp http://group-mmm.org/~ichiro/
