Skip to content
Success

Changes

Summary

  1. sitegen
  2. numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
Changeset 6979:0f9e0290b8b6 by immler:
sitegen
The file was modified web/entries/Automatic_Refinement.shtml (diff)
The file was modified web/entries/Collections.shtml (diff)
The file was modified web/entries/Ordinary_Differential_Equations.shtml (diff)
The file was modified web/entries/Refine_Monadic.shtml (diff)
The file was modified web/entries/Show.shtml (diff)
The file was modified web/statistics.shtml (diff)
Changeset 6978:37c47e6924e3 by immler:
numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
The file was addedthys/Affine_Arithmetic/Straight_Line_Program.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Example_Bessel.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Example_Lorenz_Classic.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Example_Utilities.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Initials.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Parallel.thy
The file was addedthys/Ordinary_Differential_Equations/IVP/Reachability_Analysis.thy
The file was addedthys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Plot.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy
The file was addedthys/Ordinary_Differential_Equations/ODE_Analysis.thy
The file was addedthys/Ordinary_Differential_Equations/ODE_Examples.thy
The file was addedthys/Ordinary_Differential_Equations/ODE_Numerics.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/GenCF_No_Comp.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/Refine_Dflt_No_Comp.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/Refine_Folds.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/Refine_String.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy
The file was modified metadata/metadata (diff)
The file was modified thys/Affine_Arithmetic/Affine_Approximation.thy (diff)
The file was modified thys/Affine_Arithmetic/Affine_Arithmetic.thy (diff)
The file was modified thys/Affine_Arithmetic/Affine_Form.thy (diff)
The file was modified thys/Affine_Arithmetic/Counterclockwise.thy (diff)
The file was modified thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy (diff)
The file was modified thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy (diff)
The file was modified thys/Affine_Arithmetic/Euclidean_Space_Explicit.thy (diff)
The file was modified thys/Affine_Arithmetic/Ex_Ineqs.thy (diff)
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy (diff)
The file was modified thys/Affine_Arithmetic/Intersection.thy (diff)
The file was modified thys/Affine_Arithmetic/Polygon.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Example1.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Example3.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Example_Exp.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Example_Oil.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Example_Variational_Equation.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Example_van_der_Pol.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Flow.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Library/Linear_ODE.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Library/MVT_Ex.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Library/Multivariate_Taylor.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/One_Step_Method.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Optimize_Float.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Optimize_Integer.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Print.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ROOT (diff)
The file was modified thys/Ordinary_Differential_Equations/document/root.tex (diff)
The file was removedthys/Ordinary_Differential_Equations/Ex/Examples.thy
The file was removedthys/Ordinary_Differential_Equations/Numerics/Euler_Affine.thy
The file was removedthys/Ordinary_Differential_Equations/Numerics/Euler_Affine_Code.thy
The file was removedthys/Ordinary_Differential_Equations/Ordinary_Differential_Equations.thy