{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:19:18Z","timestamp":1771485558606,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_34","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"462-478","source":"Crossref","is-referenced-by-count":25,"title":["Exercises in Nonstandard Static Analysis of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Ichiro","family":"Hasuo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"34_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comp. Sci.\u00a0138(1), 3\u201334 (1995)","journal-title":"Theor. Comp. Sci."},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Refining the control structure of loops using static analysis. In: EMSOFT, pp. 49\u201358 (2009)","DOI":"10.1145\/1629335.1629343"},{"issue":"3","key":"34_CR3","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1016\/j.jcss.2011.08.009","volume":"78","author":"A. Benveniste","year":"2012","unstructured":"Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci.\u00a078(3), 877\u2013910 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 300\u2013309. ACM (2007)","DOI":"10.1145\/1273442.1250769"},{"issue":"2","key":"34_CR5","doi-asserted-by":"crossref","first-page":"251","DOI":"10.3233\/FI-2009-0043","volume":"91","author":"S. Bliudze","year":"2009","unstructured":"Bliudze, S., Krob, D.: Modelling of complex systems: Systems as dataflow machines. Fundam. Inform.\u00a091(2), 251\u2013274 (2009)","journal-title":"Fundam. Inform."},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R., NavidPour, S.: Proving programs robust. In: Gyim\u00f3thy, T., Zeller, A. (eds.) SIGSOFT FSE, pp. 102\u2013112. ACM (2011)","DOI":"10.1145\/2025113.2025131"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"issue":"4","key":"34_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"R.A. Gamboa","year":"2001","unstructured":"Gamboa, R.A., Kaufmann, M.: Nonstandard analysis in ACL2. J. Autom. Reason.\u00a027(4), 323\u2013351 (2001)","journal-title":"J. Autom. Reason."},{"key":"34_CR9","doi-asserted-by":"crossref","unstructured":"Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis. Springer (1998)","DOI":"10.1007\/978-1-4612-0615-6"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D. Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided Static Analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 349\u2013365. Springer, Heidelberg (2007)"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Suenaga, K.: Exercises in Nonstandard Static Analysis of hybrid systems. Extended version with proofs (2012), www-mmm.is.s.u-tokyo.ac.jp\/~ichiro","DOI":"10.1007\/978-3-642-31424-7_34"},{"key":"34_CR12","unstructured":"Hurd, A.E., Loeb, P.A.: An Introduction to Nonstandard Real Analysis. Academic Press (1985)"},{"issue":"1","key":"34_CR13","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput.\u00a020(1), 309\u2013352 (2010)","journal-title":"J. Log. Comput."},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems\u2014Proving Theorems for Complex Dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"34_CR15","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. Tech. Rep. CMU\u2013CS\u201311\u2013144, Carnegie-Mellon Univ., Pittsburgh PA 15213 (2011)"},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"Robinson, A.: Non-standard analysis, revised edn. Princeton University Press (1996)","DOI":"10.1515\/9781400884223"},{"key":"34_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1007\/978-3-540-31954-2_38","volume-title":"Hybrid Systems: Computation and Control","author":"E. Rodr\u00edguez-Carbonell","year":"2005","unstructured":"Rodr\u00edguez-Carbonell, E., Tiwari, A.: Generating Polynomial Invariants for Hybrid Systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 590\u2013605. Springer, Heidelberg (2005)"},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 221\u2013230. ACM (2010)","DOI":"10.1145\/1755952.1755984"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 318\u2013329. ACM (2004)","DOI":"10.1145\/982962.964028"},{"issue":"1","key":"34_CR20","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods in System Design\u00a032(1), 25\u201355 (2008)","journal-title":"Formal Methods in System Design"},{"key":"34_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R. Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying Loop Invariant Generation Using Splitter Predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 703\u2013719. Springer, Heidelberg (2011)"},{"key":"34_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-22012-8_31","volume-title":"Automata, Languages and Programming","author":"K. Suenaga","year":"2011","unstructured":"Suenaga, K., Hasuo, I.: Programming with Infinitesimals: A While-Language for Hybrid System Modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 392\u2013403. Springer, Heidelberg (2011)"},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press (1993)","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:57Z","timestamp":1620129597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}