Instrumenting a weakest precondition calculus for counterexample generation
type: Item
instance of: scholarly article
title: Instrumenting a weakest precondition calculus for counterexample generation
zbMATH Open document ID: 1395.68097
author: Sylvain Dailler
author: David Hauzar
author: Claude Marché
author: Yannick Moy
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2018-06-27T00:00:00Z
full work available at URL: jlamp.pdf
Mathematics Subject Classification ID: 68N99
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6895327
zbMATH Keywords: deductive program verification
zbMATH Keywords: weakest precondition calculus
zbMATH Keywords: satisfiability modulo theories
zbMATH Keywords: counterexamples
describes a project that uses: KRAKATOA
describes a project that uses: BVD
describes a project that uses: OpenJML
describes a project that uses: Boogie
describes a project that uses: Why3
describes a project that uses: VeriFast
describes a project that uses: VCC
describes a project that uses: Caduceus
describes a project that uses: Nitpick
describes a project that uses: z3
describes a project that uses: CVC4
describes a project that uses: WhyML
MaRDI profile type: Publication
OpenAlex ID: W2806126867
Wikidata QID: Q124831167
cites work: Q4144755
cites work: Why3 — Where Programs Meet Provers
cites work: Avoiding exponential explosion
cites work: Efficient weakest preconditions
cites work: Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
cites work: Adding decision procedures to SMT solvers using axioms with triggers
cites work: Building High Integrity Applications with SPARK
cites work: Using Answer Set Programming in the Development of Verified Software.
cites work: Computer Aided Verification
cites work: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
cites work: Generating error traces from verification-condition counterexamples
DOI: 10.1016/J.JLAMP.2018.05.003
Recommended article: Counterexample-Guided Precondition Inference
Recommended article: The weakest precondition calculus: Recursion and duality
Recommended article: Fundamental Approaches to Software Engineering
Recommended article: Q4484349
Recommended article: Counterexample-guided quantifier instantiation for synthesis in SMT
Recommended article: Weakest Preconditions for High-Level Programs
Recommended article: Weakest preconditions for pure Prolog programs
description: scientific article; zbMATH DE number 6895327