Simple relational correctness proofs for static analyses and program transformations

DOI10.1145/964001.964003zbMath1325.68057OpenAlexW2149996206MaRDI QIDQ3452246

Nick Benton

Publication date: 11 November 2015

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

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

zbMATH Keywords

typessecuritypartial equivalence relationsprogram analysisdenotational semanticsHoare logicinformation flowdependencyoptimizing compilation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (38)

Relational Differential Dynamic Logic ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Constraint-based relational verification ⋮ Product programs and relational program logics ⋮ Proof optimization for partial redundancy elimination ⋮ Counting Successes: Effects and Transformations for Non-deterministic Programs ⋮ Certified verification of relational properties ⋮ Laws of Programming for References ⋮ Relational separation logic ⋮ Observational purity and encapsulation ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Dead code elimination based pointer analysis for multithreaded programs ⋮ Divergences on monads for relational program logics ⋮ Recognition of logically related regions based heap abstraction ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Is Your Software on Dope? ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Probabilistic Lipschitz analysis of neural networks ⋮ A self-certifying compilation framework for WebAssembly ⋮ Approximate relational Hoare logic for continuous random samplings ⋮ Predicate Pairing for program verification ⋮ A language-independent proof system for full program equivalence ⋮ Verifying relative safety, accuracy, and termination for program approximations ⋮ Program and proof optimizations with type systems ⋮ Relational bytecode correlations ⋮ Imperative-program transformation by instrumented-interpreter specialization ⋮ Fifty years of Hoare's logic ⋮ An Algebraic Account of References in Game Semantics ⋮ Certificate Translation in Abstract Interpretation ⋮ Relational Decomposition ⋮ Inter-program Properties ⋮ A Machine-Checked Framework for Relational Separation Logic ⋮ Secure information flow by self-composition ⋮ Unnamed Item ⋮ Relational cost analysis in a functional-imperative setting

This page was built for publication: Simple relational correctness proofs for static analyses and program transformations