Correct Code Containing Containers

DOI10.1007/978-3-642-21768-5_9zbMath1335.68052OpenAlexW34185828MaRDI QIDQ3012966

Yannick Moy, Claire Dross, Jean-Christophe Filliâtre

Publication date: 7 July 2011

Published in: Tests and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21768-5_9

zbMATH Keywords

iteratorsaxiomatizationSMTannotationscontainersAPI usage verificationautomatic proversverification by contracts

Mathematics Subject Classification ID

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

Related Items (2)

Adding decision procedures to SMT solvers using axioms with triggers ⋮ Verification of mutable linear data structures and iterator-based algorithms in Dafny

Uses Software

• Coq
• KRAKATOA
• Why3
• Caduceus
• z3
• Alt-Ergo
• SIMPLIFY
• Jahob
• STLlint

Cites Work

• Interacting with Modal Logics in the Coq Proof Assistant
• Simplify: a theorem prover for program checking
• An Abstract Machine for the Old Value Retrieval
• Efficient E-Matching for SMT Solvers
• Precise reasoning for programs using containers
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System

This page was built for publication: Correct Code Containing Containers