Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.scico.2010.07.004
+Normal rank
@@ Property / OpenAlex ID @@
+W2045388381
@@ Property / OpenAlex ID: W2045388381 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+A Transformation System for Developing Recursive Programs
+Normal rank
@@ Property / cites work @@
+Compositional shape analysis by means of bi-abduction
+Normal rank
@@ Property / cites work @@
+Combining programming with theorem proving
@@ Property / cites work: Combining programming with theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Verification of Shape and Size Properties Via Separation Logic
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Interprocedural Shape Analysis with Separated Heap Abstractions
+Normal rank
@@ Property / cites work @@
+A Theory of Pointers for the UTP
@@ Property / cites work: A Theory of Pointers for the UTP / 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 @@
+Q4934618
@@ Property / cites work: Q4934618 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4417801
@@ Property / cites work: Q4417801 / rank @@
+Normal rank
@@ Property / cites work @@
+BI as an assertion language for mutable data structures
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q5762903
@@ Property / cites work: Q5762903 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying properties of well-founded linked lists
@@ Property / cites work: Verifying properties of well-founded linked lists / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4024014
@@ Property / cites work: Q4024014 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+Presburger arithmetic with bounded quantifier alternation
+Normal rank
@@ Property / cites work @@
+Static Analysis
@@ Property / cites work: Static Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Extending separation logic with fixpoints and postponed substitution
+Normal rank
@@ Property / cites work @@
+Q3995087
@@ Property / cites work: Q3995087 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804919
@@ Property / cites work: Q4804919 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4532095
@@ Property / cites work: Q4532095 / rank @@
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Scalable Shape Analysis for Systems Code
@@ Property / cites work: Scalable Shape Analysis for Systems Code / rank @@
+Normal rank