Apple • Meta • Amazon Prime Video • Amazon Web Services • CertiK • IBM Research • JaneStreet • Uber • Futurewei Technologies, Inc. • Certora • Veridise Inc.

---

Apple

Apple has a long history of investing in programming languages, program analysis, and a wide range of developer tools as technologies that underpin Apple’s product and software ecosystem.

Company Contact: Ted Kremenek kremenek@apple.com

Positions:

• C++ Compiler Engineer The C Languages & Libraries and Security Tools teams at Apple are looking for software engineers with expertise in C++ language design and compiler implementation to develop and enhance the Clang compiler. Our team works with security, performance, and operating system engineers across Apple to help shape the future of our platform through languages and tools. As an engineer on the team, you will be involved in all aspects of taking a language feature from concept to implementation to deployment. We are active contributors to Clang and LLVM as well as other programming language communities.

• Compiler Tools Engineer Apple’s compiler team is looking for a Cloud infrastructure engineer to drive tooling for open source and internal compiler technologies. We want to minimize the latency and engineering effort to deploy changes in the Swift and Clang compilers and the LLDB debugger, while maintaining (and improving!) our Cloud infrastructure. We believe that continuous deployment of toolchain technologies will substantially increase the compiler team’s productivity, as well as the productivity of our internal users.

• Debugger Engineer The LLDB team within Apple’s Developer Tools organization is looking for an engineer to work on the debugger. LLDB is a core part of Apple’s developer tools, used internally to debug Apple’s software stack and externally by millions of developers. Our team works across many different organizations to deliver a state-of-the-art debugging experience to all our users. You will be working as part of a highly skilled engineering organization in the exploration, design, and implementation of new ideas that will drive the future of Apple’s technology and tools.

• GPU Backend Engineer — Performance As a member of the Apple Silicon GPU Compiler Backend Performance Team, you’ll implement improvements to the open-source LLVM mid-level optimizer as well as our LLVM-based machine-dependent code generator for Apple’s GPU. This may include improving the performance of generated code, compile time, and maintainability of the code, as well as implementing new features driven by changes to the Metal API and shading language. We are looking to hire for both an entry-level position and a senior position.

• GPU Backend Engineer — Pre-Silicon As a member of the compiler backend team you will design and implement new features and performance optimizations needed for future Apple GPUs. You will join a small team with diverse talents and ample room for growth that works on every Apple Silicon GPU we ship in different devices including iPhone, iPad, Apple W atch, Apple TV and Macs. You will be able to influence and help design new GPU architectures. You will work and collaborate cross-functionally with GPU archit ecture, silicon design, device driver and Metal API teams to develop the GPU HW and SW stack for Apple Silicon GPUs.

• Linker Engineer The dyld team is responsible for the technologies related to linking and loading executable files on Apple platforms (dyld, ld64, cc tools). As an engineer on the team, you will improve Apple’s linker tools to e link nsure that programs link and launch efficiently — and directly improve the user experience for all users of practically every device Apple ships. You will also collaborate with the compiler teams and engineers across Apple to improve the CPU and memory efficiency of software across the OS.

• Performance Compiler Engineer The CPU and Accelerator Compilers Team is looking for engineers passionate about working on advancing compiler performance and optimization technology. We are responsible for optimizations and code generation for CPUs and Accelerators on all Apple platforms. Our team works across many different organizations on state-of-the art, industry impacting technology that enhances the user experience for all Apple customers with better run-time performance, battery life, compile-times, code size or enhanced security. A lot of the team’s work happens directly in the LLVM open source project and gets presented at LLVM Developer Meetings and Apple’s WWDC conferences.

• Swift Compiler Engineer The Apple Swift Compiler group is responsible for evolving the Swift programming language and continuing to improve the performance, safety, and reliability of the Swift language. We are looking for engineers to help improve our translation of the Swift Intermediate Language (SIL) into LLVM IR. This will require you to develop a deep knowledge of SIL and LLVM IR, take responsibility for evolving our representations of functions and runtime type metadata, and will require you to work closely with LLVM, linker, loader, OS, and CPU experts to ensure the results are correct, compact, and efficient.

• Security Tools Compiler Engineer Apple’s compiler group is looking for engineers to implement compiler and language features to improve the security and safety of C, C++, and Objective-C. Our team works with security, performance, and operating system engineers across Apple to help shape the future of our platform through languages and tools. In addition to those interested in security tools, we are also looking for engineers with expertise i n C++ language design for those interested specifically in investing in security in C++ code.

• SwiftUI Frameworks Compiler Engineer DSLs and functional programming lie at the heart of declarative APIs such as SwiftUI, Swift Charts, and Swift Regex. As a member of the SwiftUI team, you will apply compiler technologies to help make UI DSLs more expressive and more performant than ever. You will also contribute to the open-source Swift programming language itself and draft proposals to Swift Evolution. You’ll collaborate with experts throughout Apple including: Swift compiler engineers, graphics engineers, programming language designers, and API designers. Curious and enterprising individuals who take an expansive view of their role will thrive in this multi-disciplinary environment!

Meta

Meta is seeking experienced Research Scientists and Software Engineers to join our teams. We will also be opening new graduate Research Scientist and Software Internship positions for 2023 soon. To learn more about careers in research at Meta visit www.research.fb.com/careers/

Our open culture and diverse teams of experts, along with our emphasis on academic collaboration and sharing model, deliver a unique chance to grow as a researcher and engineer while directly contributing new ideas and technologies that impact experiences of billions of people around the world.

Amazon Prime Video

The Prime Video App controls video playback for all Prime Video content. We use Automated Reasoning to make sure we provide the best experience to our customers on an application that has hundreds of components developed by dozens of teams worldwide in a range of programming languages, tech stacks and development patterns, and which runs on thousands of different hardware configurations.

Company Contact: Pauline Bolignano (Manager of the Prime Video Automated Reasoning team) pln@amazon.co.uk

Positions:

• Senior Applied Scientist, Prime Video Automated Reasoning Leadership role for program analysis expert to develop novel solutions to provide the best experience to Prime Video customers.
• Applied Scientist, Prime Video Automated Reasoning Critical contributor with program analysis experience to develop novel solutions to provide the best experience to Prime Video customers.
• Internships - please contact us

Amazon Web Services

AWS Automated Reasoning teams work at the intersection of theory and practice to drive scientific innovation and provide value for our customers. Our Applied Scientists are responsible for delivering tools that are called billions of times daily. Amazon development teams are integrating automated-reasoning tools such as Dafny, P, and SAW into their development processes, raising the bar on the security, durability, availability, and quality of our products. AWS customers now have access to automated-reasoning-based features such as IAM Access Analyzer, S3 Block Public Access, or VPC Reachability Analyzer. With these services, AWS Automated Reasoning teams are changing how computer systems built on top of the cloud are developed and operated.

Company Contact: Valerie Kolstad Tasiran (Senior Program Manager, Automated Reasoning) vkolstad@amazon.com

Positions:

• Applied Scientist, Automated Reasoning Work on cutting edge technology related to formal methods, automated reasoning, automated testing, and adjacent areas. Collaborate with fellow applied scientists to solve challenging problems that provide value to customers by improving the quality of software. You will have opportunities to publish your work.

• Applied Scientist, AWS Cryptography AWS Cryptography is looking for experts in reasoning on low-level code (e.g. C, LLVM, assembly) to contribute to the formal verification of cryptographic algorithm implementations.

• Applied Scientist, Privacy Engineering The mission of AWS Privacy Engineering is to make AWS the best computing service in the world for customers who require digital privacy.

• Applied Scientist, Program Synthesis Program Synthesis for AWS. Join a new group in AWS that builds novel program analysis and program synthesis techniques for securing and maintaining the code base of foundational AWS services.

• Applied Scientist, S3 Automated Reasoning Group Amazon’s Simple Storage Service (S3) offers industry-leading scalability, data availability, security, and performance. S3’s Automated Reasoning Group (S3-ARG) develops and applied automated reasoning techniques to deliver correct, secure, durable, and available distributed systems and storage services. S3 consists of hundreds of distributed micro-services that process millions of requests per second. Getting such a complex and fast-evolving system right requires developing cutting edge automated reasoning methods that are continuously integrated into the software development process. If you are interested in exploring, please e-mail s3-arg-jobs@amazon.com.

• Applied Science Internships, Ph.D. Students AWS Automated Reasoning teams work in areas including: Distributed proof search, SAT and SMT solvers, Reasoning about distributed systems, Automating regulatory compliance, Program analysis and synthesis, Security and privacy, Cryptography, Static analysis, Property-based testing, Model-checking, Deductive verification, compilation into mainstream programming languages, Automatic test generation, Static and dynamic methods for concurrent systems. Our teams are currently located in: Seattle, Bay Area, NYC, Boston, Minneapolis, Austin, Portland, London, Munich. Internships are available year-round.

CertiK

CertiK’s mission is to secure the Web3 world. We were founded in 2018 by professors at Columbia and Yale. CertiK is a pioneer in blockchain security, using best-in-class technology to secure and monitor blockchains, smart contracts, and Web3 apps.

Company Contact: David Tarditi, david.tarditi@certik.com

Positions:

• Software Engineer (all levels) - Tools You will design and develop tools that identify security issues or assist security auditors to locate blockchain security issues. We develop and apply technologies such as static analysis, model checking, fuzz testing, language-based security (such as type systems), automated program verification, and theorem-prover based program verification.

• Staff Software Engineer - Tools You will design and develop tools that help identify blockchain security issues. As a Staff Software Engineer, you will set the technical direction for solving problems and may lead a small team working on a tool or area. We develop and apply technologies such as static analysis, model checking, fuzz testing, language-based security (such as type systems), automated program verification, and theorem-prover based program verification. Your title and responsibilities will be commensurate with your experience and background.

• Internship Fall/Winter 2022 - Software Engineer, Tools You will design and develop software tools that help identify blockchain security issues. We develop and apply technologies such as static analysis, model checking, fuzz testing, language-based security (such as type systems), automated program verification, and theorem-prover based program verification. During your internship, you will have the opportunity to work in one of these areas or related areas, depending on your experience, interest, and project availability.

IBM Research

We’re a group of researchers, scientists, technologists, engineers, designers, and thinkers inventing what’s next in computing. We’re relentlessly curious about all the ways that computing can change the world. We’re currently obsessed with advancing the state of the art in AI and hybrid cloud, and defining the future of quantum computing.

Positions:

• Research Scientist The candidate will be working on applying AI techniques to improve the productivity of software development. The scope of the work includes using neural networks and/or program analysis techniques to perform code translation, code generation, code classification as well as other tools that can assist software programmers to develop, maintain, and debug code. The candidate will be inventing novel techniques and implement them as AI pipelines using Pytorch and/or Tensorflow. The innovations are expected to be published in top conferences/journals, disclosed as patents, and/or transferred to IBM’s business units as impactful products.

Jane Street

Jane Street is a quantitative trading firm with offices worldwide. We hire smart, humble people who love to solve problems, build systems, and test theories. You’ll learn something new every day in our office—whether it’s connecting with others to share perspectives, participating in a talk, or game night. Our success is driven by our people and we never stop improving.

Company Contact: jobs@janestreet.com

Positions:

• Software Engineer, NYC We’re always hiring software engineers for all three of our offices. Technology is at the core of how we approach our work, and engineers are intimately tied into every area of the business. We are big believers in functional programming, using OCaml, a statically-typed functional programming language, as our primary development language. We also believe in the value of open source software, using it in our daily work and releasing hundreds of thousands of lines of our own code as open source.

• Software Engineer, LDN We’re always hiring software engineers for all three of our offices. Technology is at the core of how we approach our work, and engineers are intimately tied into every area of the business. We are big believers in functional programming, using OCaml, a statically-typed functional programming language, as our primary development language. We also believe in the value of open source software, using it in our daily work and releasing hundreds of thousands of lines of our own code as open source.

• Software Engineer, HKG We’re always hiring software engineers for all three of our offices. Technology is at the core of how we approach our work, and engineers are intimately tied into every area of the business. We are big believers in functional programming, using OCaml, a statically-typed functional programming language, as our primary development language. We also believe in the value of open source software, using it in our daily work and releasing hundreds of thousands of lines of our own code as open source.

• Tools & Compilers Research Internship, LDN We’re looking for PhD and masters students with outstanding research experience in programming languages, compilers, verification, and related areas. Jane Street’s Compilers team focuses on improving OCaml as a foundation for Jane Street’s ever-growing technology stack, in collaboration with the greater OCaml community. During the internship, you’ll learn how we use OCaml in our day-to-day work, gain exposure to the libraries and tools that are foundational to our internal systems, gain a better understanding of the wide range of problems we solve every day, and try out new ideas and apply state-of-the art research to a large actively-developed production codebase.

• Tools & Compilers Research Internship, NYC We’re looking for PhD and masters students with outstanding research experience in programming languages, compilers, verification, and related areas. Jane Street’s Compilers team focuses on improving OCaml as a foundation for Jane Street’s ever-growing technology stack, in collaboration with the greater OCaml community. During the internship, you’ll learn how we use OCaml in our day-to-day work, gain exposure to the libraries and tools that are foundational to our internal systems, gain a better understanding of the wide range of problems we solve every day, and try out new ideas and apply state-of-the art research to a large actively-developed production codebase.

• FPGA Engineer, LDN We are looking to hire a Engineers with experience in both software and hardware design to work on FPGA-based applications, and on tools for creating such applications. We’re big believers in the ability of tools to make programming faster, more pleasant, and more reliable. We think the same is true for hardware design, and we’re looking for people with real world experience who are interested in using programming language technology to improve the process of designing, testing and validating hardware designs. Day to day work will involve OCaml & Hardcaml, for both RTL design and testing/integration. Engineers will also work with some Verilog and C.

• Developer Experience Engineer, NYC We are looking for a Software Engineer to act as the primary liaison between our other Software Engineers and users of our tools throughout the firm. This role is for someone who loves helping people and solving problems. Approximately half of your job would be to act as a tools Engineer, contributing to a wide variety of tools, including text editor plugins, our code-review system, and the Dune build system. We’d also want you to spend time learning about engineering processes across the firm; this will involve rotating through different teams in order to understand their challenges and help them onboard new tools and processes. You’d have a role in helping us plan and prioritize our work, helping us understand engineering needs across the firm, and using that knowledge to prioritize our project stack accordingly.

Uber

At Uber, we reimagine the way the world moves for the better. The idea was born on a snowy night in Paris in 2008, and ever since then, our DNA of reimagination and reinvention carries on. We’ve grown into a global platform moving people and things in ever-expanding ways, taking on big problems to help drivers, riders, delivery partners, and eaters make movement happen at the push of a button for everyone, everywhere. We welcome people from all backgrounds who seek the opportunity to help build a future where everyone and everything can move independently. If you have the curiosity, passion, and collaborative spirit, work with us, and let’s move the world forward together.

Company Contact: rajbarik@uber.com

Positions:

• Software Engineer, PhD Job Description: Uber Engineering is growing quickly as we look to take on some exciting opportunities at scale and around the world. As we grow our team and code base, there is a growing need for automatic analysis tools to keep our code quality and performance high while ensuring our engineers can continue to adapt quickly. To support this need, the Programming Systems Group is looking for hardworking engineers to develop new optimizations, static and dynamic analysis tools, and programming models, and apply them to Uber’s code base. You should also be passionate about writing clean, efficient, and well-tested code.

Futurewei Technologies, Inc.

Futurewei focuses research on advanced information and communications technology (ICT) domains that will benefit an intelligent and digital society. By focusing on open innovation beyond traditional ICT industry, we aim to advance these technologies into real world solutions through standardization, open-source collaboration and partnering with industrial ecosystems.

Company Contact: Smita Baruah sbaruah@futurewei.com

Positions:

• Rust Compiler Sr. Staff Engineer 8+ years software development experience; Thorough understanding of compilers and related tool chains; Solid programming skills in Rust and/or C, C++, assembly language; Solid skills on performance analysis and performance improvement; Motivated and effective in acquiring new knowledge; Excellent teamwork and communication skills; Proven track record of significant open-source contributions, especially in Rust related communities is preferred; MS/PhD or equivalent in computer science or EE preferred; Location: Santa Clara, CA

Certora

Certora is a leader in automated software verification, currently focusing on the security and correctness of smart contracts. Decentralized Financial Applications (DeFis), which are one of the most common applications of smart contracts, are already worth 200 billion USDs. Our customers are some of the top DeFi protocol innovators; they develop smart contracts that are invoked by end-users to execute financial transactions. Providing formal correctness guarantees for smart contracts is critical because any bugs can be exploited by malicious users leading to losses at the scale of millions or even billions of USDs. Certora is the only company that provides automated techniques for verifying smart contracts with no false alarms, strong formal correctness guarantees, and full automation. Our team currently consists of world-class experts in formal verification who are developing next-generation formal verification techniques. We are actively hiring for various roles that require a strong background in formal verification, programming languages, and software engineering.

Company Contact: Aviva Gatt, aviva@certora.com

Positions:

• Software engineer Language Design Develop the syntax and type system of a declarative programming language for specifying correctness properties of smart contracts. Collaborate with world-class computer scientists and researchers working at Certora to drive fundamental research in formal methods and software verification. Communicate research ideas both internally and externally through lectures, talks, and publications at academic and industrial conferences. Gradually educate yourself and get hands-on experience in various areas of software verification to eventually become a true expert in this area.

• Software engineers formal verification SMT Develop a novel and reliable program verification tool leveraging automated reasoning, static analysis, abstraction, and SMT solving to verify real programs. Collaborate with world-class computer scientists and researchers working at Certora to drive fundamental research in formal methods and software verification. Communicate research ideas both internally and externally through lectures, talks, and publications at academic and industrial conferences. Gradually educate yourself and get hands-on experience in various areas of software verification to eventually become a true expert in this area.

Veridise Inc.

Veridise is a new security auditing company for DeFi applications. Veridise technology is based on cutting edge formal verification research and can provide formal correctness and security guarantees in a cost- effective way. We are a 100% remote company offering competitive salaries and amazing benefits! To learn more about Veridise, watch our online demos or request a security audit by visiting www.veridise.com.

Company Contact: To be considered, please fill out our general application. You may also email Samantha Oglesby, Chief of Staff, contact@veridise.com with any questions.

Positions:

• Security Software Engineer (Remote/US/Europe/China) Veridise is developing cutting-edge tools for guaranteeing correctness of DeFi software and blockchain infrastructure. We are looking for security engineers who can collaborate with clients to advise them on the security of their source code. This will involve inspecting the code both manually and with the aid of our tools. In addition, security engineers will be responsible for writing formal behavioral specifications and using our verification tools. This position will require a close collaboration with Veridise engineers who will be developing tools to help automate the auditing process

• Software Engineer, Compiler (Remote/US/Eurpoe/China) Veridise Inc is seeking a Compiler engineer to join our product development team. We’re looking for a candidate who is passionate about programming languages, compiler tooling, and program analysis. Our team focuses on automated analysis of blockchain programs, so the ideal candidate should be familiar with program analysis and common analysis requirements (pointer analysis, SSA, dependence analysis), familiar with all parts of the compiler infrastructure (language front-ends, optimizations, tooling, code generation) and interested in blockchain languages/platforms. They should also have good interpersonal skills as they will be working along-side our analysis teams. In addition, our infrastructure is currently based on LLVM, so candidates with LLVM experience are strongly preferred.