Abstraction and subsumption in modular verification of C programs (Q2147702): Difference between revisions

@@ Property / cites work @@
+Solving reflexive domain equations in a category of complete metric spaces
+Normal rank
@@ Property / cites work @@
+Program Logics for Certified Compilers
@@ Property / cites work: Program Logics for Certified Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Relational Decomposition
@@ Property / cites work: Relational Decomposition / rank @@
+Normal rank
@@ Property / cites work @@
+VST-Floyd: a separation logic tool to verify correctness of C programs
+Normal rank
@@ Property / cites work @@
+Q4525781
@@ Property / cites work: Q4525781 / rank @@
+Normal rank
@@ Property / cites work @@
+Iris from the ground up: A modular foundation for higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Hoare logic and auxiliary variables
@@ Property / cites work: Hoare logic and auxiliary variables / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Q4411818
@@ Property / cites work: Q4411818 / rank @@
+Normal rank
@@ Property / cites work @@
+Separation logic and abstraction
@@ Property / cites work: Separation logic and abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+A proof outline logic for object-oriented programming
+Normal rank
@@ Property / cites work @@
+Dynamic Frames in Java Dynamic Logic
@@ Property / cites work: Dynamic Frames in Java Dynamic Logic / rank @@
+Normal rank