[{"extern":"1","month":"09","date_created":"2018-12-11T12:09:01Z","page":"76 - 92","quality_controlled":"1","publication":"Proceedings of the 2nd International Conference on Embedded Software","intvolume":"      2491","status":"public","publisher":"ACM","day":"25","alternative_title":["LNCS"],"type":"conference","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"},{"last_name":"Matic","full_name":"Matic, Slobodan","first_name":"Slobodan"}],"citation":{"ama":"Henzinger TA, Kirsch C, Majumdar R, Matic S. Time-safety checking for embedded programs. In: <i>Proceedings of the 2nd International Conference on Embedded Software</i>. Vol 2491. ACM; 2002:76-92. doi:<a href=\"https://doi.org/10.1007/3-540-45828-X_7\">10.1007/3-540-45828-X_7</a>","apa":"Henzinger, T. A., Kirsch, C., Majumdar, R., &#38; Matic, S. (2002). Time-safety checking for embedded programs. In <i>Proceedings of the 2nd International Conference on Embedded Software</i> (Vol. 2491, pp. 76–92). Grenoble, France: ACM. <a href=\"https://doi.org/10.1007/3-540-45828-X_7\">https://doi.org/10.1007/3-540-45828-X_7</a>","short":"T.A. Henzinger, C. Kirsch, R. Majumdar, S. Matic, in:, Proceedings of the 2nd International Conference on Embedded Software, ACM, 2002, pp. 76–92.","mla":"Henzinger, Thomas A., et al. “Time-Safety Checking for Embedded Programs.” <i>Proceedings of the 2nd International Conference on Embedded Software</i>, vol. 2491, ACM, 2002, pp. 76–92, doi:<a href=\"https://doi.org/10.1007/3-540-45828-X_7\">10.1007/3-540-45828-X_7</a>.","chicago":"Henzinger, Thomas A, Christoph Kirsch, Ritankar Majumdar, and Slobodan Matic. “Time-Safety Checking for Embedded Programs.” In <i>Proceedings of the 2nd International Conference on Embedded Software</i>, 2491:76–92. ACM, 2002. <a href=\"https://doi.org/10.1007/3-540-45828-X_7\">https://doi.org/10.1007/3-540-45828-X_7</a>.","ista":"Henzinger TA, Kirsch C, Majumdar R, Matic S. 2002. Time-safety checking for embedded programs. Proceedings of the 2nd International Conference on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 76–92.","ieee":"T. A. Henzinger, C. Kirsch, R. Majumdar, and S. Matic, “Time-safety checking for embedded programs,” in <i>Proceedings of the 2nd International Conference on Embedded Software</i>, Grenoble, France, 2002, vol. 2491, pp. 76–92."},"conference":{"location":"Grenoble, France","name":"EMSOFT: Embedded Software ","end_date":"2002-10-09","start_date":"2002-10-07"},"title":"Time-safety checking for embedded programs","language":[{"iso":"eng"}],"doi":"10.1007/3-540-45828-X_7","acknowledgement":"Supported in part by the DARPA SEC grant F33615-C-98-3614, MARCO GSRC grant 98-DT-660, AFOSR MURI grant F49620-00-1-0327, NSF grant CCR-9988172, and a Microsoft Research Fellowship.","abstract":[{"lang":"eng","text":"Giotto is a platform-independent language for specifying software for high-performance control applications. In this paper we present a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We show that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs."}],"_id":"4470","date_published":"2002-09-25T00:00:00Z","article_processing_charge":"No","volume":2491,"publication_status":"published","publist_id":"259","year":"2002","oa_version":"None","date_updated":"2023-06-05T08:50:59Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publication_identifier":{"isbn":["9783540443070"]}},{"publisher":"Springer","status":"public","intvolume":"      2380","publication":"Proceedings of the 29th International Colloquium on Automata, Languages and Programming","quality_controlled":"1","page":"644 - 656","date_created":"2018-12-11T12:09:01Z","month":"06","extern":"1","acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003, the DARPA contract NAG2-1214, and the NSF grant CCR-9988172.","doi":"10.1007/3-540-45465-9_55","language":[{"iso":"eng"}],"title":"Synthesis of uninitialized systems","conference":{"location":"Malaga, Spain","name":"ICALP: Automata, Languages and Programming","start_date":"2002-07-08","end_date":"2002-07-13"},"citation":{"mla":"Henzinger, Thomas A., et al. “Synthesis of Uninitialized Systems.” <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>, vol. 2380, Springer, 2002, pp. 644–56, doi:<a href=\"https://doi.org/10.1007/3-540-45465-9_55\">10.1007/3-540-45465-9_55</a>.","ieee":"T. A. Henzinger, S. Krishnan, O. Kupferman, and F. Mang, “Synthesis of uninitialized systems,” in <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>, Malaga, Spain, 2002, vol. 2380, pp. 644–656.","ista":"Henzinger TA, Krishnan S, Kupferman O, Mang F. 2002. Synthesis of uninitialized systems. Proceedings of the 29th International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2380, 644–656.","chicago":"Henzinger, Thomas A, Sriram Krishnan, Orna Kupferman, and Freddy Mang. “Synthesis of Uninitialized Systems.” In <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>, 2380:644–56. Springer, 2002. <a href=\"https://doi.org/10.1007/3-540-45465-9_55\">https://doi.org/10.1007/3-540-45465-9_55</a>.","apa":"Henzinger, T. A., Krishnan, S., Kupferman, O., &#38; Mang, F. (2002). Synthesis of uninitialized systems. In <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i> (Vol. 2380, pp. 644–656). Malaga, Spain: Springer. <a href=\"https://doi.org/10.1007/3-540-45465-9_55\">https://doi.org/10.1007/3-540-45465-9_55</a>","ama":"Henzinger TA, Krishnan S, Kupferman O, Mang F. Synthesis of uninitialized systems. In: <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>. Vol 2380. Springer; 2002:644-656. doi:<a href=\"https://doi.org/10.1007/3-540-45465-9_55\">10.1007/3-540-45465-9_55</a>","short":"T.A. Henzinger, S. Krishnan, O. Kupferman, F. Mang, in:, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, Springer, 2002, pp. 644–656."},"author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Krishnan","first_name":"Sriram","full_name":"Krishnan, Sriram"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"},{"full_name":"Mang, Freddy","first_name":"Freddy","last_name":"Mang"}],"type":"conference","alternative_title":["LNCS"],"day":"26","publication_status":"published","volume":2380,"article_processing_charge":"No","abstract":[{"lang":"eng","text":"The sequential synthesis problem, which is closely related to Church’s solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. In this paper we solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Büchi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. We also study the problem of deciding whether a given specification is uninitialized, that is, if its uninitialized and initialized synthesis problems coincide. We show that this problem has, for each specification formalism, the same complexity as the equivalence problem."}],"_id":"4471","date_published":"2002-06-26T00:00:00Z","publication_identifier":{"isbn":["9783540438649"]},"scopus_import":"1","date_updated":"2023-06-05T08:05:13Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","year":"2002","publist_id":"257"},{"article_processing_charge":"No","_id":"4472","date_published":"2002-06-19T00:00:00Z","abstract":[{"text":"We present a methodology and tool for verifying and certifying systems code. The verification is based on the lazy-abstraction paradigm for intertwining the following three logical steps: construct a predicate abstraction from the code, model check the abstraction, and automatically refine the abstraction based on counterexample analysis. The certification is based on the proof-carrying code paradigm. Lazy abstraction enables the automatic construction of small proof certificates. The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software verification Tool. We describe our experience applying Blast to Linux and Windows device drivers. Given the C code for a driver and for a temporal-safety monitor, Blast automatically generates an easily checkable correctness certificate if the driver satisfies the specification, and an error trace otherwise.","lang":"eng"}],"publication_status":"published","volume":2404,"year":"2002","oa_version":"None","publist_id":"258","publication_identifier":{"isbn":["9783540439974"]},"date_updated":"2023-06-05T08:11:32Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","page":"526 - 538","date_created":"2018-12-11T12:09:01Z","extern":"1","month":"06","publisher":"Springer","intvolume":"      2404","status":"public","quality_controlled":"1","publication":"Proceedings of the 14th International Conference on Computer Aided Verification","conference":{"location":"Copenhagen, Denmark","end_date":"2002-07-31","start_date":"2002-07-27","name":"CAV: Computer Aided Verification"},"title":"Temporal safety proofs for systems code","citation":{"ista":"Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. 2002. Temporal safety proofs for systems code. Proceedings of the 14th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 526–538.","ieee":"T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer, “Temporal safety proofs for systems code,” in <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>, Copenhagen, Denmark, 2002, vol. 2404, pp. 526–538.","chicago":"Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>, 2404:526–38. Springer, 2002. <a href=\"https://doi.org/10.1007/3-540-45657-0_45\">https://doi.org/10.1007/3-540-45657-0_45</a>.","mla":"Henzinger, Thomas A., et al. “Temporal Safety Proofs for Systems Code.” <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>, vol. 2404, Springer, 2002, pp. 526–38, doi:<a href=\"https://doi.org/10.1007/3-540-45657-0_45\">10.1007/3-540-45657-0_45</a>.","short":"T.A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, W. Weimer, in:, Proceedings of the 14th International Conference on Computer Aided Verification, Springer, 2002, pp. 526–538.","apa":"Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., &#38; Weimer, W. (2002). Temporal safety proofs for systems code. In <i>Proceedings of the 14th International Conference on Computer Aided Verification</i> (Vol. 2404, pp. 526–538). Copenhagen, Denmark: Springer. <a href=\"https://doi.org/10.1007/3-540-45657-0_45\">https://doi.org/10.1007/3-540-45657-0_45</a>","ama":"Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety proofs for systems code. In: <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>. Vol 2404. Springer; 2002:526-538. doi:<a href=\"https://doi.org/10.1007/3-540-45657-0_45\">10.1007/3-540-45657-0_45</a>"},"alternative_title":["LNCS"],"author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"George","full_name":"Necula, George","last_name":"Necula"},{"first_name":"Ranjit","full_name":"Jhala, Ranjit","last_name":"Jhala"},{"last_name":"Sutre","full_name":"Sutre, Grégoire","first_name":"Grégoire"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"},{"last_name":"Weimer","first_name":"Westley","full_name":"Weimer, Westley"}],"type":"conference","day":"19","acknowledgement":"This work was supported in part by the NSF ITR grants CCR-0085949, CCR-0081588, the NSF Career grant CCR-9875171, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, the SRC contract 99-TJ-683, a Microsoft fellowship, and gifts from AT&T Research and Microsoft Research.","doi":"10.1007/3-540-45657-0_45","language":[{"iso":"eng"}]},{"quality_controlled":"1","publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","intvolume":"        24","status":"public","publisher":"ACM","extern":"1","month":"01","date_created":"2018-12-11T12:09:02Z","page":"51 - 64","language":[{"iso":"eng"}],"doi":"10.1145/509705.509707","day":"01","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Qadeer","full_name":"Qadeer, Shaz","first_name":"Shaz"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"},{"last_name":"Tasiran","first_name":"Serdar","full_name":"Tasiran, Serdar"}],"type":"journal_article","citation":{"mla":"Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24, no. 1, ACM, 2002, pp. 51–64, doi:<a href=\"https://doi.org/10.1145/509705.509707\">10.1145/509705.509707</a>.","chicago":"Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM, 2002. <a href=\"https://doi.org/10.1145/509705.509707\">https://doi.org/10.1145/509705.509707</a>.","ieee":"T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee rule for checking simulation,” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24, no. 1. ACM, pp. 51–64, 2002.","ista":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems (TOPLAS). 24(1), 51–64.","ama":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for checking simulation. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. 2002;24(1):51-64. doi:<a href=\"https://doi.org/10.1145/509705.509707\">10.1145/509705.509707</a>","apa":"Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (2002). An assume-guarantee rule for checking simulation. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM. <a href=\"https://doi.org/10.1145/509705.509707\">https://doi.org/10.1145/509705.509707</a>","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming Languages and Systems (TOPLAS) 24 (2002) 51–64."},"title":"An assume-guarantee rule for checking simulation","volume":24,"publication_status":"published","date_published":"2002-01-01T00:00:00Z","_id":"4473","abstract":[{"text":"The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P ≤s Q, denoting &quot;P is simulated by Q,&quot; into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also extend our assume-guarantee rule to account for fairness constraints on transition systems.","lang":"eng"}],"issue":"1","article_processing_charge":"No","date_updated":"2023-06-05T07:59:47Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publication_identifier":{"issn":["0164-0925"]},"publist_id":"256","article_type":"original","oa_version":"None","year":"2002"},{"status":"public","intvolume":"       173","quality_controlled":"1","publication":"Information and Computation","publisher":"Elsevier","date_created":"2018-12-11T12:09:02Z","extern":"1","month":"02","page":"64 - 81","doi":"10.1006/inco.2001.3085","language":[{"iso":"eng"}],"acknowledgement":"We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers for their comments on this paper.","type":"journal_article","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Orna","full_name":"Kupferman, Orna","last_name":"Kupferman"},{"last_name":"Rajamani","full_name":"Rajamani, Sriram","first_name":"Sriram"}],"day":"25","title":"Fair simulation","citation":{"ista":"Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information and Computation. 173(1), 64–81.","ieee":"T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” <i>Information and Computation</i>, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.","chicago":"Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.” <i>Information and Computation</i>. Elsevier, 2002. <a href=\"https://doi.org/10.1006/inco.2001.3085\">https://doi.org/10.1006/inco.2001.3085</a>.","mla":"Henzinger, Thomas A., et al. “Fair Simulation.” <i>Information and Computation</i>, vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:<a href=\"https://doi.org/10.1006/inco.2001.3085\">10.1006/inco.2001.3085</a>.","short":"T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173 (2002) 64–81.","apa":"Henzinger, T. A., Kupferman, O., &#38; Rajamani, S. (2002). Fair simulation. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.2001.3085\">https://doi.org/10.1006/inco.2001.3085</a>","ama":"Henzinger TA, Kupferman O, Rajamani S. Fair simulation. <i>Information and Computation</i>. 2002;173(1):64-81. doi:<a href=\"https://doi.org/10.1006/inco.2001.3085\">10.1006/inco.2001.3085</a>"},"volume":173,"oa":1,"main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub","open_access":"1"}],"publication_status":"published","abstract":[{"lang":"eng","text":"The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems."}],"_id":"4474","date_published":"2002-02-25T00:00:00Z","issue":"1","article_processing_charge":"No","publication_identifier":{"issn":["0890-5401"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2023-06-05T07:53:27Z","scopus_import":"1","year":"2002","oa_version":"Published Version","publist_id":"255","article_type":"original"},{"publication_status":"published","publisher":"ACM","status":"public","quality_controlled":"1","publication":"Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","article_processing_charge":"No","page":"58 - 70","_id":"4476","abstract":[{"text":"One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.","lang":"eng"}],"date_published":"2002-01-01T00:00:00Z","date_created":"2018-12-11T12:09:03Z","extern":"1","month":"01","acknowledgement":"We thank Wes Weimer and Jeff Foster for many useful discussions. \r\n","doi":"10.1145/503272.503279","publication_identifier":{"isbn":["9781581134506"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","language":[{"iso":"eng"}],"date_updated":"2023-06-05T07:45:53Z","scopus_import":"1","conference":{"location":"Portland, OR, USA","end_date":"2002-01-18","start_date":"2002-01-16","name":"POPL: Principles of Programming Languages"},"title":"Lazy abstraction","citation":{"chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre. “Lazy Abstraction.” In <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, 58–70. ACM, 2002. <a href=\"https://doi.org/10.1145/503272.503279\">https://doi.org/10.1145/503272.503279</a>.","ista":"Henzinger TA, Jhala R, Majumdar R, Sutre G. 2002. Lazy abstraction. Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL: Principles of Programming Languages, 58–70.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy abstraction,” in <i>Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i>, Portland, OR, USA, 2002, pp. 58–70.","mla":"Henzinger, Thomas A., et al. “Lazy Abstraction.” <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, ACM, 2002, pp. 58–70, doi:<a href=\"https://doi.org/10.1145/503272.503279\">10.1145/503272.503279</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2002, pp. 58–70.","ama":"Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>. ACM; 2002:58-70. doi:<a href=\"https://doi.org/10.1145/503272.503279\">10.1145/503272.503279</a>","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sutre, G. (2002). Lazy abstraction. In <i>Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i> (pp. 58–70). Portland, OR, USA: ACM. <a href=\"https://doi.org/10.1145/503272.503279\">https://doi.org/10.1145/503272.503279</a>"},"year":"2002","oa_version":"None","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"},{"last_name":"Sutre","first_name":"Grégoire","full_name":"Sutre, Grégoire"}],"type":"conference","day":"01","publist_id":"254"}]