[FOM] an interesting article in Notices of American Mathematical Society

[André Platzer]

Hello,

Rigorously proved results about dynamics is quite an important area, indeed. Especially with the increased significance of embedded systems and cyber-physical systems, which are usually modeled as hybrid systems that combined discrete dynamical systems with continuous dynamical systems.

Enabling rigorous proofs about the behavior of various forms of dynamical systems is exactly what the family of dynamic logics for dynamical systems is meant for. Here's a survey of some of the principles in that line of work:

- Logics of dynamical systems. LICS 2012.
http://dx.doi.org/10.1109/LICS.2012.13

More numerical techniques also exist for verification purposes by constraint propagation, e.g.

- Safety verification of hybrid systems by constraint propagation-based abstraction refinement. Trans. on Embedded Computing Sys. 2007
http://dx.doi.org/10.1145/1210268.1210276

There are surprising links between the symbolic and the numerical point of view:

- The complete proof theory of hybrid systems. LICS 2012.
http://dx.doi.org/10.1109/LICS.2012.64

Andre

> On Oct 1, 2015, at 09:29, Frédéric Blanqui <frederic.blanqui at inria.fr> wrote:
> 
> Hello.
> 
> The following two papers may also be of interest:
> 
> -  Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program,
> by Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
> http://dx.doi.org/10.1007/s10817-012-9255-4
> 
> - Trusting computations: A mechanized proof from partial differential equations to actual program,
> by Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
> http://dx.doi.org/10.1016/j.camwa.2014.06.004
> 
> Frédéric.
> 
> Le 01/10/2015 02:35, Kreinovich, Vladik a écrit :
>> Dear Friends, 
>>  
>> The latest (October 2015) issue of the Notices of American Mathematical Society (AMS) have an article “Rigorous Numerics in Dynamics” by Jan Bouwe van den Berg and Jean-Philippe Lessard, which describe computer-based tools that enable to generate rigorous (proved) results about dynamical systems – as opposed to more traditional computer simulations that, die to their approximate character, so not guarantee anything about the actual system. This article can be accessed from the AMS website http://www.ams.org/notices/201509/rnoti-p1057.pdf
>>  
>> Please note that there will be an AMS Short Course on Rigorous Numerics in Dynamics in Seattle, Washington, on January 4-5, right before the January 6-9, 2016 Joint Mathematics Meeting in Seattle. This is the largest mathematics meeting in the world, it includes the annual meetings of the Mathematical Association of America (MAA) and the American Mathematical Society (AMS), with sessions and meetings of the Association for Symbolic Logic (ASL), the Association for Women in Mathematics (AWM), the National Association for Mathematicians (NAM), and the Society for Industrial and Applied Mathematics (SIAM).
>> For more information about the Joint Meeting, see http://jointmathematicsmeetings.org/jmm
>> For details about the Short Course, see http://www.ams.org/notices/201509/rnoti-p1106.pdf
>> 
>> 
>> _______________________________________________
>> FOM mailing list
>> 
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3638 bytes
Desc: not available
URL: </pipermail/fom/attachments/20151002/fb3969f8/attachment-0001.p7s>