Precondition Inference from Intermittent Assertions and Application to Contracts on Collections

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

Patrick Cousot, Radhia Cousot, Francesco Logozzo

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

68Q55: Semantics in the theory of computing

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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