Variance analyses from invariance analyses

DOI10.1145/1190216.1190249zbMath1295.68076OpenAlexW4241086578MaRDI QIDQ3189800

Aziem Chawdhary, Byron Cook, Dino Distefano, Josh Berdine, Peter W. O'Hearn

Publication date: 12 September 2014

Published in: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1190216.1190249

zbMATH Keywords

livenessformal verificationprogram analysisterminationsoftware model checking

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (11)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Algebraic program analysis ⋮ Temporal property verification as a program analysis task ⋮ Proving termination of nonlinear command sequences ⋮ Loop Summarization and Termination Analysis ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation ⋮ Loop summarization using state and transition invariants ⋮ Programs with lists are counter automata ⋮ A Hybrid Denotational Semantics for Hybrid Systems ⋮ Automata-Based Termination Proofs ⋮ Local Reasoning about Data Update

This page was built for publication: Variance analyses from invariance analyses