RV-Match



An ISO-compliant compiler for C and C++ capable of detecting a broad range of undefined and unspecified behavior in applications. Its use has discovered bugs in many software projects. It is based on an underlying technology capable of a variety of software analysis applications, including program verification, bounded model checking, and more.



RV-Predict



A code instrumentation engine for C/C++ and Java which can be used to detect and debug race-conditions in a variety of software applications, regardless of whether the race condition actually occurs within the execution being instrumented.



RV-Monitor



A runtime-monitoring library for C/C++ and Java which can not only detect when your software system has entered into an undesirable state with a variety of formalisms for defining properties that must not be violated, but which can also take corrective actions to restore the correct state in a manner which can be found to be provably-correct using software verification systems.



If you are interested in working with us, we are looking for someone with the following skills:



Responsibilities

• Work in a flexible environment with a very small team of engineers, in which you may be required from time to time to switch focus between several different projects.


• Develop code in C, C++, Java, OCAML, and a domain-specific programming language (K) which extends the functionality of code designed to detect software reliability issues.


• Analyze the performance of applications in order to reduce their runtime overhead.


• Work with formal methods techniques in order to develop tools which combine the boundaries of academic research with a firm foundation in usability and industry viability.

You will report directly to the lead software engineer, but we are seeking a candidate who can work relatively independently and demonstrate initiative and the ability to quickly gain experience in our core technologies. A candidate who does well on the job will have strong potential for advancement within the company.



Required Skills

• B.S. in Computer Science or equivalent experience.


• 2+ years industry or graduate-level experience programming in an object-oriented language like C++ or Java, and a willingness to learn Java if necessary.


• Familiarity with writing code in a functional language like OCAML, and a willingness to learn OCAML if necessary.


• Familiarity with the fundamentals of developing software on the Unix/Linux platform.


• Ability to work well with others and work where necessary and under the agreed-upon constraints.

Bonus Skills

• Candidates with an M.S. or Ph.D. in formal methods or programming language who can demonstrate their skill at development would be considered very valuable.


• Advanced knowledge of C/C++, or a candidate who demonstrates the ability to learn such skills, strongly desired.


• Industry experience developing in Java and OCAML preferred, but experience with another object-oriented and functional language is acceptable.


• Familiarity with multi-threaded code execution and memory models.


• Familiarity with optimizing and profiling the performance of applications.


• Knowledge of static analysis, dynamic analysis, program verification, or other formal tools for analysis of software reliability is a plus.


• Strong familiarity with writing and speaking in the English language desired, but fluent non-native speakers are acceptable.