1. Guillaume Claret
  2. fu_logic

Source

fu_logic /

Filename Size Date modified Message
49 B
16.9 KB
8.3 KB
155 B
117 B
354 B
8.2 KB
11.9 KB
622 B
6.6 KB
7.2 KB
5.2 KB
176 B
Coq formalization of Fu's temporal logic for concurrent programs :
*Still under development*

The goal is to give a Coq formalization of this paper :
http://flint.cs.yale.edu/publications/roch.html
to verify the soundness of the logic, and use it to prove several algorithms.

Files :
- Main.v : common libraries
- ProgramData.v : separation algebra and program syntax
- Assertion.v : state and trace assertions (semantics and properties)
- ProgramSemantics.v : program operational semantics
- SequentialProof.v : rules on sequential programs and soundness
- ConcurrentProof.v : rules on concurrent programs and soundness