Programming Languages and Systems
From MaRDI portal
Publication:5493379
DOI10.1007/11575467zbMATH Open1159.68374MaRDI QIDQ5493379FDOQ5493379
Authors: K. Rustan M. Leino, Francesco Logozzo 
Publication date: 20 October 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
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)
- Inferring Loop Invariants Using Postconditions
- Loop invariants in floating point algorithms
- Deaccumulation techniques for improving provability
- Predicate abstraction in a program logic calculus
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Verification by Parallelization of Parametric Code
- Proving safety with trace automata and bounded model checking
- Modular inference of subprogram contracts for safety checking
- Title not available (Why is that?)
- Verification and falsification of programs with loops using predicate abstraction
- Falsifying safety properties through games on over-approximating models
- Could We Have Chosen a Better Loop Invariant or Method Contract?
- Automatic inference of access permissions
- Predicate Abstraction in a Program Logic Calculus
- Loop Invariants from Counterexamples
Uses Software
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)
