[TYPES/announce] PhD positions at Stevens in PL and Systems
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Cypress group at Stevens is recruiting PhD students. With eight research faculty, we do a broad range of theoretical and practical work. Eric Koskinen, Dave Naumann, and I will be particularly of interest to the TYPES crowd, but people like Tegan Brennan, Georgios Portokalidis, and Jun Xu work on adjacent PL/SE/security/systems topics. https://urldefense.com/v3/__https://www.cs.stevens.edu/cypress/people/__;!!IBzWLUs!BFwPKYyax6Ai8OJEM4UazeUOF_lVKWwm_2NBJLa2ljqjPG0O0Q6C5twd-zRIbNk7x0VQe5U3ZU8zIw$ https://urldefense.com/v3/__http://www.weaselhat.com/2021/09/17/im-looking-for-phd-students/__;!!IBzWLUs!BFwPKYyax6Ai8OJEM4UazeUOF_lVKWwm_2NBJLa2ljqjPG0O0Q6C5twd-zRIbNk7x0VQe5VP3mxvBA$ Stevens is in Hoboken, NJ, directly across the Hudson from New York City. Applications are reviewed on a rolling basis. https://urldefense.com/v3/__https://gradadmissions.stevens.edu/apply/__;!!IBzWLUs!BFwPKYyax6Ai8OJEM4UazeUOF_lVKWwm_2NBJLa2ljqjPG0O0Q6C5twd-zRIbNk7x0VQe5XpEB-9QQ$ GRE/GMAT can be waived---contact me for more information.
[TYPES/announce] PhD and postdoc positions at Université Paris-Saclay, CEA List institute, France, in Advanced Program Analysis for Software Security
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The BINSEC team (https://urldefense.com/v3/__https://binsec.github.io/__;!!IBzWLUs!CMjGi_C3VMplAl-GA7VN6dpwnuOZ_yM50eEvYtbVWyfoMzjZT5W4UVs-D_tugvcwHig_JyaX2NKdpg$ ) opens two PhD and one postdoc positions to work with Michaël Marcozzi and Sébastien Bardin on automatic detection and prevention advanced software vunerabilities. . Start: as soon as possible in 2022. Duration: 3 years (PhD), 2 years (postdoc). . Keywords: binary-level security, program analysis, formal methods, symbolic execution, static analysis, fuzzing, speculation https://urldefense.com/v3/__https://binsec.github.io/jobs/2021/12/03/phd-postdoc-offer.html__;!!IBzWLUs!CMjGi_C3VMplAl-GA7VN6dpwnuOZ_yM50eEvYtbVWyfoMzjZT5W4UVs-D_tugvcwHig_Jya5MmGAnw$ == ABOUT US OUR TEAM - The BINary-level SECurity research group (BINSEC) is a dynamic team of 9 junior and 4 senior researchers. The group has frequent publications in top-tier security, formal methods and software engineering conferences. We work in close collaboration with other French and international research teams, industrial partners and national agencies. The team is part of Université Paris-Saclay, the world’s 13th and European Union’s 1st university, according to the Shanghai ARWU Ranking in 2021. OUR WORK - The team has high-level expertise in several binary code analysis approaches, namely symbolic execution, abstract interpretation and fuzzing. We apply these techniques to improve software security at the binary level, covering notably vulnerability detection, code (de)obfuscation and formal verification. See our website at https://urldefense.com/v3/__https://binsec.github.io/__;!!IBzWLUs!CMjGi_C3VMplAl-GA7VN6dpwnuOZ_yM50eEvYtbVWyfoMzjZT5W4UVs-D_tugvcwHig_JyaX2NKdpg$ for additional information. == JOB OFFERS * a Ph.D position (3 years) in complex software vulnerability detection through greybox and hybrid fuzzing * a Ph.D position (3 years) in formal verification of security properties against micro-architectural attacks * a postdoc position (2 years) in software vulnerability detection in IoT systems through static analysis, fuzzing, symbolic execution and/or machine learning Under the supervision of our senior researchers, you will be expected to solve research problems, implement your solutions into evaluated prototypes, publish at top conferences and journals, mentor students and broadly participate in the scientific life of the team. All positions comprises both theoretical work and coding. You will be able to dedicate a small fraction of your time to teaching if you want so. Our former team members have been able to secure stimulating positions in academia or industry and we will support you in advancing your career. == APPLICATION Candidates should send a CV, a cover letter, and other information (see the link below) to binsec-j...@saxifrage.saclay.cea.fr as soon as possible (and at the latest by January 2022). Applications will be reviewed immediately as they arrive (first come, first served). The positions are expected to start as soon as possible in 2022 (upon completion of all administrative requirements). https://urldefense.com/v3/__https://binsec.github.io/jobs/2021/12/03/phd-postdoc-offer.html__;!!IBzWLUs!CMjGi_C3VMplAl-GA7VN6dpwnuOZ_yM50eEvYtbVWyfoMzjZT5W4UVs-D_tugvcwHig_Jya5MmGAnw$
[TYPES/announce] NFM 2022 - FINAL CALL FOR PAPERS
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] NFM 2022 – FINAL CALL FOR PAPERS The 14th NASA Formal Methods Symposium https://urldefense.com/v3/__https://nfm2022.caltech.edu__;!!IBzWLUs!FS-IzUOJyKQyoKx034C9mMvu2Z7A18z9MLlB2RljVDaCDjfbbCThPjDOJiv4W5nqt9oeHy5CWamKZw$ May 24-27, 2022 Pasadena, California, USA *** EXTENDED SUBMISSION DEADLINE: January 10, 2022 *** The symposium is planned to be held in person at California Institute of Technology, but potentially transitioning to fully virtual if the COVID situation persists. Virtual presentations will be possible even if the conference is held in-person. The symposium has NO registration fee for presenting and attending. IMPORTANT DATES - Abstract Submission: January 3, 2022 *** extended *** - Paper Submission: January 10, 2022 *** extended *** - Paper Notifications: February 28, 2022 - Camera-ready Papers: March 28, 2022 - Symposium: May 24-27, 2022 THEME OF SYMPOSIUM The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems. The focus of the symposium will be on formal/rigorous techniques for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace during all stages of the software life-cycle. The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Research Group, composed of researchers spanning six NASA centers. The organization of NFM 2022 is being led by the Jet Propulsion Laboratory (JPL), located in Pasadena, California. INVITED TALKS AND TUTORIALS - Dines Bjoerner, Technical University of Denmark, Denmark - Edwin Brady, University of St. Andrews, UK - Steve Chien, NASA Jet Propulsion Laboratory, USA - Ankush Desai, Amazon Web Services, USA - Daniel Jackson, MIT, USA - Julia Lawall, INTIA Paris, France - Anastasia Mavridou, KBR Inc / NASA Ames Research Center, USA - Leonardo De Moura, Microsoft Research, USA - Sriram Sankaranarayanan, University of Colorado Boulder, USA - Alex Summers, University of British Columbia, Canada - Emina Torlak, University of Washington, USA TOPICS ON INTEREST Topics of interest include, but are not limited to, the following aspects of formal methods: Advances in formal methods - Interactive and automated theorem proving - SMT and SAT solving - Model checking - Static analysis - Runtime verification - Automated testing - Specification languages, textual and graphical - Refinement - Code synthesis - Design for verification and correct-by-design techniques - Requirements specification and analysis Integration of formal methods techniques - Integration of diverse formal methods techniques - Use of machine learning and probabilistic reasoning techniques in formal methods - Integration of formal methods into software engineering practices. - Combination of formal methods with simulation and analysis techniques - Formal methods and fault tolerance, resilient computing, and self healing systems - Formal methods and graphical modeling languages such as SysML, UML, MATLAB/Simulink - Formal methods and autonomy, e.g., verification of systems and languages for planning and scheduling (PDDL, Plexil, etc.), self-sufficient systems, and fault-tolerant systems. Formal methods in practice - Experience reports of application of formal methods on real systems, such as autonomous systems, safety-critical systems, concurrent and distributed systems, cyber-physical, embedded, and hybrid systems, fault-detection, diagnostics, and prognostics systems, and human-machine interaction analysis. - Use of formal methods in systems engineering (including hardware components) - Use of formal methods in education - Reports on negative results in the development and the application for formal methods in practice. - Usability of formal method tools, and their infusion into industrial contexts. - Challenge problems for future reference by the formal methods community. The formulation of these papers can range from plain English description of a problem over formal specifications, to specific implementations in a programming language. NASA OPEN SOURCE Courageous authors, who want to delve in open source software being applied in real NASA missions, and find possible connections to and applications of Formal Methods, are invited to visit the open source repositories for the following two frameworks for
[TYPES/announce] Postdoc position at the University of Lisbon
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] University of Lisbon -- One Post Doctoral Research Fellowship We are looking to fill one post-doctoral research fellowship in the area of programming languages, type systems and logics. The position is funded by the research project "SafeSessions - Safe Concurrent Programming with Session Types", https://urldefense.com/v3/__https://www.lasige.pt/project/safesessions/__;!!IBzWLUs!A2S_14d2AW5szG565PdsS_-WGxz9tgiyFXWyJtiRYtTTta3AONbI602l85wghr-phhaVjb_UCBGYxw$ . We seek applicants with strong interest in some of the following topics: programming language design and implementation, logics and types, concurrency and distribution. Applicants should hold a PhD degree in Computer Science or related area. The position is funded by the Foundation for Science and Technology for an initial period of 12 months, renewable until the end of the project (February 29, 2024 or six months thereafter). Applications are open until February 15, 2022. The complete offer description can be found at https://urldefense.com/v3/__https://www.euraxess.pt/jobs/721789__;!!IBzWLUs!A2S_14d2AW5szG565PdsS_-WGxz9tgiyFXWyJtiRYtTTta3AONbI602l85wghr-phhaVjb8bu0XBiQ$ . Further information can be obtained from lasige-candidatu...@listas.di.ciencias.ulisboa.pt. Applicants are encouraged to contact Professor Vasco T. Vasconcelos directly. About the University of Lisbon and the LASIGE research lab The University of Lisbon (ULisboa) is the largest university in Portugal and a leading one within wider Europe. Comprising eighteen faculties, ULisboa offers 400 degree programmes at undergraduate and postgraduate level. Each year it accepts more than 5,000 international students – around 10% of its total cohort – who represent 100 different countries. ULisboa leads the main international rankings, is amongst the 200 best universities worldwide according to the 2019 Shanghai Ranking. LASIGE, https://urldefense.com/v3/__https://www.lasige.pt__;!!IBzWLUs!A2S_14d2AW5szG565PdsS_-WGxz9tgiyFXWyJtiRYtTTta3AONbI602l85wghr-phhaVjb-lI63vlA$ , is a research unit at ULisboa evaluated as Excellent by the Portuguese Science Agency (FCT) in 2018, with a perfect score of 15 points. LASIGE closely mentors more than 100 young researchers (at masters, doctoral, and post-doctoral level), continually stimulating excellence in research. LASIGE members teach MSc and PhD level courses in Computer Science and Engineering (CSE) at ULisboa, regularly publish in top venues, and enjoy top-notch bibliometric indices. LASIGE runs a large number of international projects, boasts three spin-offs, and multiple technology transfers. The high-level research conducted at LASIGE, the scientific background and international projection of its group leaders, the academic and industrial network to which it belongs, and the experience in advanced training of its members makes LASIGE the perfect research unit to work as a postdoc. If this was not enough, the city of Lisbon offers history and culture, shopping, restaurants, nearby beaches and a vibrant nightlife.
