wiki:WikiStart

F5 Toolchain for RCF

F5 is a toolchain for Refined Concurrent FPC (RCF) including a type-checker with union, intersection, and polymorphic types, as well as static reasoning about type disjointness, and a user-friendly GUI for examining typing derivations; an automatic code generator for symbolic implementations of zero-knowledge; a visual debugger, and more.

Papers

Formalization

Download Coq formalization of our calculus, type system and soundness proof by Cătălin Hriţcu. Works with Coq 8.2.

Implementation

Download F5 tool-chain for RCF by Thorsten Tarrach and Cătălin Hriţcu  Apache License, Version 2.0.

Screenshots

http://www.infsec.cs.uni-saarland.de/projects/f5-releases/Screenshots/Failure001.png http://www.infsec.cs.uni-saarland.de/projects/f5-releases/Screenshots/Failure002-Z3.png http://www.infsec.cs.uni-saarland.de/projects/f5-releases/Screenshots/Failure002-eprover.png http://www.infsec.cs.uni-saarland.de/projects/f5-releases/Screenshots/Success001.png http://www.infsec.cs.uni-saarland.de/projects/f5-releases/Screenshots/Debugger.png

Bug Tracker

Because of a recent spam wave you need to be logged-in to create new tickets. If you need an account or want to report a bug directly please contact catalin.hritcu@….