One Logic to Use Them All

DOI10.1007/978-3-642-38574-2_1zbMath1381.68266OpenAlexW2123470495MaRDI QIDQ4928425

Jean-Christophe Filliâtre

Publication date: 14 June 2013

Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_1

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (8)

On the diversity of asynchronous communication ⋮ Hammer for Coq: automation for dependent type theory ⋮ WhyMP, a formally verified arbitrary-precision integer library ⋮ Why3-do: the way of harmonious distributed system proofs ⋮ The matrix reproved (verification pearl) ⋮ Indexed and fibred structures for Hoare logic ⋮ A Generic Intermediate Representation for Verification Condition Generation ⋮ Unnamed Item

Uses Software

• Coq
• Dafny
• VAMPIRE
• KRAKATOA
• PVS
• SPASS
• TPTP
• Yices
• Why3
• Frama-C
• z3
• SIMPLIFY
• Sledgehammer
• VeriFast
• CVC4
• iProver
• KIV
• E Theorem Prover
• seL4

This page was built for publication: One Logic to Use Them All