Contract-based verification of MATLAB-style matrix programs (Q282101): Difference between revisions

@@ Property / describes a project that uses @@
+MaJIC
@@ Property / describes a project that uses: MaJIC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Simulink
@@ Property / describes a project that uses: Simulink / 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 @@
+JML
@@ Property / describes a project that uses: JML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Frama-C
@@ Property / describes a project that uses: Frama-C / rank @@
+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 @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+WhyML
@@ Property / describes a project that uses: WhyML / 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-015-0353-z
+Normal rank
@@ Property / OpenAlex ID @@
+W2340067148
@@ Property / OpenAlex ID: W2340067148 / rank @@
+Normal rank
@@ Property / cites work @@
+Contract-based verification of MATLAB-style matrix programs
+Normal rank
@@ Property / cites work @@
+A theory of type polymorphism in programming
@@ Property / cites work: A theory of type polymorphism in programming / rank @@
+Normal rank
@@ Property / cites work @@
+Static Contract Checking with Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Type inference with subtypes
@@ Property / cites work: Type inference with subtypes / rank @@
+Normal rank
@@ Property / cites work @@
+Why3 — Where Programs Meet Provers
@@ Property / cites work: Why3 — Where Programs Meet Provers / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+Invariant and Type Inference for Matrices
@@ Property / cites work: Invariant and Type Inference for Matrices / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Induction for SMT Solvers
@@ Property / cites work: Induction for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Dependent ML An approach to practical programming with dependent types
+Normal rank