K Project Needs Professional Developers
The K framework team is looking for five R&D professionals to advance the implementation of the K framework in the open source space. Currently, there are two implementations:
UIUC-K is richer in features, being able to do symbolic execution and deductive program verification based on a given language semantics. RV-K provides a much faster concrete execution engine. Our objective is to combine these two versions into one version of K capable of both concrete and symbolic execution. We expect the new version to be one order of magnitude faster than RV-K on concrete program execution, making it close in performance or even exceed adhoc implementations of the target language. Also, the new version will implement several additional features to the framework, all language-independent, such as: semantics-based compilation; bounded symbolic model checking; deductive program verification; test-case generation. Additionally, we eventually want to be able to generate proof certificates from any successful verification effort, reducing trust to only the formal semantics of the target programming language, which should be open source and thus available to the scrutiny of the entire scientific community. Several existing or started K language semantics will also need to be completed and migrated to the new version of K. Also, the semantics of several programming languages will need to be defined, specially of ones used for smart contracts on the blockchain or for embedded platforms.
The successful candidates will work closely with R&D professionals in the following institutions:
The successful candidates must be outstanding programmers in both object-oriented and functional languages. They must also enjoy brainstorming, doing research and writing papers. We eventually aim at publishing the results of our work in top-tier conferences. If you are interested, please contact us at:
To see if you qualify, we strongly encourage you to take the following challenge:
If you are confused about what this challenge is asking from you, or don't know how to do it, then there is a good chance that you do not qualify for any of our job openings. Currently, there are two job openings at RV, two job openings at iOHK, and one job opening at ADSC. ADSC hire must have a PhD in computer science or engineering completed, and his/her physical presence is required at ADSC, so must be willing to move to Singapore.