Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-021-09607-x
@@ Property / DOI: 10.1007/s10817-021-09607-x / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+KAD
@@ Property / describes a project that uses: KAD / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Differential_Game_Logic
@@ Property / describes a project that uses: Differential_Game_Logic / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RODAS
@@ Property / describes a project that uses: RODAS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Kleene Algebra
@@ Property / describes a project that uses: Kleene Algebra / 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/s10817-021-09607-x
+Normal rank
@@ Property / OpenAlex ID @@
+W3210385152
@@ Property / OpenAlex ID: W3210385152 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4433933
@@ Property / cites work: Q4433933 / rank @@
+Normal rank
@@ Property / cites work @@
+Building program construction and verification tools from algebraic principles
+Normal rank
@@ Property / cites work @@
+Q4003604
@@ Property / cites work: Q4003604 / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Coquelicot: a user-friendly library of real analysis for Coq
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Internal axioms for domain semirings
@@ Property / cites work: Internal axioms for domain semirings / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of Hybrid Systems
@@ Property / cites work: Verification of Hybrid Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Bellerophon: tactical theorem proving for hybrid systems
+Normal rank
@@ Property / cites work @@
+KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
+Normal rank
@@ Property / cites work @@
+Q3898534
@@ Property / cites work: Q3898534 / rank @@
+Normal rank
@@ Property / cites work @@
+Modal Kleene algebra applied to program correctness
+Normal rank
@@ Property / cites work @@
+Solving Ordinary Differential Equations II
@@ Property / cites work: Solving Ordinary Differential Equations II / rank @@
+Normal rank
@@ Property / cites work @@
+Q4525781
@@ Property / cites work: Q4525781 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4067388
@@ Property / cites work: Q4067388 / rank @@
+Normal rank
@@ Property / cites work @@
+Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
+Normal rank
@@ Property / cites work @@
+Verifying hybrid systems with modal Kleene algebra
+Normal rank
@@ Property / cites work @@
+Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+The flow of ODEs: formalization of variational equation and Poincaré map
+Normal rank
@@ Property / cites work @@
+Q5270088
@@ Property / cites work: Q5270088 / rank @@
+Normal rank
@@ Property / cites work @@
+Boolean Algebras with Operators. Part I
@@ Property / cites work: Boolean Algebras with Operators. Part I / rank @@
+Normal rank
@@ Property / cites work @@
+Q4693151
@@ Property / cites work: Q4693151 / rank @@
+Normal rank
@@ Property / cites work @@
+The Picard Algorithm for Ordinary Differential Equations in Coq
+Normal rank
@@ Property / cites work @@
+Predicate Transformer Semantics
@@ Property / cites work: Predicate Transformer Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+The Structure of Differential Invariants and Differential Cut Elimination
+Normal rank
@@ Property / cites work @@
+Logical Analysis of Hybrid Systems
@@ Property / cites work: Logical Analysis of Hybrid Systems / rank @@
+Normal rank
@@ Property / cites work @@
+A complete uniform substitution calculus for differential dynamic logic
+Normal rank
@@ Property / cites work @@
+Logical Foundations of Cyber-Physical Systems
@@ Property / cites work: Logical Foundations of Cyber-Physical Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Differential Equation Axiomatization
@@ Property / cites work: Differential Equation Axiomatization / rank @@
+Normal rank
@@ Property / cites work @@
+Algebra of Monotonic Boolean Transformers
@@ Property / cites work: Algebra of Monotonic Boolean Transformers / rank @@
+Normal rank
@@ Property / cites work @@
+Generating invariants for non-linear hybrid systems
+Normal rank
@@ Property / cites work @@
+Q4884543
@@ Property / cites work: Q4884543 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3996704
@@ Property / cites work: Q3996704 / rank @@
+Normal rank
@@ Property / cites work @@
+On the expressive power of Kleene algebra with domain
+Normal rank
@@ Property / cites work @@
+Hoare Semigroups
@@ Property / cites work: Hoare Semigroups / rank @@
+Normal rank
@@ Property / cites work @@
+Q2897328
@@ Property / cites work: Q2897328 / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S10817-021-09607-X
@@ Property / DOI: 10.1007/S10817-021-09607-X / rank @@
+Normal rank