Applpi

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.

1. Library overview
2. Case study
3. Execution of applpi programs as OCaml programs
4. Extensions

Library overview

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

Case study

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

Execution of applpi programs as Ocaml programs

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

Extensions

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