[{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","related_material":{"record":[{"status":"public","id":"4403","relation":"earlier_version"}]},"title":"Algorithmic analysis of array-accessing programs","ec_funded":1,"publist_id":"3748","citation":{"ama":"Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2012;13(3). doi:<a href=\"https://doi.org/10.1145/2287718.2287727\">10.1145/2287718.2287727</a>","ista":"Alur R, Cerny P, Weinstein S. 2012. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 13(3), 27.","apa":"Alur, R., Cerny, P., &#38; Weinstein, S. (2012). Algorithmic analysis of array-accessing programs. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/2287718.2287727\">https://doi.org/10.1145/2287718.2287727</a>","chicago":"Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2012. <a href=\"https://doi.org/10.1145/2287718.2287727\">https://doi.org/10.1145/2287718.2287727</a>.","ieee":"R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing programs,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 13, no. 3. ACM, 2012.","mla":"Alur, Rajeev, et al. “Algorithmic Analysis of Array-Accessing Programs.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 13, no. 3, 27, ACM, 2012, doi:<a href=\"https://doi.org/10.1145/2287718.2287727\">10.1145/2287718.2287727</a>.","short":"R. Alur, P. Cerny, S. Weinstein, ACM Transactions on Computational Logic (TOCL) 13 (2012)."},"quality_controlled":"1","year":"2012","date_created":"2018-12-11T12:00:36Z","day":"01","volume":13,"type":"journal_article","article_processing_charge":"No","publisher":"ACM","issue":"3","publication":"ACM Transactions on Computational Logic (TOCL)","status":"public","_id":"2967","abstract":[{"lang":"eng","text":"For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use Boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over an unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) PSPACE-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly nested loops. The second result establishes connections to automata and logics defining languages over data words."}],"intvolume":"        13","publication_status":"published","isi":1,"department":[{"_id":"ToHe"}],"article_number":"27","acknowledgement":"This research was supported in part by the NSF Cybertrust award CNS 0524059, by the European Research Council (ERC) Advanced Investigator Grant QUAREM, and by the Austrian Science Fund (FWF) project S11402-N23.","doi":"10.1145/2287718.2287727","scopus_import":"1","oa_version":"None","month":"08","external_id":{"isi":["000308370100009"]},"language":[{"iso":"eng"}],"project":[{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"}],"date_updated":"2025-09-30T08:04:33Z","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol"},{"first_name":"Scott","full_name":"Weinstein, Scott","last_name":"Weinstein"}],"date_published":"2012-08-01T00:00:00Z"},{"file":[{"checksum":"dd3d590f383bb2ac6cfda1489ac1c42a","file_size":163983,"file_id":"4882","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:11:27Z","file_name":"IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf","creator":"system","date_updated":"2020-07-14T12:46:00Z"}],"publication_status":"published","status":"public","abstract":[{"lang":"eng","text":"We consider two-player zero-sum stochastic games on graphs with ω-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode. On the basis of information, these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes (POMDPs), and the blind one-player games, known as probabilistic automata. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, Büchi, or coBüchi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability 1), limit-sure winning (i.e., winning with probability arbitrarily close to 1), and value-threshold winning (i.e., winning with probability at least ν, where ν is a given rational). "}],"_id":"3128","intvolume":"        43","pubrep_id":"303","publisher":"Springer","issue":"2","publication":"Formal Methods in System Design","article_processing_charge":"No","type":"journal_article","page":"268 - 284","day":"01","volume":43,"year":"2012","date_created":"2018-12-11T12:01:33Z","corr_author":"1","quality_controlled":"1","oa":1,"citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey of Partial-Observation Stochastic Parity Games.” <i>Formal Methods in System Design</i>. Springer, 2012. <a href=\"https://doi.org/10.1007/s10703-012-0164-2\">https://doi.org/10.1007/s10703-012-0164-2</a>.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2012). A survey of partial-observation stochastic parity games. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-012-0164-2\">https://doi.org/10.1007/s10703-012-0164-2</a>","ista":"Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 43(2), 268–284.","ama":"Chatterjee K, Doyen L, Henzinger TA. A survey of partial-observation stochastic parity games. <i>Formal Methods in System Design</i>. 2012;43(2):268-284. doi:<a href=\"https://doi.org/10.1007/s10703-012-0164-2\">10.1007/s10703-012-0164-2</a>","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation stochastic parity games,” <i>Formal Methods in System Design</i>, vol. 43, no. 2. Springer, pp. 268–284, 2012.","mla":"Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic Parity Games.” <i>Formal Methods in System Design</i>, vol. 43, no. 2, Springer, 2012, pp. 268–84, doi:<a href=\"https://doi.org/10.1007/s10703-012-0164-2\">10.1007/s10703-012-0164-2</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design 43 (2012) 268–284."},"publist_id":"3570","title":"A survey of partial-observation stochastic parity games","ec_funded":1,"file_date_updated":"2020-07-14T12:46:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["005"],"date_published":"2012-10-01T00:00:00Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_updated":"2025-09-30T07:57:51Z","language":[{"iso":"eng"}],"external_id":{"isi":["000324114600006"]},"month":"10","has_accepted_license":"1","scopus_import":"1","oa_version":"Submitted Version","doi":"10.1007/s10703-012-0164-2","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"isi":1},{"doi":"10.1007/978-3-642-31424-7_24","acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation.","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"alternative_title":["LNCS"],"date_published":"2012-07-01T00:00:00Z","author":[{"last_name":"Guet","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C","first_name":"Calin C","orcid":"0000-0001-6220-2052"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"id":"3B43276C-F248-11E8-B48F-1D18A9856A87","last_name":"Mateescu","full_name":"Mateescu, Maria","first_name":"Maria"},{"first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","last_name":"Sezgin"}],"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"date_updated":"2024-10-09T20:54:47Z","conference":{"start_date":"2012-07-07","end_date":"2012-07-13","name":"CAV: Computer Aided Verification","location":"Berkeley, CA, USA"},"language":[{"iso":"eng"}],"month":"07","oa_version":"None","scopus_import":1,"year":"2012","date_created":"2018-12-11T12:01:36Z","quality_controlled":"1","corr_author":"1","citation":{"mla":"Guet, Calin C., et al. <i>Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits</i>. Vol. 7358, Springer, 2012, pp. 294–309, doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">10.1007/978-3-642-31424-7_24</a>.","ieee":"C. C. Guet, A. Gupta, T. A. Henzinger, M. Mateescu, and A. Sezgin, “Delayed continuous time Markov chains for genetic regulatory circuits,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 294–309.","short":"C.C. Guet, A. Gupta, T.A. Henzinger, M. Mateescu, A. Sezgin, in:, Springer, 2012, pp. 294–309.","ista":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. 2012. Delayed continuous time Markov chains for genetic regulatory circuits. CAV: Computer Aided Verification, LNCS, vol. 7358, 294–309.","ama":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. Delayed continuous time Markov chains for genetic regulatory circuits. In: Vol 7358. Springer; 2012:294-309. doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">10.1007/978-3-642-31424-7_24</a>","chicago":"Guet, Calin C, Ashutosh Gupta, Thomas A Henzinger, Maria Mateescu, and Ali Sezgin. “Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,” 7358:294–309. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">https://doi.org/10.1007/978-3-642-31424-7_24</a>.","apa":"Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., &#38; Sezgin, A. (2012). Delayed continuous time Markov chains for genetic regulatory circuits (Vol. 7358, pp. 294–309). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">https://doi.org/10.1007/978-3-642-31424-7_24</a>"},"publist_id":"3561","ec_funded":1,"title":"Delayed continuous time Markov chains for genetic regulatory circuits","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","_id":"3136","abstract":[{"lang":"eng","text":"Continuous-time Markov chains (CTMC) with their rich theory and efficient simulation algorithms have been successfully used in modeling stochastic processes in diverse areas such as computer science, physics, and biology. However, systems that comprise non-instantaneous events cannot be accurately and efficiently modeled with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that allows for the specification of a lower bound on the time interval between an event's initiation and its completion, and we propose an algorithm for the computation of their behavior. Our algorithm effectively decomposes the computation into two stages: a pure CTMC governs event initiations while a deterministic process guarantees lower bounds on event completion times. Furthermore, from the nature of delayed CTMCs, we obtain a parallelized version of our algorithm. We use our formalism to model genetic regulatory circuits (biological systems where delayed events are common) and report on the results of our numerical algorithm as run on a cluster. We compare performance and accuracy of our results with results obtained by using pure CTMCs. © 2012 Springer-Verlag."}],"publisher":"Springer","type":"conference","day":"01","page":"294 - 309","volume":"7358 "},{"acknowledgement":"Research partially supported by the Danish-Chinese Center for Cyber Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB.","doi":"10.1007/978-3-642-30793-5_13","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T07:41:26Z","alternative_title":["LNCS"],"ddc":["004"],"date_published":"2012-06-01T00:00:00Z","author":[{"last_name":"Delahaye","full_name":"Delahaye, Benoît","first_name":"Benoît"},{"first_name":"Uli","full_name":"Fahrenberg, Uli","last_name":"Fahrenberg"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Legay","full_name":"Legay, Axel","first_name":"Axel"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"month":"06","has_accepted_license":"1","oa_version":"Submitted Version","scopus_import":1,"conference":{"location":"Stockholm, Sweden","name":"FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems ","end_date":"2012-06-16","start_date":"2012-06-13"},"language":[{"iso":"eng"}],"oa":1,"citation":{"short":"B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer, 2012, pp. 203–218.","ieee":"B. Delahaye, U. Fahrenberg, T. A. Henzinger, A. Legay, and D. Nickovic, “Synchronous interface theories and time triggered scheduling,” presented at the FORTE: Formal Techniques for Networked and Distributed Systems &#38; FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273, pp. 203–218.","mla":"Delahaye, Benoît, et al. <i>Synchronous Interface Theories and Time Triggered Scheduling</i>. Vol. 7273, Springer, 2012, pp. 203–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">10.1007/978-3-642-30793-5_13</a>.","ista":"Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. 2012. Synchronous interface theories and time triggered scheduling. FORTE: Formal Techniques for Networked and Distributed Systems &#38; FMOODS: Formal Methods for Open Object-Based Distributed Systems , LNCS, vol. 7273, 203–218.","ama":"Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. Synchronous interface theories and time triggered scheduling. In: Vol 7273. Springer; 2012:203-218. doi:<a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">10.1007/978-3-642-30793-5_13</a>","chicago":"Delahaye, Benoît, Uli Fahrenberg, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Synchronous Interface Theories and Time Triggered Scheduling,” 7273:203–18. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">https://doi.org/10.1007/978-3-642-30793-5_13</a>.","apa":"Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., &#38; Nickovic, D. (2012). Synchronous interface theories and time triggered scheduling (Vol. 7273, pp. 203–218). Presented at the FORTE: Formal Techniques for Networked and Distributed Systems &#38; FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-642-30793-5_13\">https://doi.org/10.1007/978-3-642-30793-5_13</a>"},"year":"2012","date_created":"2018-12-11T12:01:43Z","quality_controlled":"1","title":"Synchronous interface theories and time triggered scheduling","file_date_updated":"2020-07-14T12:46:01Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"3539","status":"public","intvolume":"      7273","_id":"3155","abstract":[{"text":"We propose synchronous interfaces, a new interface theory for discrete-time systems. We use an application to time-triggered scheduling to drive the design choices for our formalism; in particular, additionally to deriving useful mathematical properties, we focus on providing a syntax which is adapted to natural high-level system modeling. As a result, we develop an interface model that relies on a guarded-command based language and is equipped with shared variables and explicit discrete-time clocks. We define all standard interface operations: compatibility checking, composition, refinement, and shared refinement. Apart from the synchronous interface model, the contribution of this paper is the establishment of a formal relation between interface theories and real-time scheduling, where we demonstrate a fully automatic framework for the incremental computation of time-triggered schedules.","lang":"eng"}],"pubrep_id":"88","file":[{"creator":"system","date_updated":"2020-07-14T12:46:01Z","content_type":"application/pdf","relation":"main_file","file_name":"IST-2012-88-v1+1_Synchronous_interface_theories_and_time_triggered_scheduling.pdf","date_created":"2018-12-12T10:11:25Z","file_id":"4879","access_level":"open_access","checksum":"feae2e07f2d9a59843f8ddabf25d179f","file_size":493198}],"publication_status":"published","type":"conference","page":"203 - 218","day":"01","volume":7273,"publisher":"Springer"},{"quality_controlled":"1","date_created":"2018-12-11T12:01:45Z","year":"2012","citation":{"ama":"Asarin E, Donzé A, Maler O, Nickovic D. Parametric identification of temporal properties. In: Vol 7186. Springer; 2012:147-160. doi:<a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">10.1007/978-3-642-29860-8_12</a>","ista":"Asarin E, Donzé A, Maler O, Nickovic D. 2012. Parametric identification of temporal properties. RV: Runtime Verification, LNCS, vol. 7186, 147–160.","apa":"Asarin, E., Donzé, A., Maler, O., &#38; Nickovic, D. (2012). Parametric identification of temporal properties (Vol. 7186, pp. 147–160). Presented at the RV: Runtime Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">https://doi.org/10.1007/978-3-642-29860-8_12</a>","chicago":"Asarin, Eugene, Alexandre Donzé, Oded Maler, and Dejan Nickovic. “Parametric Identification of Temporal Properties,” 7186:147–60. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">https://doi.org/10.1007/978-3-642-29860-8_12</a>.","short":"E. Asarin, A. Donzé, O. Maler, D. Nickovic, in:, Springer, 2012, pp. 147–160.","ieee":"E. Asarin, A. Donzé, O. Maler, and D. Nickovic, “Parametric identification of temporal properties,” presented at the RV: Runtime Verification, San Francisco, CA, United States, 2012, vol. 7186, pp. 147–160.","mla":"Asarin, Eugene, et al. <i>Parametric Identification of Temporal Properties</i>. Vol. 7186, Springer, 2012, pp. 147–60, doi:<a href=\"https://doi.org/10.1007/978-3-642-29860-8_12\">10.1007/978-3-642-29860-8_12</a>."},"oa":1,"publist_id":"3525","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2020-07-14T12:46:01Z","title":"Parametric identification of temporal properties","publication_status":"published","file":[{"file_size":374726,"checksum":"ba4a75287008fc64b8fbf78a7476ec32","file_id":"7862","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"2012_RV_Asarin.pdf","date_created":"2020-05-15T12:50:15Z","creator":"dernst","date_updated":"2020-07-14T12:46:01Z"}],"abstract":[{"text":"Given a dense-time real-valued signal and a parameterized temporal logic formula with both magnitude and timing parameters, we compute the subset of the parameter space that renders the formula satisfied by the trace. We provide two preliminary implementations, one which follows the exact semantics and attempts to compute the validity domain by quantifier elimination in linear arithmetics and one which conducts adaptive search in the parameter space.","lang":"eng"}],"_id":"3162","intvolume":"      7186","status":"public","article_processing_charge":"No","publisher":"Springer","volume":7186,"page":"147 - 160","day":"01","type":"conference","doi":"10.1007/978-3-642-29860-8_12","department":[{"_id":"ToHe"}],"author":[{"last_name":"Asarin","full_name":"Asarin, Eugene","first_name":"Eugene"},{"first_name":"Alexandre","full_name":"Donzé, Alexandre","last_name":"Donzé"},{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"}],"date_published":"2012-01-01T00:00:00Z","alternative_title":["LNCS"],"ddc":["000"],"date_updated":"2021-01-12T07:41:29Z","language":[{"iso":"eng"}],"conference":{"end_date":"2011-09-30","start_date":"2011-09-27","location":"San Francisco, CA, United States","name":"RV: Runtime Verification"},"oa_version":"Submitted Version","scopus_import":1,"has_accepted_license":"1","month":"01"},{"publist_id":"3515","title":"Lumpability abstractions of rule based systems","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3719"}]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2018-12-11T12:01:47Z","year":"2012","quality_controlled":"1","article_type":"original","oa":1,"citation":{"apa":"Feret, J., Henzinger, T. A., Koeppl, H., &#38; Petrov, T. (2012). Lumpability abstractions of rule based systems. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2011.12.059\">https://doi.org/10.1016/j.tcs.2011.12.059</a>","chicago":"Feret, Jérôme, Thomas A Henzinger, Heinz Koeppl, and Tatjana Petrov. “Lumpability Abstractions of Rule Based Systems.” <i>Theoretical Computer Science</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.tcs.2011.12.059\">https://doi.org/10.1016/j.tcs.2011.12.059</a>.","ama":"Feret J, Henzinger TA, Koeppl H, Petrov T. Lumpability abstractions of rule based systems. <i>Theoretical Computer Science</i>. 2012;431:137-164. doi:<a href=\"https://doi.org/10.1016/j.tcs.2011.12.059\">10.1016/j.tcs.2011.12.059</a>","ista":"Feret J, Henzinger TA, Koeppl H, Petrov T. 2012. Lumpability abstractions of rule based systems. Theoretical Computer Science. 431, 137–164.","short":"J. Feret, T.A. Henzinger, H. Koeppl, T. Petrov, Theoretical Computer Science 431 (2012) 137–164.","ieee":"J. Feret, T. A. Henzinger, H. Koeppl, and T. Petrov, “Lumpability abstractions of rule based systems,” <i>Theoretical Computer Science</i>, vol. 431. Elsevier, pp. 137–164, 2012.","mla":"Feret, Jérôme, et al. “Lumpability Abstractions of Rule Based Systems.” <i>Theoretical Computer Science</i>, vol. 431, Elsevier, 2012, pp. 137–64, doi:<a href=\"https://doi.org/10.1016/j.tcs.2011.12.059\">10.1016/j.tcs.2011.12.059</a>."},"publication":"Theoretical Computer Science","publisher":"Elsevier","OA_type":"free access","article_processing_charge":"No","type":"journal_article","volume":431,"page":"137 - 164","day":"04","publication_status":"published","intvolume":"       431","_id":"3168","abstract":[{"text":"The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the combinatorial complexity by quotienting the reachable set of molecular species into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently, we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper, we prove that this quotienting yields a sufficient condition for weak lumpability (that is to say that the quotient system is still Markovian for a given set of initial distributions) and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system (which means that the conditional probability of being in a given state in the original system knowing that we are in its equivalence class is an invariant of the system). We illustrate the framework on a case study of the epidermal growth factor (EGF)/insulin receptor crosstalk.","lang":"eng"}],"status":"public","pubrep_id":"73","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.tcs.2011.12.059"}],"department":[{"_id":"ToHe"}],"isi":1,"doi":"10.1016/j.tcs.2011.12.059","acknowledgement":"We would like to thank the anonymous reviewers for their comments on the different versions of the paper. We would also like to thank Ferdinanda Camporesi for her careful reading and the useful insights that she gave us about the paper.\r\nJérôme Feret’s contribution was partially supported by the AbstractCell ANR-Chair of Excellence. Heinz Koeppl’s research is supported by the Swiss National Science Foundation, grant no. 200020-117975/1. Tatjana Petrov’s research is supported by SystemsX.ch (the Swiss Initiative in Systems Biology).","language":[{"iso":"eng"}],"external_id":{"isi":["000303302400010"]},"month":"05","oa_version":"Published Version","scopus_import":"1","date_published":"2012-05-04T00:00:00Z","author":[{"full_name":"Feret, Jérôme","last_name":"Feret","first_name":"Jérôme"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Heinz","full_name":"Koeppl, Heinz","last_name":"Koeppl"},{"first_name":"Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov","full_name":"Petrov, Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"OA_place":"publisher","date_updated":"2025-09-30T07:50:35Z"},{"external_id":{"isi":["000298529200003"]},"language":[{"iso":"eng"}],"scopus_import":"1","oa_version":"Published Version","month":"01","author":[{"last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna","first_name":"Arjun"}],"date_published":"2012-01-06T00:00:00Z","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"215543"},{"grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_updated":"2025-09-30T07:46:06Z","OA_place":"publisher","department":[{"_id":"ToHe"}],"isi":1,"doi":"10.1016/j.tcs.2011.08.002","acknowledgement":"This work was partially supported by the ERC Advanced Grant QUAREM, the FWF NFN Grant S11402-N23 (RiSE), the European Union project COMBEST and the European Network of Excellence Artist Design.","article_processing_charge":"No","OA_type":"free access","publisher":"Elsevier","issue":"1","publication":"Theoretical Computer Science","day":"06","page":"21 - 35","volume":413,"type":"journal_article","publication_status":"published","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.tcs.2011.08.002"}],"pubrep_id":"42","status":"public","_id":"3249","abstract":[{"text":"Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of &quot;fit&quot; or &quot;desirability&quot;. We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.","lang":"eng"}],"intvolume":"       413","publist_id":"3408","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5389"},{"relation":"earlier_version","id":"4393","status":"public"}]},"ec_funded":1,"title":"Simulation distances","article_type":"original","quality_controlled":"1","corr_author":"1","year":"2012","date_created":"2018-12-11T12:02:15Z","citation":{"ista":"Cerny P, Henzinger TA, Radhakrishna A. 2012. Simulation distances. Theoretical Computer Science. 413(1), 21–35.","ama":"Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. <i>Theoretical Computer Science</i>. 2012;413(1):21-35. doi:<a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">10.1016/j.tcs.2011.08.002</a>","chicago":"Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances.” <i>Theoretical Computer Science</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">https://doi.org/10.1016/j.tcs.2011.08.002</a>.","apa":"Cerny, P., Henzinger, T. A., &#38; Radhakrishna, A. (2012). Simulation distances. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">https://doi.org/10.1016/j.tcs.2011.08.002</a>","ieee":"P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” <i>Theoretical Computer Science</i>, vol. 413, no. 1. Elsevier, pp. 21–35, 2012.","mla":"Cerny, Pavol, et al. “Simulation Distances.” <i>Theoretical Computer Science</i>, vol. 413, no. 1, Elsevier, 2012, pp. 21–35, doi:<a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">10.1016/j.tcs.2011.08.002</a>.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 413 (2012) 21–35."},"oa":1},{"publication_status":"published","author":[{"first_name":"Ahmed","full_name":"Bouajjani, Ahmed","last_name":"Bouajjani"},{"last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara","first_name":"Cezara"},{"full_name":"Enea, Constantin","last_name":"Enea","first_name":"Constantin"},{"last_name":"Sighireanu","full_name":"Sighireanu, Mihaela","first_name":"Mihaela"}],"date_published":"2012-02-26T00:00:00Z","alternative_title":["LNCS"],"intvolume":"      7148","_id":"3253","abstract":[{"lang":"eng","text":"We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs."}],"status":"public","date_updated":"2024-10-21T06:02:58Z","language":[{"iso":"eng"}],"conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","location":"Philadelphia, PA, USA","start_date":"2012-01-22","end_date":"2012-01-24"},"publisher":"Springer","scopus_import":"1","volume":7148,"oa_version":"None","day":"26","page":"1 - 22","month":"02","type":"conference","quality_controlled":"1","date_created":"2018-12-11T12:02:17Z","doi":"10.1007/978-3-642-27940-9_1","year":"2012","citation":{"ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Abstract domains for automated reasoning about list manipulating programs with infinite data. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 1–22.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Abstract domains for automated reasoning about list manipulating programs with infinite data. In: Vol 7148. Springer; 2012:1-22. doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">10.1007/978-3-642-27940-9_1</a>","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data,” 7148:1–22. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">https://doi.org/10.1007/978-3-642-27940-9_1</a>.","apa":"Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Abstract domains for automated reasoning about list manipulating programs with infinite data (Vol. 7148, pp. 1–22). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">https://doi.org/10.1007/978-3-642-27940-9_1</a>","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Abstract domains for automated reasoning about list manipulating programs with infinite data,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 1–22.","mla":"Bouajjani, Ahmed, et al. <i>Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data</i>. Vol. 7148, Springer, 2012, pp. 1–22, doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">10.1007/978-3-642-27940-9_1</a>.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2012, pp. 1–22."},"acknowledgement":"This work was partly supported by the French National Research Agency (ANR) project Veridyc (ANR-09-SEGI-016).","publist_id":"3404","department":[{"_id":"ToHe"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","title":"Abstract domains for automated reasoning about list manipulating programs with infinite data"},{"article_processing_charge":"No","publication":"Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering","publisher":"ACM","day":"01","type":"conference","publication_status":"published","arxiv":1,"main_file_link":[{"url":"http://arxiv.org/abs/1109.6926","open_access":"1"}],"abstract":[{"text":"Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition Ψ - usually a state predicate - such that the program satisfies the specification under the condition Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.","lang":"eng"}],"_id":"1384","status":"public","publist_id":"5826","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Conditional model checking: A technique to pass information between verifiers","ec_funded":1,"quality_controlled":"1","date_created":"2018-12-11T11:51:42Z","year":"2012","citation":{"mla":"Beyer, Dirk, et al. “Conditional Model Checking: A Technique to Pass Information between Verifiers.” <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>, 57, ACM, 2012, doi:<a href=\"https://doi.org/10.1145/2393596.2393664\">10.1145/2393596.2393664</a>.","short":"D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, ACM, 2012.","ieee":"D. Beyer, T. A. Henzinger, M. Keremoglu, and P. Wendler, “Conditional model checking: A technique to pass information between verifiers,” in <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>, Cary, NC, USA, 2012.","chicago":"Beyer, Dirk, Thomas A Henzinger, Mehmet Keremoglu, and Philipp Wendler. “Conditional Model Checking: A Technique to Pass Information between Verifiers.” In <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>. ACM, 2012. <a href=\"https://doi.org/10.1145/2393596.2393664\">https://doi.org/10.1145/2393596.2393664</a>.","apa":"Beyer, D., Henzinger, T. A., Keremoglu, M., &#38; Wendler, P. (2012). Conditional model checking: A technique to pass information between verifiers. In <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>. Cary, NC, USA: ACM. <a href=\"https://doi.org/10.1145/2393596.2393664\">https://doi.org/10.1145/2393596.2393664</a>","ista":"Beyer D, Henzinger TA, Keremoglu M, Wendler P. 2012. Conditional model checking: A technique to pass information between verifiers. Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. FSE: Foundations of Software Engineering, 57.","ama":"Beyer D, Henzinger TA, Keremoglu M, Wendler P. Conditional model checking: A technique to pass information between verifiers. In: <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>. ACM; 2012. doi:<a href=\"https://doi.org/10.1145/2393596.2393664\">10.1145/2393596.2393664</a>"},"oa":1,"external_id":{"arxiv":["1109.6926"]},"language":[{"iso":"eng"}],"conference":{"location":"Cary, NC, USA","name":"FSE: Foundations of Software Engineering","end_date":"2012-11-16","start_date":"2012-11-11"},"oa_version":"Preprint","scopus_import":"1","month":"11","author":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"Dirk"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"full_name":"Keremoglu, Mehmet","last_name":"Keremoglu","first_name":"Mehmet"},{"full_name":"Wendler, Philipp","last_name":"Wendler","first_name":"Philipp"}],"date_published":"2012-11-01T00:00:00Z","date_updated":"2025-06-11T08:07:37Z","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"article_number":"57","department":[{"_id":"ToHe"}],"doi":"10.1145/2393596.2393664","acknowledgement":"This  research  was  supported  by  the  Canadian  NSERC grant   RGPIN   341819-07,    the   ERC   Advanced   Grant QUAREM, and the Austrian Science Fund NFN RiSE."},{"title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","year":"2012","date_created":"2022-03-21T07:58:39Z","quality_controlled":"1","corr_author":"1","citation":{"apa":"Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in <i>Automated Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182."},"publisher":"Springer","publication":"Automated Technology for Verification and Analysis","article_processing_charge":"No","type":"conference","series_title":"LNCS","page":"167-182","day":"15","volume":7561,"publication_status":"published","status":"public","_id":"10903","abstract":[{"text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.","lang":"eng"}],"intvolume":"      7561","department":[{"_id":"ToHe"}],"doi":"10.1007/978-3-642-33386-6_14","publication_identifier":{"eisbn":["9783642333866"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642333859"]},"acknowledgement":"This work has been partially supported by the French ANR project Veridyc","conference":{"location":"Thiruvananthapuram, India","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2012-10-06","start_date":"2012-10-03"},"language":[{"iso":"eng"}],"month":"10","oa_version":"None","scopus_import":"1","alternative_title":["LNCS"],"date_published":"2012-10-15T00:00:00Z","author":[{"last_name":"Bouajjani","full_name":"Bouajjani, Ahmed","first_name":"Ahmed"},{"last_name":"Dragoi","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara"},{"first_name":"Constantin","full_name":"Enea, Constantin","last_name":"Enea"},{"first_name":"Mihaela","last_name":"Sighireanu","full_name":"Sighireanu, Mihaela"}],"place":"Berlin, Heidelberg","date_updated":"2024-10-09T21:02:34Z"},{"doi":"10.1007/978-3-642-28756-5_46","editor":[{"last_name":"Flanagan","full_name":"Flanagan, Cormac","first_name":"Cormac"},{"last_name":"König","full_name":"König, Barbara","first_name":"Barbara"}],"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642287558"],"eisbn":["9783642287565"],"issn":["0302-9743"]},"department":[{"_id":"ToHe"}],"place":"Berlin, Heidelberg","author":[{"full_name":"Grebenshchikov, Sergey","last_name":"Grebenshchikov","first_name":"Sergey"},{"last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh"},{"last_name":"Lopes","full_name":"Lopes, Nuno P.","first_name":"Nuno P."},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"first_name":"Andrey","last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey"}],"date_published":"2012-04-01T00:00:00Z","alternative_title":["LNCS"],"date_updated":"2024-10-09T21:02:32Z","language":[{"iso":"eng"}],"conference":{"location":"Tallinn, Estonia","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2012-04-01","start_date":"2012-03-24"},"scopus_import":"1","oa_version":"Published Version","month":"04","corr_author":"1","quality_controlled":"1","date_created":"2022-03-21T08:03:30Z","year":"2012","citation":{"short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>.","ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>.","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38; B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>"},"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"HSF(C): A software verifier based on Horn clauses","publication_status":"published","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"_id":"10906","intvolume":"      7214","abstract":[{"lang":"eng","text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool."}],"status":"public","article_processing_charge":"No","publication":"Tools and Algorithms for the Construction and Analysis of Systems","publisher":"Springer","volume":7214,"page":"549-551","day":"01","series_title":"LNCS","type":"conference"},{"publication_status":"published","status":"public","pmid":1,"_id":"2302","intvolume":"        10","abstract":[{"text":"We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only &quot;significant&quot; mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model's variables.","lang":"eng"}],"article_processing_charge":"No","publisher":"IEEE","issue":"2","publication":"IEEE ACM Transactions on Computational Biology and Bioinformatics","page":"310 - 322","day":"03","volume":10,"type":"journal_article","corr_author":"1","quality_controlled":"1","year":"2012","date_created":"2018-12-11T11:56:52Z","citation":{"short":"T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology and Bioinformatics 10 (2012) 310–322.","ieee":"T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical reaction networks,” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>, vol. 10, no. 2. IEEE, pp. 310–322, 2012.","mla":"Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:<a href=\"https://doi.org/10.1109/TCBB.2012.91\">10.1109/TCBB.2012.91</a>.","apa":"Henzinger, T. A., &#38; Mateescu, M. (2012). The propagation approach for computing biochemical reaction networks. <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>. IEEE. <a href=\"https://doi.org/10.1109/TCBB.2012.91\">https://doi.org/10.1109/TCBB.2012.91</a>","chicago":"Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/TCBB.2012.91\">https://doi.org/10.1109/TCBB.2012.91</a>.","ama":"Henzinger TA, Mateescu M. The propagation approach for computing biochemical reaction networks. <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>. 2012;10(2):310-322. doi:<a href=\"https://doi.org/10.1109/TCBB.2012.91\">10.1109/TCBB.2012.91</a>","ista":"Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 10(2), 310–322."},"publist_id":"4625","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"The propagation approach for computing biochemical reaction networks","ec_funded":1,"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Mateescu","full_name":"Mateescu, Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria"}],"date_published":"2012-07-03T00:00:00Z","date_updated":"2025-09-29T14:17:43Z","project":[{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"}],"external_id":{"isi":["000323504100006"],"pmid":["22778152"]},"language":[{"iso":"eng"}],"scopus_import":"1","oa_version":"None","month":"07","doi":"10.1109/TCBB.2012.91","isi":1,"department":[{"_id":"ToHe"},{"_id":"CaGu"}]},{"publication_status":"published","status":"public","_id":"494","abstract":[{"text":"We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata.","lang":"eng"}],"intvolume":"        13","publisher":"ACM","issue":"4","publication":"ACM Transactions on Computational Logic (TOCL)","article_processing_charge":"No","type":"journal_article","day":"01","volume":13,"year":"2012","date_created":"2018-12-11T11:46:47Z","quality_controlled":"1","corr_author":"1","citation":{"ama":"Boker U, Kupferman O. Translating to Co-Büchi made tight, unified, and useful. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2012;13(4). doi:<a href=\"https://doi.org/10.1145/2362355.2362357\">10.1145/2362355.2362357</a>","ista":"Boker U, Kupferman O. 2012. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 13(4), 29.","apa":"Boker, U., &#38; Kupferman, O. (2012). Translating to Co-Büchi made tight, unified, and useful. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/2362355.2362357\">https://doi.org/10.1145/2362355.2362357</a>","chicago":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2012. <a href=\"https://doi.org/10.1145/2362355.2362357\">https://doi.org/10.1145/2362355.2362357</a>.","ieee":"U. Boker and O. Kupferman, “Translating to Co-Büchi made tight, unified, and useful,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 13, no. 4. ACM, 2012.","mla":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 13, no. 4, 29, ACM, 2012, doi:<a href=\"https://doi.org/10.1145/2362355.2362357\">10.1145/2362355.2362357</a>.","short":"U. Boker, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 13 (2012)."},"publist_id":"7326","title":"Translating to Co-Büchi made tight, unified, and useful","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2012-10-01T00:00:00Z","author":[{"first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","full_name":"Boker, Udi"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"date_updated":"2025-09-30T08:35:21Z","language":[{"iso":"eng"}],"external_id":{"isi":["000310163600002"]},"month":"10","scopus_import":"1","oa_version":"None","doi":"10.1145/2362355.2362357","article_number":"29","isi":1,"department":[{"_id":"ToHe"}]},{"year":"2012","date_created":"2018-12-18T13:01:46Z","corr_author":"1","quality_controlled":"1","oa":1,"citation":{"chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In <i>10th International Symposium on Automated Technology for Verification and Analysis</i>, 7561:107–21. Springer Nature, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>.","apa":"Gupta, A. (2012). Improved single pass algorithms for resolution proof reduction. In <i>10th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121). Thiruvananthapuram, Kerala, India: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>","ista":"Gupta A. 2012. Improved single pass algorithms for resolution proof reduction. 10th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 107–121.","ama":"Gupta A. Improved single pass algorithms for resolution proof reduction. In: <i>10th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 7561. Springer Nature; 2012:107-121. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>","ieee":"A. Gupta, “Improved single pass algorithms for resolution proof reduction,” in <i>10th International Symposium on Automated Technology for Verification and Analysis</i>, Thiruvananthapuram, Kerala, India, 2012, vol. 7561, pp. 107–121.","short":"A. Gupta, in:, 10th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2012, pp. 107–121.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” <i>10th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 7561, Springer Nature, 2012, pp. 107–21, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>."},"ec_funded":1,"title":"Improved single pass algorithms for resolution proof reduction","file_date_updated":"2020-07-14T12:47:10Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2018-12-18T13:07:35Z","file_name":"2012_ATVA_Gupta.pdf","content_type":"application/pdf","relation":"main_file","date_updated":"2020-07-14T12:47:10Z","creator":"dernst","checksum":"68415837a315de3cc4d120f6019d752c","file_size":465502,"access_level":"open_access","file_id":"5746"}],"publication_status":"published","status":"public","_id":"5745","intvolume":"      7561","abstract":[{"text":"Unsatisfiability proofs find many applications in verification. Today, many SAT solvers are capable of producing resolution proofs of unsatisfiability. For efficiency smaller proofs are preferred over bigger ones. The solvers apply proof reduction methods to remove redundant parts of the proofs while and after generating the proofs. One method of reducing resolution proofs is redundant resolution reduction, i.e., removing repeated pivots in the paths of resolution proofs (aka Pivot recycle). The known single pass algorithm only tries to remove redundancies in the parts of the proof that are trees. In this paper, we present three modifications to improve the algorithm such that the redundancies can be found in the parts of the proofs that are DAGs. The first modified algorithm covers greater number of redundancies as compared to the known algorithm without incurring any additional cost. The second modified algorithm covers even greater number of the redundancies but it may have longer run times. Our third modified algorithm is parametrized and can trade off between run times and the coverage of the redundancies. We have implemented our algorithms in OpenSMT and applied them on unsatisfiability proofs of 198 examples from plain MUS track of SAT11 competition. The first and second algorithm additionally remove 0.89% and 10.57% of clauses respectively as compared to the original algorithm. For certain value of the parameter, the third algorithm removes almost as many clauses as the second algorithm but is significantly faster.","lang":"eng"}],"pubrep_id":"180","publisher":"Springer Nature","publication":"10th International Symposium on Automated Technology for Verification and Analysis","article_processing_charge":"No","type":"conference","day":"28","page":"107-121","volume":7561,"doi":"10.1007/978-3-642-33386-6_10","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642333859"],"issn":["0302-9743"],"eisbn":["9783642333866"]},"acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative\r\nReactive Modeling (QUAREM).","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"ddc":["005"],"date_published":"2012-09-28T00:00:00Z","author":[{"first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"}],"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"date_updated":"2025-04-15T07:56:27Z","OA_place":"repository","conference":{"location":"Thiruvananthapuram, Kerala, India","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2012-10-06","start_date":"2012-10-03"},"language":[{"iso":"eng"}],"month":"09","has_accepted_license":"1","oa_version":"Submitted Version","scopus_import":"1"},{"external_id":{"isi":["000298464800003"]},"language":[{"iso":"eng"}],"scopus_import":"1","oa_version":"None","month":"02","author":[{"first_name":"Arkadeb","last_name":"Ghosal","full_name":"Ghosal, Arkadeb"},{"first_name":"Daniel","full_name":"Iercan, Daniel","last_name":"Iercan"},{"first_name":"Christoph","full_name":"Kirsch, Christoph","last_name":"Kirsch"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Sangiovanni Vincentelli","full_name":"Sangiovanni Vincentelli, Alberto","first_name":"Alberto"}],"date_published":"2012-02-01T00:00:00Z","date_updated":"2025-09-30T07:33:11Z","department":[{"_id":"ToHe"}],"isi":1,"doi":"10.1016/j.scico.2010.06.004","article_processing_charge":"No","publication":"Science of Computer Programming","issue":"2","publisher":"Elsevier","volume":77,"day":"01","page":"96 - 112","type":"journal_article","publication_status":"published","_id":"3836","abstract":[{"lang":"eng","text":"Hierarchical Timing Language (HTL) is a coordination language for distributed, hard real-time applications. HTL is a hierarchical extension of Giotto and, like its predecessor, based on the logical execution time (LET) paradigm of real-time programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine (or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram structure needs to be flattened; the flattening makes separatecompilation difficult, and may result in E machinecode of exponential size. In this paper, we propose a generalization of the E machine, which supports a hierarchicalprogram structure at runtime through real-time trigger mechanisms that are arranged in a tree. We present the generalized E machine, and a modular compiler for HTL that generates code of linear size. The compiler may generate code for any part of a given HTL program separately in any order."}],"intvolume":"        77","status":"public","publist_id":"2370","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code","quality_controlled":"1","date_created":"2018-12-11T12:05:26Z","year":"2012","citation":{"apa":"Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., &#38; Sangiovanni Vincentelli, A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. <i>Science of Computer Programming</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">https://doi.org/10.1016/j.scico.2010.06.004</a>","chicago":"Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” <i>Science of Computer Programming</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">https://doi.org/10.1016/j.scico.2010.06.004</a>.","ama":"Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. <i>Science of Computer Programming</i>. 2012;77(2):96-112. doi:<a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">10.1016/j.scico.2010.06.004</a>","ista":"Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. 77(2), 96–112.","short":"A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli, Science of Computer Programming 77 (2012) 96–112.","mla":"Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” <i>Science of Computer Programming</i>, vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:<a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">10.1016/j.scico.2010.06.004</a>.","ieee":"A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli, “Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code,” <i>Science of Computer Programming</i>, vol. 77, no. 2. Elsevier, pp. 96–112, 2012."}},{"day":"02","page":"394 - 413","volume":78,"type":"journal_article","article_processing_charge":"No","publisher":"Elsevier","issue":"2","publication":"Journal of Computer and System Sciences","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.jcss.2011.05.002"}],"status":"public","_id":"3846","abstract":[{"lang":"eng","text":"We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications."}],"intvolume":"        78","file":[{"file_size":336450,"checksum":"241b939deb4517cdd4426d49c67e3fa2","file_id":"5897","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_name":"a_survey_of_stochastic_omega-regular_games.pdf","date_created":"2019-01-29T10:54:28Z","creator":"kschuh","date_updated":"2020-07-14T12:46:17Z"}],"publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"A survey of stochastic ω regular games","file_date_updated":"2020-07-14T12:46:17Z","publist_id":"2341","citation":{"short":"K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78 (2012) 394–413.","ieee":"K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,” <i>Journal of Computer and System Sciences</i>, vol. 78, no. 2. Elsevier, pp. 394–413, 2012.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω Regular Games.” <i>Journal of Computer and System Sciences</i>, vol. 78, no. 2, Elsevier, 2012, pp. 394–413, doi:<a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">10.1016/j.jcss.2011.05.002</a>.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2012). A survey of stochastic ω regular games. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">https://doi.org/10.1016/j.jcss.2011.05.002</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic ω Regular Games.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">https://doi.org/10.1016/j.jcss.2011.05.002</a>.","ama":"Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. <i>Journal of Computer and System Sciences</i>. 2012;78(2):394-413. doi:<a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">10.1016/j.jcss.2011.05.002</a>","ista":"Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 78(2), 394–413."},"oa":1,"article_type":"original","quality_controlled":"1","corr_author":"1","year":"2012","date_created":"2018-12-11T12:05:29Z","has_accepted_license":"1","oa_version":"Submitted Version","scopus_import":"1","month":"03","external_id":{"isi":["000299719100002"]},"language":[{"iso":"eng"}],"date_updated":"2025-09-30T07:32:39Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"}],"ddc":["000"],"date_published":"2012-03-02T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"isi":1,"acknowledgement":"This research was supported in part by the ONR grant N00014-02-1-0671, by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949, and CCR-0225610.","doi":"10.1016/j.jcss.2011.05.002"},{"doi":"10.1007/978-3-642-27940-9_29","acknowledgement":"This research was supported in part by the European Research Council (ERC) Advanced Investigator Grant QUAREM and by the Austrian Science Fund (FWF) project S11402-N23.","department":[{"_id":"ToHe"}],"author":[{"first_name":"Damien","orcid":"0000-0002-3197-8736","full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"},{"full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"alternative_title":["LNCS"],"ddc":["000","005"],"date_published":"2012-01-01T00:00:00Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"date_updated":"2026-04-09T14:35:23Z","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","location":"Philadelphia, PA, USA","start_date":"2012-01-22","end_date":"2012-01-24"},"language":[{"iso":"eng"}],"has_accepted_license":"1","scopus_import":"1","oa_version":"Submitted Version","month":"01","quality_controlled":"1","year":"2012","date_created":"2018-12-11T12:02:16Z","citation":{"ista":"Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 445–460.","ama":"Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition systems. In: Vol 7148. Springer; 2012:445-460. doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">10.1007/978-3-642-27940-9_29</a>","chicago":"Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">https://doi.org/10.1007/978-3-642-27940-9_29</a>.","apa":"Zufferey, D., Wies, T., &#38; Henzinger, T. A. (2012). Ideal abstractions for well structured transition systems (Vol. 7148, pp. 445–460). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">https://doi.org/10.1007/978-3-642-27940-9_29</a>","mla":"Zufferey, Damien, et al. <i>Ideal Abstractions for Well Structured Transition Systems</i>. Vol. 7148, Springer, 2012, pp. 445–60, doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">10.1007/978-3-642-27940-9_29</a>.","short":"D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.","ieee":"D. Zufferey, T. Wies, and T. A. Henzinger, “Ideal abstractions for well structured transition systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 445–460."},"oa":1,"publist_id":"3406","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"1405","relation":"dissertation_contains","status":"public"}]},"title":"Ideal abstractions for well structured transition systems","ec_funded":1,"file_date_updated":"2020-07-14T12:46:05Z","file":[{"file_name":"IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf","date_created":"2018-12-12T10:09:35Z","content_type":"application/pdf","relation":"main_file","date_updated":"2020-07-14T12:46:05Z","creator":"system","file_size":217104,"checksum":"f2f0d55efa32309ad1fe65a5fcaad90c","access_level":"open_access","file_id":"4759"}],"publication_status":"published","pubrep_id":"100","status":"public","_id":"3251","intvolume":"      7148","abstract":[{"text":"Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system.","lang":"eng"}],"publisher":"Springer","day":"01","page":"445 - 460","volume":7148,"type":"conference"},{"title":"Solving recursion-free Horn clauses over LI+UIF","ec_funded":1,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publist_id":"3383","citation":{"mla":"Gupta, Ashutosh, et al. <i>Solving Recursion-Free Horn Clauses over LI+UIF</i>. Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:<a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">10.1007/978-3-642-25318-8_16</a>.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Solving recursion-free Horn clauses over LI+UIF,” presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan, 2011, vol. 7078, pp. 188–203.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203.","ista":"Gupta A, Popeea C, Rybalchenko A. 2011. Solving recursion-free Horn clauses over LI+UIF. APLAS: Asian Symposium on Programming Languages and Systems, LNCS, vol. 7078, 188–203.","ama":"Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over LI+UIF. In: Yang H, ed. Vol 7078. Springer; 2011:188-203. doi:<a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">10.1007/978-3-642-25318-8_16</a>","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Solving Recursion-Free Horn Clauses over LI+UIF.” edited by Hongseok Yang, 7078:188–203. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">https://doi.org/10.1007/978-3-642-25318-8_16</a>.","apa":"Gupta, A., Popeea, C., &#38; Rybalchenko, A. (2011). Solving recursion-free Horn clauses over LI+UIF. In H. Yang (Ed.) (Vol. 7078, pp. 188–203). Presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan: Springer. <a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">https://doi.org/10.1007/978-3-642-25318-8_16</a>"},"year":"2011","date_created":"2018-12-11T12:02:20Z","quality_controlled":"1","type":"conference","day":"05","page":"188 - 203","volume":7078,"publisher":"Springer","status":"public","intvolume":"      7078","abstract":[{"lang":"eng","text":"Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms."}],"_id":"3264","publication_status":"published","department":[{"_id":"ToHe"}],"editor":[{"last_name":"Yang","full_name":"Yang, Hongseok","first_name":"Hongseok"}],"doi":"10.1007/978-3-642-25318-8_16","month":"12","oa_version":"None","scopus_import":"1","conference":{"location":"Kenting, Taiwan","name":"APLAS: Asian Symposium on Programming Languages and Systems","end_date":"2011-12-07","start_date":"2011-12-05"},"language":[{"iso":"eng"}],"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"date_updated":"2024-10-21T06:03:01Z","alternative_title":["LNCS"],"date_published":"2011-12-05T00:00:00Z","author":[{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh"},{"last_name":"Popeea","full_name":"Popeea, Corneliu","first_name":"Corneliu"},{"full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko","first_name":"Andrey"}]},{"oa":1,"citation":{"short":"T.A. Henzinger, M. Mateescu, in:, Springer, 2011, pp. 1–3.","mla":"Henzinger, Thomas A., and Maria Mateescu. <i>Propagation Models for Computing Biochemical Reaction Networks</i>. Springer, 2011, pp. 1–3, doi:<a href=\"https://doi.org/10.1145/2037509.2037510\">10.1145/2037509.2037510</a>.","ieee":"T. A. Henzinger and M. Mateescu, “Propagation models for computing biochemical reaction networks,” presented at the CMSB: Computational Methods in Systems Biology, Paris, France, 2011, pp. 1–3.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Propagation Models for Computing Biochemical Reaction Networks,” 1–3. Springer, 2011. <a href=\"https://doi.org/10.1145/2037509.2037510\">https://doi.org/10.1145/2037509.2037510</a>.","apa":"Henzinger, T. A., &#38; Mateescu, M. (2011). Propagation models for computing biochemical reaction networks (pp. 1–3). Presented at the CMSB: Computational Methods in Systems Biology, Paris, France: Springer. <a href=\"https://doi.org/10.1145/2037509.2037510\">https://doi.org/10.1145/2037509.2037510</a>","ista":"Henzinger TA, Mateescu M. 2011. Propagation models for computing biochemical reaction networks. CMSB: Computational Methods in Systems Biology, 1–3.","ama":"Henzinger TA, Mateescu M. Propagation models for computing biochemical reaction networks. In: Springer; 2011:1-3. doi:<a href=\"https://doi.org/10.1145/2037509.2037510\">10.1145/2037509.2037510</a>"},"year":"2011","date_created":"2018-12-11T12:02:32Z","corr_author":"1","quality_controlled":"1","title":"Propagation models for computing biochemical reaction networks","file_date_updated":"2020-07-14T12:46:06Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publist_id":"3341","status":"public","_id":"3299","abstract":[{"text":"We introduce propagation models, a formalism designed to support general and efficient data structures for the transient analysis of biochemical reaction networks. We give two use cases for propagation abstract data types: the uniformization method and numerical integration. We also sketch an implementation of a propagation abstract data type, which uses abstraction to approximate states.","lang":"eng"}],"pubrep_id":"92","file":[{"date_created":"2018-12-12T10:07:50Z","file_name":"IST-2012-92-v1+1_Propagation_models_for_computing_biochemical_reaction_networks.pdf","relation":"main_file","content_type":"application/pdf","date_updated":"2020-07-14T12:46:06Z","creator":"system","file_size":255780,"checksum":"7f5c65509db1a9fb049abedd9663ed06","access_level":"open_access","file_id":"4649"}],"publication_status":"published","type":"conference","day":"21","page":"1 - 3","publisher":"Springer","doi":"10.1145/2037509.2037510","department":[{"_id":"ToHe"}],"date_updated":"2024-10-09T20:54:34Z","ddc":["000","004"],"date_published":"2011-09-21T00:00:00Z","author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Mateescu, Maria","last_name":"Mateescu","first_name":"Maria"}],"month":"09","has_accepted_license":"1","oa_version":"Submitted Version","scopus_import":1,"conference":{"start_date":"2011-09-21","end_date":"2011-09-23","name":"CMSB: Computational Methods in Systems Biology","location":"Paris, France"},"language":[{"iso":"eng"}]},{"conference":{"name":"WCSB: Workshop on Computational Systems Biology (TICSP)"},"publisher":"Tampere International Center for Signal Processing","language":[{"iso":"eng"}],"type":"conference","month":"01","has_accepted_license":"1","day":"01","oa_version":"Submitted Version","ddc":["005","570"],"date_published":"2011-01-01T00:00:00Z","author":[{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Mateescu","full_name":"Mateescu, Maria","first_name":"Maria"}],"file":[{"file_size":240820,"checksum":"aa4d7a832a5419e6c0090650ebff2b9a","access_level":"open_access","file_id":"5331","file_name":"IST-2012-91-v1+1_Tail_approximation_for_the_chemical_master_equation.pdf","date_created":"2018-12-12T10:18:12Z","content_type":"application/pdf","relation":"main_file","date_updated":"2020-07-14T12:46:06Z","creator":"system"}],"publication_status":"published","date_updated":"2024-10-09T20:54:34Z","status":"public","_id":"3301","abstract":[{"lang":"eng","text":"The chemical master equation is a differential equation describing the time evolution of the probability distribution over the possible “states” of a biochemical system. The solution of this equation is of interest within the systems biology field ever since the importance of the molec- ular noise has been acknowledged. Unfortunately, most of the systems do not have analytical solutions, and numerical solutions suffer from the course of dimensionality and therefore need to be approximated. Here, we introduce the concept of tail approximation, which retrieves an approximation of the probabilities in the tail of a distribution from the total probability of the tail and its conditional expectation. This approximation method can then be used to numerically compute the solution of the chemical master equation on a subset of the state space, thus fighting the explosion of the state space, for which this problem is renowned."}],"pubrep_id":"91","publist_id":"3339","title":"Tail approximation for the chemical master equation","file_date_updated":"2020-07-14T12:46:06Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"year":"2011","date_created":"2018-12-11T12:02:33Z","quality_controlled":"1","corr_author":"1","oa":1,"citation":{"short":"T.A. Henzinger, M. Mateescu, in:, Tampere International Center for Signal Processing, 2011.","mla":"Henzinger, Thomas A., and Maria Mateescu. <i>Tail Approximation for the Chemical Master Equation</i>. Tampere International Center for Signal Processing, 2011.","ieee":"T. A. Henzinger and M. Mateescu, “Tail approximation for the chemical master equation,” presented at the WCSB: Workshop on Computational Systems Biology (TICSP), 2011.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Tail Approximation for the Chemical Master Equation.” Tampere International Center for Signal Processing, 2011.","apa":"Henzinger, T. A., &#38; Mateescu, M. (2011). Tail approximation for the chemical master equation. Presented at the WCSB: Workshop on Computational Systems Biology (TICSP), Tampere International Center for Signal Processing.","ista":"Henzinger TA, Mateescu M. 2011. Tail approximation for the chemical master equation. WCSB: Workshop on Computational Systems Biology (TICSP).","ama":"Henzinger TA, Mateescu M. Tail approximation for the chemical master equation. In: Tampere International Center for Signal Processing; 2011."}}]