Using First-Order Theorem Provers in the Jahob Data Structure Verification System

DOI10.1007/978-3-540-69738-1_5zbMath1132.68348OpenAlexW1744728944MaRDI QIDQ5452598

Karen Zee, Thomas Wies, Charles Bouillaguet, Viktor Kuncak, Martin C. Rinard

Publication date: 4 April 2008

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

Full work available at URL: http://hdl.handle.net/1721.1/34874

Mathematics Subject Classification ID

Related Items (10)

Verification of heap manipulating programs with ordered data by extended forest automata ⋮ Trace-based verification of imperative programs with I/O ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Correct Code Containing Containers ⋮ Translating higher-order clauses to first-order clauses ⋮ Automatic decidability and combinability ⋮ Using First-Order Theorem Provers in the Jahob Data Structure Verification System ⋮ Theory decision by decomposition ⋮ Verifying Whiley programs with Boogie ⋮ Extending Sledgehammer with SMT solvers

Uses Software

• KRAKATOA
• TPTP
• Spec#
• SPASS+T
• Zap
• Automath
• TestEra
• E Theorem Prover
• Jahob

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deciding Boolean algebra with Presburger arithmetic
• Lightweight relevance filtering for machine-generated resolution problems
• The TPTP problem library. CNF release v1. 2. 1
• Isabelle/HOL. A proof assistant for higher-order logic
• Shape Analysis of Sets.
• Data Refinement
• Automated Reasoning
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Using First-Order Theorem Provers in the Jahob Data Structure Verification System