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)

Full work available at URL https://doi.org/10.1007/11575467

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

(16)

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

Describes a project that uses

Uses Software

• BoogiePL
• Zapato
• Spec#
• CVC Lite

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)