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

@@ Property / Mathematics Subject Classification ID @@
+N30
@@ Property / Mathematics Subject Classification ID: 68N30 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+Q60
@@ Property / Mathematics Subject Classification ID: 68Q60 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B70
@@ Property / Mathematics Subject Classification ID: 03B70 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6059154
@@ Property / zbMATH DE Number: 6059154 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+automated verification
@@ Property / zbMATH Keywords: automated verification / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+separation logic
@@ Property / zbMATH Keywords: separation logic / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+entailment checking
@@ Property / zbMATH Keywords: entailment checking / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+inductive shape predicates with size and bag properties
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Spec#
@@ Property / describes a project that uses: Spec# / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ESC/Java
@@ Property / describes a project that uses: ESC/Java / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MONA
@@ Property / describes a project that uses: MONA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HIP
@@ Property / describes a project that uses: HIP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Smallfoot
@@ Property / describes a project that uses: Smallfoot / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Z
@@ Property / describes a project that uses: Z / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Eiffel
@@ Property / describes a project that uses: Eiffel / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+JML
@@ Property / describes a project that uses: JML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SIMPLIFY
@@ Property / describes a project that uses: SIMPLIFY / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC
@@ Property / describes a project that uses: CVC / 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.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
@@ links / mardi / name / links / mardi / name @@
+Publication:436400