We add, to the common combination of a While-language and a Hoare-style program logic, a constant that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete. © 2011 Springer-Verlag.
CITATION STYLE
Suenaga, K., & Hasuo, I. (2011). Programming with infinitesimals: A While-language for hybrid system modeling. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6756 LNCS, pp. 392–403). https://doi.org/10.1007/978-3-642-22012-8_31
Mendeley helps you to discover research relevant for your work.