Programming Languages and Systems

DOI10.1007/11575467MaRDI QIDQ5493379zbMATH OpenFDO

Authors K. Rustan M. Leino, Francesco Logozzo

Publication date 20 October 2006

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

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• An iterative method for generating loop invariants
• Automatically inferring loop invariants via algorithmic learning
• Automatic generation of non-linear loop invariants
• Automatic proving or disproving equality loop invariants based on finite difference techniques
• Constraint-Based Invariant Inference over Predicate Abstraction

Cited in

(15)

• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Verification and falsification of programs with loops using predicate abstraction
• Proving safety with trace automata and bounded model checking
• Automatic inference of access permissions
• Predicate abstraction in a program logic calculus
• Deaccumulation techniques for improving provability
• Falsifying safety properties through games on over-approximating models
• Inferring Loop Invariants Using Postconditions
• Predicate Abstraction in a Program Logic Calculus
• Loop Invariants from Counterexamples
• Loop invariants in floating point algorithms
• Verification by Parallelization of Parametric Code
• Modular inference of subprogram contracts for safety checking
• scientific article; zbMATH DE number 517070 (Why is no real title available?)
• Abstract Interpretation of Symbolic Execution with Explicit State Updates

Describes a project that uses

Uses Software

• Spec#
• CVC Lite
• BoogiePL
• Zapato

This page was built for publication: Programming Languages and Systems

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