Instrumenting a weakest precondition calculus for counterexample generation

DOI10.1016/j.jlamp.2018.05.003zbMath1395.68097OpenAlexW2806126867WikidataQ124831167 ScholiaQ124831167MaRDI QIDQ1648649

Sylvain Dailler, Yannick Moy, Claude Marché, David Hauzar

Publication date: 27 June 2018

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01802488/file/jlamp.pdf

zbMATH Keywords

counterexamplessatisfiability modulo theoriesdeductive program verificationweakest precondition calculus

Mathematics Subject Classification ID

Related Items (2)

Logic for reasoning about bugs in loops over data sequences (IFIL) ⋮ Knowledge forgetting in propositional \(\mu\)-calculus

Uses Software

• Nitpick
• KRAKATOA
• Why3
• Caduceus
• z3
• VCC
• VeriFast
• Boogie
• CVC4
• WhyML
• BVD
• OpenJML

Cites Work

• Unnamed Item
• Adding decision procedures to SMT solvers using axioms with triggers
• Efficient weakest preconditions
• Generating error traces from verification-condition counterexamples
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Building High Integrity Applications with SPARK
• Avoiding exponential explosion
• Computer Aided Verification
• Why3 — Where Programs Meet Provers
• Using Answer Set Programming in the Development of Verified Software.
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Instrumenting a weakest precondition calculus for counterexample generation