Inductive benchmarks for automated reasoning

DOI10.1007/978-3-030-81097-9_9MaRDI QIDQ2128807zbMATH OpenOpenAlexFDO

Authors Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov

Publication date 22 April 2022

Full work available at URL http://hdl.handle.net/20.500.12708/18558

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• TIP: tons of inductive problems
• Induction for SMT solvers
• Automating Induction with an SMT Solver
• Heaps and Data Structures: A Challenge for Automated Provers
• scientific article; zbMATH DE number 2177631

Cites work

• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• Dafny: an automatic program verifier for functional correctness
• Induction for SMT solvers
• Induction in saturation-based proof search
• Integer induction in saturation
• Superposition with structural induction
• TIP: tons of inductive problems
• The Imandra Automated Reasoning System (System Description)
• Zeno: an automated prover for properties of recursive data structures
• eThor

Cited in

(5)

• TIP: tons of inductive problems
• TIP: tools for inductive provers
• Getting saturated with induction
• Induction for SMT solvers
• Using hints to increase the effectiveness of an automated reasoning program: Case studies

Describes a project that uses

Uses Software

• eThor
• Imandra
• Easychair
• CBMC
• CVC4
• Zeno
• NQTHM
• SMT-LIB
• VAMPIRE
• Dafny

This page was built for publication: Inductive benchmarks for automated reasoning

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