A language-independent proof system for full program equivalence (Q510898): Difference between revisions

@@ Property / describes a project that uses @@
+K-Java
@@ Property / describes a project that uses: K-Java / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2315369658
@@ Property / OpenAlex ID: W2315369658 / rank @@
+Normal rank
@@ Property / cites work @@
+State-dependent representation independence
@@ Property / cites work: State-dependent representation independence / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Simple relational correctness proofs for static analyses and program transformations
+Normal rank
@@ Property / cites work @@
+Biorthogonality, step-indexing and compiler correctness
+Normal rank
@@ Property / cites work @@
+K-Java
@@ Property / cites work: K-Java / rank @@
+Normal rank
@@ Property / cites work @@
+A Theoretical Foundation for Programming Languages Aggregation
+Normal rank
@@ Property / cites work @@
+All-Path Reachability Logic
@@ Property / cites work: All-Path Reachability Logic / rank @@
+Normal rank
@@ Property / cites work @@
+An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework
+Normal rank
@@ Property / cites work @@
+Regression Verification for Multi-threaded Programs
+Normal rank
@@ Property / cites work @@
+Q4812966
@@ Property / cites work: Q4812966 / rank @@
+Normal rank
@@ Property / cites work @@
+Inference rules for proving the equivalence of recursive procedures
+Normal rank
@@ Property / cites work @@
+Inference Rules for Proving the Equivalence of Recursive Procedures
+Normal rank
@@ Property / cites work @@
+Don't Try to Solve These Problems
@@ Property / cites work: Don't Try to Solve These Problems / rank @@
+Normal rank
@@ Property / cites work @@
+A kripke logical relation between ML and assembly
@@ Property / cites work: A kripke logical relation between ML and assembly / rank @@
+Normal rank
@@ Property / cites work @@
+The marriage of bisimulations and Kripke logical relations
+Normal rank
@@ Property / cites work @@
+Q4375636
@@ Property / cites work: Q4375636 / 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 @@
+Towards Modularly Comparing Programs Using Automated Theorem Provers
+Normal rank
@@ Property / cites work @@
+Program equivalence by circular reasoning
@@ Property / cites work: Program equivalence by circular reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+A generic framework for symbolic execution: a coinductive approach
+Normal rank
@@ Property / cites work @@
+Q3992568
@@ Property / cites work: Q3992568 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Q4813228
@@ Property / cites work: Q4813228 / rank @@
+Normal rank
@@ Property / cites work @@
+From Hoare Logic to Matching Logic Reachability
@@ Property / cites work: From Hoare Logic to Matching Logic Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a Unified Theory of Operational and Axiomatic Semantics
+Normal rank
@@ Property / cites work @@
+One-Path Reachability Logic
@@ Property / cites work: One-Path Reachability Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Matching Logic: An Alternative to Hoare/Floyd Logic
+Normal rank
@@ Property / cites work @@
+Equality of streams is a Π0 over 2-complete problem
+Normal rank
@@ Property / cites work @@
+Matching Logic - Extended Abstract (Invited Talk)
@@ Property / cites work: Matching Logic - Extended Abstract (Invited Talk) / rank @@
+Normal rank
@@ Property / cites work @@
+Introduction to Bisimulation and Coinduction
@@ Property / cites work: Introduction to Bisimulation and Coinduction / rank @@
+Normal rank
@@ Property / cites work @@
+Logical Bisimulations and Functional Languages
@@ Property / cites work: Logical Bisimulations and Functional Languages / rank @@
+Normal rank
@@ Property / cites work @@
+A rewriting logic approach to operational semantics
+Normal rank