Skip to content
This repository has been archived by the owner on Jun 17, 2020. It is now read-only.

Meetup: Formal Verification aproaches for RhoLang #1005

Open
golovach-ivan opened this issue Oct 18, 2018 · 2 comments
Open

Meetup: Formal Verification aproaches for RhoLang #1005

golovach-ivan opened this issue Oct 18, 2018 · 2 comments

Comments

@golovach-ivan
Copy link

golovach-ivan commented Oct 18, 2018

Hold Meetup: Formal Verification aproaches for RhoLang (Europe/Ukraine).
Explain and compare 5 different ways

  • Interactive Theorem Provers (write the specification as an independent mathematical theorem).
  • Contracts (encode the specification as assertions, pre/post conditions).
  • Barbed Bisimulation (write the specification as an simplified program in the same language).
  • Modal/Separation Logics (encode the specification as logic formulae).
  • Kobayashi Type Systems for Process Calculi (encode the specification into channels types).

This issue is result of #945 research activity.

Benefit to RChain

Budget and Objective

Involved

golovach.ivan - 75%
kovmargo - 25%

Expenses

Publicity, Banners, Digital graphics $100
Hall renting $100
Camera and associated gadgets renting + video processing $150
Logistics $50
Slides development - golovach.ivan time
Speech/Info preparing - golovach.ivan time
Video processing consultancy, organization - kov.margo time

Estimated Budget of Task: $[2000]
Estimated Timeline Required to Complete the Task: [1week]
How will we measure completion? [processed video uploaded to Youtube channel + slides uploaded to #779 ("meetup in the box" issue) google directory

@Ojimadu
Copy link
Contributor

Ojimadu commented Oct 20, 2018

@golovach-ivan, Have you gotten any sponsor for this? If No, please don't proceed until someone from the marketing organization supports this with a budget.

@dhsorens
Copy link

dhsorens commented Oct 26, 2018

@golovach-ivan A reference book is under way in the rchain/Rholang directory. I would be very interested in getting involved in anything that happens here, as I am building the formal semantics of Rholang for precisely this purpose. Feel free to contact me on discord at @ Derek.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants