SMT-based planning synthesis for distributed system reconfigurations

• Software and benchmarks

Superposition with datatypes and codatatypes

• Tool (Vampire pre-release — Github)
• Benchmarks and results

An inference rule for the acyclicity property of term algebras

• Benchmarks

Coming to terms with quantified reasoning

• Tool (Vampire 4.1 — Linux 64-bit binary)
• Benchmarks and results (most of these problems were originally published by Andrew Reynolds and Jasmin Blanchette)

Reasoning about loops using Vampire in KeY

• Tool (TPTP problem generator — Github)
• Tool (Vampire 4.0 — Linux 64-bit binary)
• Tool (Vampire 4.0 — OS X binary)
• Benchmarks

Catamorphism generation and fusion using Coq

• Tool (Coq module — Github)