Relational Decomposition (Q3087994): Difference between revisions

@@ Property / describes a project that uses @@
+SPARK
@@ Property / describes a project that uses: SPARK / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Toolchain
@@ Property / describes a project that uses: Toolchain / 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/978-3-642-22863-6_6
+Normal rank
@@ Property / OpenAlex ID @@
+W2914544883
@@ Property / OpenAlex ID: W2914544883 / rank @@
+Normal rank
@@ Property / cites work @@
+A logic for information flow in object-oriented programs
+Normal rank
@@ Property / cites work @@
+Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays
+Normal rank
@@ Property / cites work @@
+Verified Software Toolchain
@@ Property / cites work: Verified Software Toolchain / rank @@
+Normal rank
@@ Property / cites work @@
+A program logic for resources
@@ Property / cites work: A program logic for resources / rank @@
+Normal rank
@@ Property / cites work @@
+Stack-based access control and secure information flow
+Normal rank
@@ Property / cites work @@
+Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
+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 @@
+Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+Power simulation and its relation to traces and failures refinement
+Normal rank
@@ Property / cites work @@
+The weakest prespecification
@@ Property / cites work: The weakest prespecification / rank @@
+Normal rank
@@ Property / cites work @@
+Prespecification in data refinement
@@ Property / cites work: Prespecification in data refinement / rank @@
+Normal rank
@@ Property / cites work @@
+On flow-sensitive security types
@@ Property / cites work: On flow-sensitive security types / rank @@
+Normal rank
@@ Property / cites work @@
+Q3997074
@@ Property / cites work: Q3997074 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated soundness proofs for dataflow analyses and transformations via local rules
+Normal rank
@@ Property / cites work @@
+A formally verified compiler back-end
@@ Property / cites work: A formally verified compiler back-end / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic numeric abstractions for heap-manipulating programs
+Normal rank
@@ Property / cites work @@
+Q4411818
@@ Property / cites work: Q4411818 / rank @@
+Normal rank
@@ Property / cites work @@
+Program and proof optimizations with type systems
@@ Property / cites work: Program and proof optimizations with type systems / rank @@
+Normal rank
@@ Property / cites work @@
+Generating compiler optimizations from proofs
@@ Property / cites work: Generating compiler optimizations from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Static Analysis
@@ Property / cites work: Static Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Inter-program Properties
@@ Property / cites work: Inter-program Properties / rank @@
+Normal rank
@@ Property / cites work @@
+Relational separation logic
@@ Property / cites work: Relational separation logic / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:3087994