Testing First-Order Logic Axioms in Program Verification

No abstract is available for this paper.

• Publication year

  2010

• Venue

  TAP@TOOLS

• Publication date

  2010-07-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-13977-2_4
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Functional Testing in the Focal Environment

  2008cited by this paper
• Finding Counter Examples in Induction Proofs

  2008cited by this paper
• A Software Safety Certification Tool for Automatically Generated Guidance, Navigation and Control Code

  2008cited by this paper
• Formalising Java's Data Race Free Guarantee

  2007cited by this paper
• The YICES SMT Solver

  2006cited by this paper
• Practical Proof Checking for Program Certification

  2005cited by this paper
• Random testing in Isabelle/HOL

  2004cited by this paper
• Combining Testing and Proving in Dependent Type Theory

  2003cited by this paper
• Template meta-programming for Haskell

  2002cited by this paper
• System Description: SystemOn TPTP

  2000influential reference
• QuickCheck: a lightweight tool for random testing of Haskell programs

  2000influential reference
• Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings

  2000cited by this paper
• Quaternions and Rotation Sequences

  1998cited by this paper
• Planware-domain-specific synthesis of high-performance schedulers

  1998cited by this paper
• Fundamentals of Astrodynamics and Applications

  1997cited by this paper
• Isabelle: A Generic Theorem Prover

  1994cited by this paper
• Prolegomena to a Theory of Mechanized Formal Reasoning

  1980cited by this paper
• The Application of Theorem Proving to Question-Answering Systems

  1969cited by this paper
• The use of theorem-proving techniques in question-answering systems

  1968cited by this paper

• Formal Verification of a Fail-Safe Cross-Chain Bridge

  2025cites this paper
• Reusable Formal Verification of DAG-based Consensus Protocols

  2024cites this paper
• Identifying Overly Restrictive Matching Paterns in SMT-based Program Verifiers (extended version)

  2022cites this paper
• An Axiomatic Approach to the Data Models Formalization for Mass Data Processing

  2020cites this paper
• An Overview of Resilient and Automatic Model-Based Testing Approaches for Automotive Industry

  2019cites this paper
• How testing helps to diagnose proof failures

  2018cites this paper
• Automating the Assembly of Aviation Safety Cases

  2014cites this paper
• Auditing User-Provided Axioms in Software Verification Conditions

  2013cites this paper
• Evidence arguments for using formal methods in software certification

  2013cites this paper
• Heterogeneous Aviation Safety Cases: Integrating the Formal and the Non-formal

  2012cites this paper