Skip to content
<awesome-gh-repos>
vic

amutake/actario

Verification Framework for Actor Systems on Coq
Source code at GitHub https://github.com/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

Section titled “![logo]!(./img/logo-mini.png) Actario”

wercker status

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

Actario = Actor + Scenario

Requirements

Section titled “Requirements”
  • coq-8.8
  • mathcomp-1.7

Install

Section titled “Install”
Terminal window
$ cd /path/to/actario
$ ./configure
$ make
$ make install

Examples

Section titled “Examples”

See [examples]!(./examples).

Current status

Section titled “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

Section titled “License”

LGPL 2.1

Papers

Section titled “Papers”
  • [AGERE!@SPLASH2015]!(./papers/AGERE2015.pdf)