Applpi is a library in the Coq proof assistant that enables concurrent programs to be modeled and verified in Coq, and the models to be run as OCaml programs. It contains a formalization of a concurrent language based on the pi-calculus, a formalization of a specification language based on spatial logic and lemmas for formal verification. Applpi has been applied to the verification of an HTTP server.

Here are some references:

- Reynald Affeldt and Naoki Kobayashi, A Coq library for verification of concurrent programs, Electronic Notes in Theoretical Computer Science, 199:17-32, 2008 (preprint, Elsevier Science direct)
- Reynald Affeldt and Naoki Kobayashi, Partial order reduction for verification of spatial properties of pi-calculus processes, Electronic Notes in Theoretical Computer Science, 128(2):151-168, 2005 (preprint, extended version, Elsevier Science direct)
- Reynald Affeldt, Naoki Kobayashi and Akinori Yonezawa, Verification of concurrent programs using the Coq proof assistant: a case study, IPSJ Transactions on Programming, 46(SIG 1):110--120, 2005 (preprint, IPSJ Digital Courier)

The whole library: applpi.tar.gz.

Modeling and specification language:

- chan.v: definition of channels
- eqdep.v: dependent equality
- chanlist.v: library to manipulate lists of channels
- set.v: sets of channels (lists without duplicated channels)
- applpi.v: syntax of applpi with linearized channels, definition of the labeled transition system and reductions
- fresh.v: some lemmas about freshness
- redseq.v: definition of reduction sequences (include the definition of a second labeled transition to define fairness)
- cong.v: structural congruence
- logic.v: basic spatial and temporal formulas
- free_chans.v: some properties of the reduction systems w.r.t. free channels

Collection of lemmas:

- Injection and inversion properties:
- inj.v: injection lemmas (require John Major equality because of dependent types)
- inv.v: inversion lemmas for the first labeled transition relation (proved by induction, the Inversion tactic apparently fails because of dependent types)
- inv_dis.v: inversion/discrimination lemmas for the first labeled transition relation
- inv2.v: inversion lemmas for the second labeled transition relation
- inv2_dis.v: inversion/discrimination lemmas for the second labeled transition relation
- trans_trans2.v: relations between the two labeled transition systems

- Properties of structural congruence:
- cong_tactic.v: tactic to decide structural congruence in simple cases
- cong_inj_dis.v: in and out are not structurally congruent, if in c and in d are structurally congruent then c=d, etc.
- cong_resp.v: structural congruence is a bisimulation, and derived corollaries
- cong_trans.v: transitions / structural congruence
- cong_resp2.v: harmony lemmas for the second labeled transition system
- cong_trans2.v: transitions of the second labeled transition system / structural congruence

- Stability properties:
- stable.v: how to infer that a process is stable, etc.
- stable_tactic.v: tactic to prove that a process is stable

- Properties of formulas:
- logic_prop.v: formula properties (idempotence, distributivity, occurrence checks)
- logic_tactic.v: tactics to prove simple spatial formulas
- logic_tactic2.v: tactics to prove that a property does not depend on structural congruent rearrangement

- Reduction and confluence properties:
- red_deter.v: deterministic reductions
- conf_red.v: confluence properties
- conf_red_new_tactic.v
- conf_red_com_always_tactic.v
- red_nondeter.v: nondeterministic reductions
- red_nondeter_tactic.v

Miscellaneous:

- util.v
- listT.v: lists at the Type level at the Type level
- myclassic.v: some classical results at the Type level
- datatypes_for_tactics.v: datatypes used in tactics
- util_for_tactics.v: meta-level functions used in tactics

A mail server written in applpi:

- SMTP_applpi.v: The model of the mail-server
- SMTP_applpi_spec.v: The specification of one property
- SMTP_th1.v: Formal proof

We use a simple example to show how we can run applpi programs using the Ocaml environment:

- exa_client_server.v: verification of a simple client/server interaction
- interpret.ml: ML semantics of concurrent primitives
- client_server.ml: ML code generated by Coq for the simple client/server above
- client_server_pretty.ml: the same as above with minor syntactical changes (simply replacing capitals letter of ML type constructors, according to the rules below)
- rules.ml
- Makefile

This extension to the specification language compiles with the library above but it cannot be used safely with the lemmas based on confluence properties:

- logic_extensions.v: additional formulas (including a fixed point operator)
- mu.v: fixed point theory and a sample equivalence proof