C Compiler Front-End Engineer

Runtime Verification Inc. is a technology company headquartered in Urbana, Illinois with staff spread across the globe. We provide testing and verification services to public and private companies in the embedded and blockchain domains. In the latter we work with infrastructure builders as well as companies building products and providing services supported and/or powered by said infrastructure.

Company mission

Our mission is to support and scale accessible, trustworthy computing. We accomplish this by generating correct-by-construction implementations and tools automatically, from their specifications. One of our unique technologies is K, a semantic framework for design, implementation and formal reasoning. It allows language designers to formally define their language using an intuitive and attractive notation, and generate for free the implementations and the analysis tools for that defined language.

Job description

Runtime Verification Inc (RV) is looking for a C Compiler Front-End Engineer to develop a proprietary, closed-source compiler for C programs based on formal methods technologies and the K Framework. The ideal candidate has extensive experience with the ISO standard for the C programming language and experience developing on a C compiler front-end. Successful hires will contribute to our existing compiler and improve its ability to correctly compile and run real-world embedded C code that has been simulated in a desktop environment. The selected individual will be responsible for:

  • Maintaining, fixing bugs, and developing new features for our C compiler that forms the core of our RV-Match tool for software analysis of C code.
  • Implementing missing features of the C programming language and instrumenting our C interpreter with information needed to detect undefined behavior in the program being compiled.
  • Building out our formal methods tools for performing dynamic, symbolic analysis and model-checking of C programs.
  • Writing code in K, a functional programming language, that compiles and interprets C programs.

Experience with compiler optimizations and compiler back-ends that target native code generation is not a major focus of this position.

What we offer

What we offer banner image
One of the best teams around

One of the best teams around.

Competitive salary

Competitive salary.

Remote friendly

Remote friendly.

Matching IRA contributions

Matching IRA contributions.

Casual dress code

Casual dress code.

Health insurance

Health insurance.

Top notch equipment

Top notch equipment.

Performance bonuses

Performance bonuses.

Company lunches

Company lunches.

Unlimited vacation

Unlimited vacation.

Must have

  • B.S. in Computer Science or equivalent (M.S. or Ph.D. in fields relating to compilers is even better)
  • 5+ years industry experience writing code in C with an understanding of undefined behavior and its consequences.
  • A history of development that includes at least one accepted patch into the compiler front-end of a C or C++ compiler.
  • Familiarity with functional programming.

Nice to have

  • Experience as a maintainer of a C or C++ compiler front-end.
  • Industry experience writing code in a functional programming language like Haskell, OCaml, Scala, etc.
  • Knowledge of formal methods, mathematical logic, or term rewriting.
  • Experience with the formal verification of C code.
  • Knowledge of and familiarity with embedded software development.
  • Experience developing and writing compiler diagnostics.
  • Familiarity with using libffi.

What’s in it for you?

  • Opportunity to work at the forefront of programming language design and verification.
  • Casual work environment with flexible work hours.
  • Full benefits package available for US based employees. Includes unlimited paid time off, retirement benefits, employer sponsored health / dental / limited life insurance.

How to apply

company mission and vision news team careers publications presentations videos faq Embedded Systems Blockhain Advisory Services Smart Contract Verification Protocol Verification Formal Design and Modeling The IELE Virtual Machine Partnerships contact media kit blog