A dynamic logic for deductive verification of multi-threaded programs (Q470007): Difference between revisions

@@ Property / describes a project that uses @@
+JML
@@ Property / describes a project that uses: JML / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s00165-012-0261-4
+Normal rank
@@ Property / OpenAlex ID @@
+W2081764864
@@ Property / OpenAlex ID: W2081764864 / rank @@
+Normal rank
@@ Property / cites work @@
+An assertion-based proof system for multithreaded Java
+Normal rank
@@ Property / cites work @@
+Proving assertions about parallel programs
@@ Property / cites work: Proving assertions about parallel programs / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Concurrent Systems with Symbolic Execution
+Normal rank
@@ Property / cites work @@
+KeY: A Formal Method for Object-Oriented Systems
@@ Property / cites work: KeY: A Formal Method for Object-Oriented Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Dynamic Logic with Non-rigid Functions
@@ Property / cites work: Dynamic Logic with Non-rigid Functions / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement and retrenchment for programming language data types
+Normal rank
@@ Property / cites work @@
+A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
+Normal rank
@@ Property / cites work @@
+Q4472236
@@ Property / cites work: Q4472236 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal verification of parallel programs
@@ Property / cites work: Formal verification of parallel programs / rank @@
+Normal rank
@@ Property / cites work @@
+Atomizer
@@ Property / cites work: Atomizer / rank @@
+Normal rank
@@ Property / cites work @@
+Model checking JAVA programs using JAVA PathFinder
+Normal rank
@@ Property / cites work @@
+The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
+Normal rank
@@ Property / cites work @@
+Q2764132
@@ Property / cites work: Q2764132 / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic execution and program testing
@@ Property / cites work: Symbolic execution and program testing / rank @@
+Normal rank
@@ Property / cites work @@
+Q4417955
@@ Property / cites work: Q4417955 / rank @@
+Normal rank
@@ Property / cites work @@
+Completing the temporal picture
@@ Property / cites work: Completing the temporal picture / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic proof technique for parallel programs
+Normal rank
@@ Property / cites work @@
+Communication in concurrent dynamic logic
@@ Property / cites work: Communication in concurrent dynamic logic / rank @@
+Normal rank
@@ Property / cites work @@
+Concurrent dynamic logic
@@ Property / cites work: Concurrent dynamic logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q2845504
@@ Property / cites work: Q2845504 / rank @@
+Normal rank
@@ Property / cites work @@
+Hoare logic for Java in Isabelle/HOL
@@ Property / cites work: Hoare logic for Java in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+A Marriage of Rely/Guarantee and Separation Logic
@@ Property / cites work: A Marriage of Rely/Guarantee and Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying safety properties of concurrent Java programs using 3-valued logic
+Normal rank