How testing helps to diagnose proof failures

DOI10.1007/S00165-018-0456-4MaRDI QIDQ1624590zbMATH OpenOpenAlexWikidataFDO

Authors Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand

Publication date 16 November 2018

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-018-0456-4

zbMATH Keywords

specificationtest generationdeductive verificationFrama-Cproof debugging

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Instrumenting a weakest precondition calculus for counterexample generation
• Predicting failures of and repairing inductive proof attempts
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Formal Approaches to Software Testing
• Automated flaw detection in algebraic specifications

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• Collaborative verification and testing with explicit assumptions
• Compositional may-must program analysis: unleashing the power of alternation
• Computer Aided Verification
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Counterexample-guided abstraction refinement for symbolic model checking
• Counterexample-guided focus
• Counterexample-guided synthesis of observation predicates
• Efficient generation of restricted growth words
• Finding Counter Examples in Induction Proofs
• Generating Unit Tests from Formal Proofs
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Describes a project that uses

Uses Software

• GitHub
• StaDy
• PathCrawler
• Frama-C
• ACSL
• PVS
• Isabelle/HOL
• Coq

This page was built for publication: How testing helps to diagnose proof failures

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