Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723): Difference between revisions

@@ Property / cites work @@
+Stateless model checking for TSO and PSO
@@ Property / cites work: Stateless model checking for TSO and PSO / rank @@
+Normal rank
@@ Property / cites work @@
+Ogre and Pythia: an invariance proof method for weak consistency models
+Normal rank
@@ Property / cites work @@
+Software Verification for Weak Memory via Program Transformation
+Normal rank
@@ Property / cites work @@
+Verification of sequential and concurrent programs
+Normal rank
@@ Property / cites work @@
+Mathematizing C++ concurrency
@@ Property / cites work: Mathematizing C++ concurrency / rank @@
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Effective abstractions for verification under relaxed memory models
+Normal rank
@@ Property / cites work @@
+Q2768503
@@ Property / cites work: Q2768503 / rank @@
+Normal rank
@@ Property / cites work @@
+A Program Logic for C11 Memory Fences
@@ Property / cites work: A Program Logic for C11 Memory Fences / rank @@
+Normal rank
@@ Property / cites work @@
+Tackling Real-Life Relaxed Concurrency with FSL++
@@ Property / cites work: Tackling Real-Life Relaxed Concurrency with FSL++ / rank @@
+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 promising semantics for relaxed-memory concurrency
+Normal rank
@@ Property / cites work @@
+Owicki-Gries Reasoning for Weak Memory Models
@@ Property / cites work: Owicki-Gries Reasoning for Weak Memory Models / rank @@
+Normal rank
@@ Property / cites work @@
+How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
+Normal rank
@@ Property / cites work @@
+Viper: A Verification Infrastructure for Permission-Based Reasoning
+Normal rank
@@ Property / cites work @@
+An axiomatic proof technique for parallel programs
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Modular Relaxed Dependencies in Weak Memory Concurrency
+Normal rank
@@ Property / cites work @@
+Automating deductive verification for weak-memory programs
+Normal rank
@@ Property / cites work @@
+A separation logic for a promising semantics
@@ Property / cites work: A separation logic for a promising semantics / rank @@
+Normal rank