Loop summarization using state and transition invariants

DOI10.1007/s10703-012-0176-yzbMath1291.68262OpenAlexW2129766426MaRDI QIDQ2248058

Aliaksei Tsitovich, Stefano Tonetta, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: http://doc.rero.ch/record/310194/files/10703_2012_Article_176.pdf

zbMATH Keywords

terminationloop invariantsprogram abstractionloop summarizationtransition invariants

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

LCTD: test-guided proofs for C programs on LLVM ⋮ Precise quantitative information flow analysis -- a symbolic approach

Uses Software

• Dafny
• SLAM
• ARMC
• ESC/Java
• SPEED
• CBMC
• TVLA
• SatAbs
• CSSV
• Houdini

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Refining abstract interpretations
• Summarization for termination: No return!
• Predicate abstraction of ANSI-C programs using SAT
• Numeric Bounds Analysis with Conflict-Driven Learning
• Dafny: An Automatic Program Verifier for Functional Correctness
• Variance analyses from invariance analyses
• Proving Conditional Termination
• Ranking Function Synthesis for Bit-Vector Relations
• Abstract Counterexample-Based Refinement for Powerset Domains
• Ranking Functions for Size-Change Termination II
• Fast Algorithms for Solving Path Problems
• Size-Change Termination and Transition Invariants
• The size-change principle for program termination
• Lazy abstraction
• SPEED
• A combination framework for tracking partition sizes
• Tools and Algorithms for the Construction and Analysis of Systems
• Ranking Abstractions
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Loop summarization using state and transition invariants