Inductive benchmarks for automated reasoning

DOI10.1007/978-3-030-81097-9_9zbMATH Open1485.68281OpenAlexW3160880798MaRDI QIDQ2128807FDOQ2128807

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

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

Mathematics Subject Classification ID

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

Cites Work

• Dafny: an automatic program verifier for functional correctness
• Zeno: an automated prover for properties of recursive data structures
• Induction for SMT solvers
• Title not available (Why is that?)
• Integer induction in saturation
• Superposition with structural induction
• TIP: tons of inductive problems
• Induction in saturation-based proof search
• The Imandra Automated Reasoning System (System Description)
• 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

Uses Software

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

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)