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

DOI10.1007/978-3-540-69738-1_5MaRDI QIDQ5452598zbMATH OpenOpenAlexFDO

Authors Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, 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

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Programming and verifying a declarative first-order prover in Isabelle/HOL
• scientific article; zbMATH DE number 1300967
• Theorem Proving in Higher Order Logics
• Simulating reachability using first-order logic with applications to verification of linked data structures
• Automated Deduction – CADE-20
• scientific article; zbMATH DE number 1926638
• scientific article; zbMATH DE number 1796120
• First-order theorem proving: foreword
• scientific article; zbMATH DE number 7699423
• scientific article; zbMATH DE number 1070624

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 2090293 (Why is no real title available?)
• scientific article; zbMATH DE number 824731 (Why is no real title available?)
• Automated Reasoning
• Combining superposition, sorts and splitting
• Data Refinement
• Deciding Boolean algebra with Presburger arithmetic
• Isabelle/HOL. A proof assistant for higher-order logic
• Lightweight relevance filtering for machine-generated resolution problems
• Shape analysis of sets
• The TPTP problem library. CNF release v1. 2. 1
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Verification, Model Checking, and Abstract Interpretation

Cited in

(11)

• Verifying Whiley programs with Boogie
• AVATAR: The Architecture for First-Order Theorem Provers
• Verification of heap manipulating programs with ordered data by extended forest automata
• Automatic decidability and combinability
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Theory decision by decomposition
• Trace-based verification of imperative programs with I/O
• Encoding monomorphic and polymorphic types
• Correct code containing containers
• Extending Sledgehammer with SMT solvers
• Translating higher-order clauses to first-order clauses

Describes a project that uses

Uses Software

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

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

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