Automating Induction with an SMT Solver

DOI10.1007/978-3-642-27940-9_21zbMath1326.68262OpenAlexW1831545713MaRDI QIDQ2891425

K. Rustan M. Leino

Publication date: 15 June 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-27940-9_21

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items

An Assertional Proof of the Stability and Correctness of Natural Mergesort, TIP: Tons of Inductive Problems, Induction in saturation-based proof search, Dafny, Removing algebraic data types from constrained Horn clauses using difference predicates, Verifying Whiley programs with Boogie

Uses Software

• ACL2
• Coq
• KRAKATOA
• PVS
• Why3
• Caduceus
• z3
• SIMPLIFY
• Sledgehammer
• VCC
• VeriFast
• Boogie
• ACL2s
• Zeno
• VeriFun

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• The ACL2 Sedan Theorem Proving System
• Dafny: An Automatic Program Verifier for Functional Correctness
• Solving SAT and SAT Modulo Theories
• Simplify: a theorem prover for program checking
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding
• Refinement Calculus
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Case-Analysis for Rippling and Inductive Proof
• Sledgehammer: Judgement Day