Verification via Supercompilation

Alexei Lisitsa - Andrei Nemytykh

Supercompilation, or Supervised Compilation is a technique for program specialization, optimization and, more generally, program transformation[26,28,21,19]. Recently we have found new applications of supercompilation for verification of parameterized systems and protocols. This page is going to keep a record of all developments in this new exciting area. See also additional information at SCP4: Verification of Protocols web page.

• Supercompilation
• Refal
• Supercompilation and Verification: an idea
• Case study
  • Verification of MESI cache coherence protocol
  
  
• Further cache coherence protocols
• MESI
  • Refal encoding
  • Result of supercompilation
• MOESI
  • Refal encoding
  • Result of supercompilation
• Illinois
  • Refal encoding
  • Result of supercompilation
• Berkley
  • Refal encoding
  • Result of supercompilation
• Firefly
  • Refal encoding
  • Result of supercompilation
• Futurebus+
  • Refal encoding
  • Result of supercompilation

More parameterized protocols

• Java Meta-Locking Algorithm
  • Refal encoding
  • Result of supercompilation
• Reader-Writer protocol
  • Refal encoding
  • Result of supercompilation

Finite state systems

Future Work

Bibliography

About this document ...