Create Reference Book: "Formal Verification for RhoLang"

[golovach-ivan]

Collect in systematic way all academic information on topic "Formal Verification for RhoLang" in the format of a Reference Book.
Chapters

• Process Algebras/Calculus
• Process Logics
• Pi-Calculi with extensions
• Type Systems: Behavioral / Spatial
• Namespace Logic examples
• Formal Verifications: Algorithms and Tools

Benefit to RChain

• formal verification community development
• formal verification tech books library development

Budget and Objective

Estimated Budget of Task: $[depends on actually done work]
Estimated Timeline Required to Complete the Task: [3-6 month]
How will we measure completion? [versions of pdf committed to google docs]

[AyAyRon-P]

@golovach-ivan I can do the layout design of this and generate interactive PDFs. Let me know if you'd like to collaborate on this issue.

[dckc]

@golovach-ivan please discuss this with potential collaborators such as @JoshOrndorff @Jake-Gillberg @pyrocto .

@JoshOrndorff , @Jake-Gillberg @pyrocto note work in progress in https://github.com/golovach-ivan/Correct-by-Construction , including what looks like an outline: https://github.com/golovach-ivan/Correct-by-Construction/tree/master/dict

[dckc]

@golovach-ivan any progress on connecting with potential collaborators?

[golovach-ivan]

As first results of this issue in Sep-Oct i'm going to compare Formal Verification aproaches for RhoLang

• 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).

1. Hold Meetup (Meetup: Formal Verification aproaches for RhoLang #1005)
2. Publish report

[dckc]

@golovach-ivan it's been over a month since I asked that you find collaborators. What's going on?!?!?!