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.

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