Correct code containing containers

DOI10.1007/978-3-642-21768-5_9MaRDI QIDQ3012966zbMATH OpenOpenAlexFDO

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

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

annotationsAPI usage verificationautomatic proversaxiomatizationcontainersiteratorsSMTverification by contracts

Mathematics Subject Classification ID

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

Recommendations

• Precise reasoning for programs using containers
• scientific article; zbMATH DE number 5652074
• Verified squared, does critical software deserve verified tools?
• Building high integrity applications with SPARK
• Light-weight containers for Isabelle: efficient, extensible, nestable

Cites work

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

Cited in

(3)

• Adding decision procedures to SMT solvers using axioms with triggers
• Precise reasoning for programs using containers
• Verification of mutable linear data structures and iterator-based algorithms in Dafny

Describes a project that uses

Uses Software

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

This page was built for publication: Correct code containing containers

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