How testing helps to diagnose proof failures

DOI10.1007/s00165-018-0456-4zbMath1425.68079OpenAlexW2808614825WikidataQ129692997 ScholiaQ129692997MaRDI QIDQ1624590

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

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

test generationspecificationdeductive verificationFrama-Cproof debugging

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Efficient generation of restricted growth words
• Counterexample-guided abstraction refinement for symbolic model checking
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Collaborative Verification and Testing with Explicit Assumptions
• Counterexample-Guided Synthesis of Observation Predicates
• Compositional may-must program analysis
• Counterexample-guided focus
• Computer Aided Verification
• Generating Unit Tests from Formal Proofs
• Finding Counter Examples in Induction Proofs

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