One logic to use them all

DOI10.1007/978-3-642-38574-2_1MaRDI QIDQ4928425zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Why3 -- where programs meet provers
• Tactical theorem proving in program verification
• Deductive software verification: from pen-and-paper proofs to industrial tools
• Information-intensive proof technology
• Verification of logic programs

Cited in

(14)

• Hammer for Coq: automation for dependent type theory
• The matrix reproved (verification pearl)
• Indexed and fibred structures for Hoare logic
• To be fair, use bundles
• WhyMP, a formally verified arbitrary-precision integer library
• On the diversity of asynchronous communication
• Handling Polymorphism in Automated Deduction
• A Why3 proof of GMP algorithms
• Why3 -- where programs meet provers
• One pendulum to run them all
• Information-intensive proof technology
• A generic intermediate representation for verification condition generation
• Why3-do: the way of harmonious distributed system proofs
• An open challenge problem repository for systems supporting binders

Describes a project that uses

Uses Software

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

This page was built for publication: One logic to use them all

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928425)