Using First-Order Theorem Provers in the Jahob Data Structure Verification System
DOI10.1007/978-3-540-69738-1_5zbMATH Open1132.68348OpenAlexW1744728944MaRDI QIDQ5452598FDOQ5452598
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
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
Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- The TPTP problem library. CNF release v1. 2. 1
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Data Refinement
- Lightweight relevance filtering for machine-generated resolution problems
- Combining superposition, sorts and splitting
- Title not available (Why is that?)
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Deciding Boolean algebra with Presburger arithmetic
- Automated Reasoning
- Shape analysis of sets
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
Uses Software
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)
