Software Engineer (Formal Methods)

Join our team as a Software Engineer specializing in Formal Methods. In this role, you will extend the scope and depth of our automated program verification tools, adapt and improve algorithms for symbolic software model checking, and build and extend translators from different input languages into intermediate representations. You will also identify new classes of security properties of smart contracts and collaborate closely with other software engineers to set technical direction and deliver working software that meets customer needs.

Missions

• Extend the scope and depth of automated program verification tools, and design and implement new tools.
• Adapt and improve algorithms for symbolic software model checking, including bounded model checking and property directed reachability.
• Build and extend translators from different input languages into intermediate representations, optimizing the generated models for automated analysis.

Profil recherché

- Master's Degree in Computer Science or a related field or 5 years of equivalent experience

- Demonstrated knowledge of fundamental computer science concepts such as data structures, algorithms, mathematical logic, and automata theory

- Minimum of 2 years of experience with one or more of the following: model checking, formal verification, SAT/SMT solving (Z3, CVC4, Yices, MathSAT, SMTInterpol), abstract interpretation, or closely related disciplines

- PhD in the broader field of automated reasoning

- Publication record in conferences like POPL, CAV, TACAS, FMCAD, FM, etc

- Experience in functional programming (OCaml or Haskell)

- Strong and creative problem-solving skills; always willing to learn and embrace new technologies and to collaborate

- Prior experience in a professional software development environment