amutake/actario

---

amutake/actario.json

{
  "createdAt": "2014-12-14T02:03:08Z",
  "defaultBranch": "master",
  "description": "Verification Framework for Actor Systems on Coq",
  "fullName": "amutake/actario",
  "homepage": "",
  "language": "OCaml",
  "name": "actario",
  "pushedAt": "2018-07-02T06:18:54Z",
  "stargazersCount": 29,
  "topics": [],
  "updatedAt": "2022-04-22T22:25:48Z",
  "url": "https://github.com/amutake/actario"
}

![logo]!(./img/logo-mini.png) Actario

Actario is a framework to formalize and verify Actor systems on Coq. This project is under development.

Actario = Actor + Scenario

Requirements

• coq-8.8
• mathcomp-1.7

Install

$ cd /path/to/actario
$ ./configure
$ make
$ make install

Examples

See [examples]!(./examples).

Current status

• Formalization of Actor model’s syntax and semantics
  • syntax: new, send, self, become (theories/syntax.v, actions)
  • semantics: labelled transition semantics (theories/semantics.v, trans)
• Convenient notation
  • theories/syntax.v
• Proof of no duplication of Actor names
  • theories/trans_invariant.v (initial_trans_star_no_dup)
• Mechanisms/Lemmas for verifying Actor systems
• Communication between configurations
• Extraction to Erlang
  • Equivalence between Actario’s semantics and Erlang’s semantics is not proven
• Supervisor
• Practical examples

License

LGPL 2.1

Papers

• [AGERE!@SPLASH2015]!(./papers/AGERE2015.pdf)