Precondition Inference from Intermittent Assertions and Application to Contracts on Collections

DOI10.1007/978-3-642-18275-4_12zbMath1317.68030OpenAlexW3196044867MaRDI QIDQ3075478

Radhia Cousot, Francesco Logozzo, Patrick Cousot

Publication date: 15 February 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00543881/file/main.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ Limits and difficulties in the design of under-approximation abstract domains ⋮ Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations ⋮ Static Contract Checking with Abstract Interpretation

Uses Software

• Eiffel
• ESC/Java
• ASTREE
• Snugglebug
• FunArray

Cites Work

• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Static Contract Checking with Abstract Interpretation
• Abstract interpretation and application to logic programs
• Guarded commands, nondeterminacy and formal derivation of programs
• Symbolic execution and program testing
• Systematic design of program transformation frameworks by abstract interpretation
• Compositional shape analysis by means of bi-abduction
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Sufficient Preconditions for Modular Assertion Checking
• Computing Procedure Summaries for Interprocedural Analysis
• Static Analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Precondition Inference from Intermittent Assertions and Application to Contracts on Collections