Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (Q2988675): Difference between revisions

@@ Property / describes a project that uses @@
+SIMPLIFY
@@ Property / describes a project that uses: SIMPLIFY / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Boogie
@@ Property / describes a project that uses: Boogie / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Dafny
@@ Property / describes a project that uses: Dafny / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LLVM
@@ Property / describes a project that uses: LLVM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SymDiff
@@ Property / describes a project that uses: SymDiff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoVaC
@@ Property / describes a project that uses: CoVaC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RVT
@@ Property / describes a project that uses: RVT / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2591626899
@@ Property / OpenAlex ID: W2591626899 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4636558
@@ Property / cites work: Q4636558 / rank @@
+Normal rank
@@ Property / cites work @@
+Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
+Normal rank
@@ Property / cites work @@
+Product programs and relational program logics
@@ Property / cites work: Product programs and relational program logics / rank @@
+Normal rank
@@ Property / cites work @@
+Secure information flow by self-composition
@@ Property / cites work: Secure information flow by self-composition / rank @@
+Normal rank
@@ Property / cites work @@
+Abstracting Allocation
@@ Property / cites work: Abstracting Allocation / rank @@
+Normal rank
@@ Property / cites work @@
+Simple relational correctness proofs for static analyses and program transformations
+Normal rank
@@ Property / cites work @@
+Relational Decomposition
@@ Property / cites work: Relational Decomposition / rank @@
+Normal rank
@@ Property / cites work @@
+Q5684216
@@ Property / cites work: Q5684216 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Proving mutual termination
@@ Property / cites work: Proving mutual termination / rank @@
+Normal rank
@@ Property / cites work @@
+Inference rules for proving the equivalence of recursive procedures
+Normal rank
@@ Property / cites work @@
+Towards Modularly Comparing Programs Using Automated Theorem Provers
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+A semantic approach to secure information flow
@@ Property / cites work: A semantic approach to secure information flow / rank @@
+Normal rank
@@ Property / cites work @@
+Small bisimulations for reasoning about higher-order imperative programs
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Verification of Equivalent-Results Methods
@@ Property / cites work: Verification of Equivalent-Results Methods / rank @@
+Normal rank
@@ Property / cites work @@
+Fully abstract models of typed \(\lambda\)-calculi
+Normal rank
@@ Property / cites work @@
+Abstract Semantic Differencing for Numerical Programs
+Normal rank
@@ Property / cites work @@
+Q4813228
@@ Property / cites work: Q4813228 / rank @@
+Normal rank
@@ Property / cites work @@
+Regression verification for unbalanced recursive functions
+Normal rank
@@ Property / cites work @@
+Abstract models of storage
@@ Property / cites work: Abstract models of storage / rank @@
+Normal rank
@@ Property / cites work @@
+Static Analysis
@@ Property / cites work: Static Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Program equivalence in a simple language with state
+Normal rank
@@ Property / cites work @@
+Relational separation logic
@@ Property / cites work: Relational separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q3256561
@@ Property / cites work: Q3256561 / rank @@
+Normal rank