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

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

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

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

68Q60: Specification and verification (program logics, model checking, etc.)

68P05: Data structures

Related Items

Using First-Order Theorem Provers in the Jahob Data Structure Verification System, Automatic decidability and combinability, Trace-based verification of imperative programs with I/O, Theory decision by decomposition, Extending Sledgehammer with SMT solvers, Translating higher-order clauses to first-order clauses, Correct Code Containing Containers

Uses Software

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

Cites Work

• Unnamed Item
• 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
• Data Refinement
• Automated Reasoning
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Verification, Model Checking, and Abstract Interpretation