Inspiration
Models of computation are a fundamental concept of computer science. Therefore almost every CS-student will encounter these models at some point in their studies. We want to help students gain a deeper understanding of the computation model primitive recursive functions (Primrec).
What it does
We built a website, where users can define Primrec functions and compute their results for a given input. Furthermore, users can define postconditions for the functions which we then try to automatically verify.
How we built it
We defined a custom language to input Primrec functions and built a parser. The website is built with React and Typescript. We used Web technologies like Typescript and Supabase to built a website for defining and
Challenges we ran into
Figuring out the translation algorithm converting Primrec functions into Constrained Horn Clauses (logic formulas in a specific form) in order to let the Eldarica solver determine the correctness of the user-defined postconditions.
Accomplishments that we're proud of
The Parser for our custom Primrec language as well as the translation algorithm.
What we learned
We gained a deeper understanding of the computer science concepts Constrained Horn Clauses and Primitive recursive functions.
Source Code
The source code for this project is completely public for anyone to see at https://github.com/formallyverifiedprimrec
Built With
- c#
- eldarica
- supabase
- typescript
Log in or sign up for Devpost to join the conversation.