[{"quality_controlled":"1","page":"773 - 789","ddc":["000"],"date_updated":"2020-08-11T10:09:47Z","_id":"2447","type":"conference","series_title":"Lecture Notes in Computer Science","doi":"10.1007/978-3-642-39799-8_54","alternative_title":["LNCS"],"article_processing_charge":"No","publisher":"Springer","conference":{"location":"St. Petersburg, Russia","name":"CAV: Computer Aided Verification","start_date":"2013-07-13","end_date":"2013-07-19"},"date_published":"2013-07-01T00:00:00Z","status":"public","publist_id":"4456","year":"2013","publication_status":"published","file_date_updated":"2020-07-14T12:45:41Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"Separation logic (SL) has gained widespread popularity because of its ability to succinctly express complex invariants of a program’s heap configurations. Several specialized provers have been developed for decidable SL fragments. However, these provers cannot be easily extended or combined with solvers for other theories that are important in program verification, e.g., linear arithmetic. In this paper, we present a reduction of decidable SL fragments to a decidable first-order theory that fits well into the satisfiability modulo theories (SMT) framework. We show how to use this reduction to automate satisfiability, entailment, frame inference, and abduction problems for separation logic using SMT solvers. Our approach provides a simple method of integrating separation logic into existing verification tools that provide SMT backends, and an elegant way of combining SL fragments with other decidable first-order theories. We implemented this approach in a verification tool and applied it to heap-manipulating programs whose verification involves reasoning in theory combinations.\r\n"}],"intvolume":"      8044","volume":8044,"date_created":"2018-12-11T11:57:43Z","author":[{"full_name":"Piskac, Ruzica","last_name":"Piskac","first_name":"Ruzica"},{"full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas"},{"orcid":"0000-0002-3197-8736","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","last_name":"Zufferey"}],"day":"01","scopus_import":1,"title":"Automating separation logic using SMT","oa_version":"Submitted Version","citation":{"ama":"Piskac R, Wies T, Zufferey D. Automating separation logic using SMT. 2013;8044:773-789. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">10.1007/978-3-642-39799-8_54</a>","short":"R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789.","ieee":"R. Piskac, T. Wies, and D. Zufferey, “Automating separation logic using SMT,” vol. 8044. Springer, pp. 773–789, 2013.","chicago":"Piskac, Ruzica, Thomas Wies, and Damien Zufferey. “Automating Separation Logic Using SMT.” Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">https://doi.org/10.1007/978-3-642-39799-8_54</a>.","ista":"Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT. 8044, 773–789.","mla":"Piskac, Ruzica, et al. <i>Automating Separation Logic Using SMT</i>. Vol. 8044, Springer, 2013, pp. 773–89, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">10.1007/978-3-642-39799-8_54</a>.","apa":"Piskac, R., Wies, T., &#38; Zufferey, D. (2013). Automating separation logic using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">https://doi.org/10.1007/978-3-642-39799-8_54</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"file":[{"checksum":"2e866932ab688f47ecd504acb4d5c7d4","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"2013_CAV_Piskac.pdf","file_id":"7859","date_updated":"2020-07-14T12:45:41Z","creator":"dernst","file_size":309182,"date_created":"2020-05-15T11:13:01Z"}],"month":"07"},{"main_file_link":[{"url":"http://arise.or.at/pubpdf/Structural_Counter_Abstraction.pdf","open_access":"1"}],"quality_controlled":"1","page":"62 - 77","_id":"2847","date_updated":"2023-09-07T11:36:36Z","series_title":"Lecture Notes in Computer Science","type":"conference","alternative_title":["LNCS"],"doi":"10.1007/978-3-642-36742-7_5","publisher":"Springer","editor":[{"full_name":"Piterman, Nir","last_name":"Piterman","first_name":"Nir"},{"first_name":"Scott","last_name":"Smolka","full_name":"Smolka, Scott"}],"ec_funded":1,"conference":{"start_date":"2013-03-16","end_date":"2013-03-24","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Rome, Italy"},"date_published":"2013-03-01T00:00:00Z","status":"public","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"publist_id":"3947","year":"2013","related_material":{"record":[{"id":"1405","relation":"dissertation_contains","status":"public"}]},"publication_status":"published","intvolume":"      7795","abstract":[{"lang":"eng","text":"Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions."}],"volume":7795,"date_created":"2018-12-11T11:59:54Z","day":"01","scopus_import":1,"author":[{"first_name":"Kshitij","full_name":"Bansal, Kshitij","last_name":"Bansal"},{"full_name":"Koskinen, Eric","last_name":"Koskinen","first_name":"Eric"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","first_name":"Thomas"},{"orcid":"0000-0002-3197-8736","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","last_name":"Zufferey"}],"title":"Structural Counter Abstraction","oa_version":"Submitted Version","citation":{"ieee":"K. Bansal, E. Koskinen, T. Wies, and D. Zufferey, “Structural Counter Abstraction,” vol. 7795. Springer, pp. 62–77, 2013.","short":"K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.","ama":"Bansal K, Koskinen E, Wies T, Zufferey D. Structural Counter Abstraction. Piterman N, Smolka S, eds. 2013;7795:62-77. doi:<a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">10.1007/978-3-642-36742-7_5</a>","apa":"Bansal, K., Koskinen, E., Wies, T., &#38; Zufferey, D. (2013). Structural Counter Abstraction. (N. Piterman &#38; S. Smolka, Eds.). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">https://doi.org/10.1007/978-3-642-36742-7_5</a>","mla":"Bansal, Kshitij, et al. <i>Structural Counter Abstraction</i>. Edited by Nir Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:<a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">10.1007/978-3-642-36742-7_5</a>.","ista":"Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman &#38; S. Smolka). 7795, 62–77.","chicago":"Bansal, Kshitij, Eric Koskinen, Thomas Wies, and Damien Zufferey. “Structural Counter Abstraction.” Edited by Nir Piterman and Scott Smolka. Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">https://doi.org/10.1007/978-3-642-36742-7_5</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"month":"03"},{"quality_controlled":"1","page":"445 - 460","ddc":["000","005"],"_id":"3251","date_updated":"2023-09-07T11:36:36Z","type":"conference","alternative_title":["LNCS"],"doi":"10.1007/978-3-642-27940-9_29","publisher":"Springer","ec_funded":1,"conference":{"location":"Philadelphia, PA, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","start_date":"2012-01-22","end_date":"2012-01-24"},"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.","date_published":"2012-01-01T00:00:00Z","status":"public","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"publist_id":"3406","year":"2012","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1405"}]},"file_date_updated":"2020-07-14T12:46:05Z","publication_status":"published","has_accepted_license":"1","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"}],"volume":7148,"date_created":"2018-12-11T12:02:16Z","day":"01","author":[{"first_name":"Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"}],"title":"Ideal abstractions for well structured transition systems","oa_version":"Submitted Version","citation":{"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>.","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>","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>.","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.","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.","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>"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa":1,"pubrep_id":"100","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"file":[{"relation":"main_file","checksum":"f2f0d55efa32309ad1fe65a5fcaad90c","file_name":"IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf","content_type":"application/pdf","access_level":"open_access","file_id":"4759","file_size":217104,"date_created":"2018-12-12T10:09:35Z","creator":"system","date_updated":"2020-07-14T12:46:05Z"}],"month":"01"},{"type":"conference","date_created":"2018-12-11T12:02:33Z","date_updated":"2021-01-12T07:42:31Z","_id":"3302","title":"Static scheduling in clouds","publisher":"USENIX","oa_version":"Submitted Version","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Singh","id":"72A86902-E99F-11E9-9F62-915534D1B916","full_name":"Singh, Anmol","first_name":"Anmol"},{"first_name":"Vasu","full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"},{"first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies"},{"first_name":"Damien","orcid":"0000-0002-3197-8736","full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"}],"day":"14","publication_status":"published","quality_controlled":"1","file_date_updated":"2020-07-14T12:46:06Z","abstract":[{"lang":"eng","text":"Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We present a new job execution environment Flextic that exploits scal- able static scheduling techniques to provide the user with a flexible pricing model, such as a tradeoff between dif- ferent degrees of execution speed and execution price, and at the same time, reduce scheduling overhead for the cloud provider. We have evaluated a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various data parallel jobs from machine learning, im- age processing, and gene sequencing that we considered, Flextic has low scheduling overhead and reduces job du- ration by up to 15% compared to Hadoop, a dynamic cloud scheduler."}],"ddc":["000","005"],"page":"1 - 6","has_accepted_license":"1","publist_id":"3338","file":[{"date_updated":"2020-07-14T12:46:06Z","creator":"system","date_created":"2018-12-12T10:18:14Z","file_size":232770,"file_id":"5333","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf","checksum":"21a461ac004bb535c83320fe79b30375","relation":"main_file"}],"department":[{"_id":"ToHe"}],"month":"06","year":"2011","conference":{"end_date":"2011-06-15","start_date":"2011-06-14","name":"HotCloud: Workshop on Hot Topics in Cloud Computing"},"date_published":"2011-06-14T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.","ieee":"T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling in clouds,” presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, 2011, pp. 1–6.","short":"T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6.","ista":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.","chicago":"Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds,” 1–6. USENIX, 2011.","apa":"Henzinger, T. A., Singh, A., Singh, V., Wies, T., &#38; Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.","mla":"Henzinger, Thomas A., et al. <i>Static Scheduling in Clouds</i>. USENIX, 2011, pp. 1–6."},"language":[{"iso":"eng"}],"pubrep_id":"90","status":"public","oa":1},{"quality_controlled":"1","publication_status":"published","abstract":[{"text":"We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures.","lang":"eng"}],"intvolume":"      6803","page":"476 - 491","date_created":"2018-12-11T12:02:40Z","type":"conference","volume":6803,"_id":"3323","date_updated":"2023-02-23T12:23:48Z","publisher":"Springer","oa_version":"None","title":"An efficient decision procedure for imperative tree data structures","scopus_import":1,"alternative_title":["LNAI "],"day":"19","doi":"10.1007/978-3-642-22438-6_36","author":[{"first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies"},{"full_name":"Muñiz, Marco","last_name":"Muñiz","first_name":"Marco"},{"last_name":"Kuncak","full_name":"Kuncak, Viktor","first_name":"Viktor"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Wrocław, Poland","end_date":"2011-08-05","start_date":"2011-07-31","name":"CADE 23: Automated Deduction "},"date_published":"2011-07-19T00:00:00Z","citation":{"short":"T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.","ieee":"T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław, Poland, 2011, vol. 6803, pp. 476–491.","ama":"Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:<a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">10.1007/978-3-642-22438-6_36</a>","mla":"Wies, Thomas, et al. <i>An Efficient Decision Procedure for Imperative Tree Data Structures</i>. Vol. 6803, Springer, 2011, pp. 476–91, doi:<a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">10.1007/978-3-642-22438-6_36</a>.","apa":"Wies, T., Muñiz, M., &#38; Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. <a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">https://doi.org/10.1007/978-3-642-22438-6_36</a>","chicago":"Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">https://doi.org/10.1007/978-3-642-22438-6_36</a>.","ista":"Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491."},"status":"public","language":[{"iso":"eng"}],"publist_id":"3312","department":[{"_id":"ToHe"}],"month":"07","related_material":{"record":[{"id":"5383","relation":"earlier_version","status":"public"}]},"year":"2011"},{"page":"371 - 386","quality_controlled":"1","main_file_link":[{"url":"https://infoscience.epfl.ch/record/170697/","open_access":"1"}],"publisher":"Springer","editor":[{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"full_name":"Schmidt, David","last_name":"Schmidt","first_name":"David"}],"alternative_title":["LNCS"],"doi":"10.1007/978-3-642-18275-4_26","type":"conference","_id":"3324","date_updated":"2021-01-12T07:42:39Z","status":"public","conference":{"start_date":"2011-01-23","end_date":"2011-01-25","name":"VMCAI: Verification Model Checking and Abstract Interpretation","location":"Texas, USA"},"date_published":"2011-01-01T00:00:00Z","year":"2011","publist_id":"3311","intvolume":"      6538","abstract":[{"lang":"eng","text":"Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs."}],"publication_status":"published","title":"Decision procedures for automating termination proofs","oa_version":"Submitted Version","day":"01","scopus_import":1,"author":[{"last_name":"Piskac","full_name":"Piskac, Ruzica","first_name":"Ruzica"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas"}],"date_created":"2018-12-11T12:02:40Z","volume":6538,"language":[{"iso":"eng"}],"oa":1,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Piskac, R., &#38; Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala &#38; D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">https://doi.org/10.1007/978-3-642-18275-4_26</a>","mla":"Piskac, Ruzica, and Thomas Wies. <i>Decision Procedures for Automating Termination Proofs</i>. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:<a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">10.1007/978-3-642-18275-4_26</a>.","ista":"Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.","chicago":"Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">https://doi.org/10.1007/978-3-642-18275-4_26</a>.","ieee":"R. Piskac and T. Wies, “Decision procedures for automating termination proofs,” presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA, 2011, vol. 6538, pp. 371–386.","short":"R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386.","ama":"Piskac R, Wies T. Decision procedures for automating termination proofs. In: Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:<a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">10.1007/978-3-642-18275-4_26</a>"},"month":"01","department":[{"_id":"ToHe"}]},{"year":"2011","related_material":{"record":[{"id":"3323","status":"public","relation":"later_version"}]},"month":"04","department":[{"_id":"ToHe"}],"file":[{"file_id":"5462","file_size":619053,"date_created":"2018-12-12T11:53:01Z","creator":"system","date_updated":"2020-07-14T12:46:40Z","relation":"main_file","checksum":"b20029184c4a819c5f4466a4a3d238b5","file_name":"IST-2011-0005_IST-2011-0005.pdf","content_type":"application/pdf","access_level":"open_access"}],"oa":1,"status":"public","pubrep_id":"19","language":[{"iso":"eng"}],"citation":{"chicago":"Wies, Thomas, Marco Muñiz, and Viktor Kuncak. <i>On an Efficient Decision Procedure for Imperative Tree Data Structures</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0005\">https://doi.org/10.15479/AT:IST-2011-0005</a>.","ista":"Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative tree data structures, IST Austria, 25p.","apa":"Wies, T., Muñiz, M., &#38; Kuncak, V. (2011). <i>On an efficient decision procedure for imperative tree data structures</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0005\">https://doi.org/10.15479/AT:IST-2011-0005</a>","mla":"Wies, Thomas, et al. <i>On an Efficient Decision Procedure for Imperative Tree Data Structures</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0005\">10.15479/AT:IST-2011-0005</a>.","ama":"Wies T, Muñiz M, Kuncak V. <i>On an Efficient Decision Procedure for Imperative Tree Data Structures</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0005\">10.15479/AT:IST-2011-0005</a>","ieee":"T. Wies, M. Muñiz, and V. Kuncak, <i>On an efficient decision procedure for imperative tree data structures</i>. IST Austria, 2011.","short":"T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative Tree Data Structures, IST Austria, 2011."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2011-04-26T00:00:00Z","alternative_title":["IST Austria Technical Report"],"day":"26","author":[{"last_name":"Wies","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas"},{"first_name":"Marco","last_name":"Muñiz","full_name":"Muñiz, Marco"},{"first_name":"Viktor","last_name":"Kuncak","full_name":"Kuncak, Viktor"}],"doi":"10.15479/AT:IST-2011-0005","title":"On an efficient decision procedure for imperative tree data structures","oa_version":"Published Version","publisher":"IST Austria","_id":"5383","date_updated":"2023-02-23T11:22:16Z","date_created":"2018-12-12T11:39:01Z","type":"technical_report","has_accepted_license":"1","page":"25","ddc":["000","006"],"abstract":[{"lang":"eng","text":"We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures."}],"file_date_updated":"2020-07-14T12:46:40Z","publication_status":"published","publication_identifier":{"issn":["2664-1690"]}},{"_id":"3358","date_updated":"2021-01-12T07:42:55Z","date_created":"2018-12-11T12:02:53Z","type":"conference","scopus_import":1,"article_processing_charge":"No","day":"10","doi":"10.1145/1966445.1966476","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu","last_name":"Singh"},{"first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","first_name":"Damien"}],"title":"Scheduling large jobs by abstraction refinement","publisher":"ACM","oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"http://cs.nyu.edu/wies/publ/scheduling_large_jobs_by_abstraction_refinement.pdf"}],"quality_controlled":"1","publication_status":"published","page":"329 - 342","abstract":[{"lang":"eng","text":"The static scheduling problem often arises as a fundamental problem in real-time systems and grid computing. We consider the problem of statically scheduling a large job expressed as a task graph on a large number of computing nodes, such as a data center. This paper solves the large-scale static scheduling problem using abstraction refinement, a technique commonly used in formal verification to efficiently solve computationally hard problems. A scheduler based on abstraction refinement first attempts to solve the scheduling problem with abstract representations of the job and the computing resources. As abstract representations are generally small, the scheduling can be done reasonably fast. If the obtained schedule does not meet specified quality conditions (like data center utilization or schedule makespan) then the scheduler refines the job and data center abstractions and, again solves the scheduling problem. We develop different schedulers based on abstraction refinement. We implemented these schedulers and used them to schedule task graphs from various computing domains on simulated data centers with realistic topologies. We compared the speed of scheduling and the quality of the produced schedules with our abstraction refinement schedulers against a baseline scheduler that does not use any abstraction. We conclude that abstraction refinement techniques give a significant speed-up compared to traditional static scheduling heuristics, at a reasonable cost in the quality of the produced schedules. We further used our static schedulers in an actual system that we deployed on Amazon EC2 and compared it against the Hadoop dynamic scheduler for large MapReduce jobs. Our experiments indicate that there is great potential for static scheduling techniques."}],"department":[{"_id":"ToHe"}],"publist_id":"3257","year":"2011","month":"04","citation":{"mla":"Henzinger, Thomas A., et al. <i>Scheduling Large Jobs by Abstraction Refinement</i>. ACM, 2011, pp. 329–42, doi:<a href=\"https://doi.org/10.1145/1966445.1966476\">10.1145/1966445.1966476</a>.","apa":"Henzinger, T. A., Singh, V., Wies, T., &#38; Zufferey, D. (2011). Scheduling large jobs by abstraction refinement (pp. 329–342). Presented at the EuroSys, Salzburg, Austria: ACM. <a href=\"https://doi.org/10.1145/1966445.1966476\">https://doi.org/10.1145/1966445.1966476</a>","ista":"Henzinger TA, Singh V, Wies T, Zufferey D. 2011. Scheduling large jobs by abstraction refinement. EuroSys, 329–342.","chicago":"Henzinger, Thomas A, Vasu Singh, Thomas Wies, and Damien Zufferey. “Scheduling Large Jobs by Abstraction Refinement,” 329–42. ACM, 2011. <a href=\"https://doi.org/10.1145/1966445.1966476\">https://doi.org/10.1145/1966445.1966476</a>.","short":"T.A. Henzinger, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2011, pp. 329–342.","ieee":"T. A. Henzinger, V. Singh, T. Wies, and D. Zufferey, “Scheduling large jobs by abstraction refinement,” presented at the EuroSys, Salzburg, Austria, 2011, pp. 329–342.","ama":"Henzinger TA, Singh V, Wies T, Zufferey D. Scheduling large jobs by abstraction refinement. In: ACM; 2011:329-342. doi:<a href=\"https://doi.org/10.1145/1966445.1966476\">10.1145/1966445.1966476</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Salzburg, Austria","start_date":"2011-04-10","end_date":"2011-04-13","name":"EuroSys"},"date_published":"2011-04-10T00:00:00Z","oa":1,"language":[{"iso":"eng"}],"status":"public"},{"year":"2010","month":"12","department":[{"_id":"ToHe"}],"publist_id":"7284","status":"public","publication":"Formal Methods in System Design","language":[{"iso":"eng"}],"citation":{"ista":"Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. 2010. Doomed program points. Formal Methods in System Design. 37(2–3), 171–199.","chicago":"Hoenicke, Jochen, Kari Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. “Doomed Program Points.” <i>Formal Methods in System Design</i>. Springer, 2010. <a href=\"https://doi.org/10.1007/s10703-010-0102-0\">https://doi.org/10.1007/s10703-010-0102-0</a>.","mla":"Hoenicke, Jochen, et al. “Doomed Program Points.” <i>Formal Methods in System Design</i>, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:<a href=\"https://doi.org/10.1007/s10703-010-0102-0\">10.1007/s10703-010-0102-0</a>.","apa":"Hoenicke, J., Leino, K., Podelski, A., Schäf, M., &#38; Wies, T. (2010). Doomed program points. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-010-0102-0\">https://doi.org/10.1007/s10703-010-0102-0</a>","ama":"Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. Doomed program points. <i>Formal Methods in System Design</i>. 2010;37(2-3):171-199. doi:<a href=\"https://doi.org/10.1007/s10703-010-0102-0\">10.1007/s10703-010-0102-0</a>","short":"J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in System Design 37 (2010) 171–199.","ieee":"J. Hoenicke, K. Leino, A. Podelski, M. Schäf, and T. Wies, “Doomed program points,” <i>Formal Methods in System Design</i>, vol. 37, no. 2–3. Springer, pp. 171–199, 2010."},"issue":"2-3","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_published":"2010-12-01T00:00:00Z","day":"01","scopus_import":1,"author":[{"first_name":"Jochen","full_name":"Hoenicke, Jochen","last_name":"Hoenicke"},{"first_name":"Kari","full_name":"Leino, Kari","last_name":"Leino"},{"last_name":"Podelski","full_name":"Podelski, Andreas","first_name":"Andreas"},{"last_name":"Schäf","full_name":"Schäf, Martin","first_name":"Martin"},{"last_name":"Wies","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas"}],"doi":"10.1007/s10703-010-0102-0","oa_version":"None","publisher":"Springer","title":"Doomed program points","_id":"533","volume":37,"date_updated":"2021-01-12T08:01:28Z","date_created":"2018-12-11T11:47:01Z","type":"journal_article","page":"171 - 199","abstract":[{"lang":"eng","text":"Any programming error that can be revealed before compiling a program saves precious time for the programmer. While integrated development environments already do a good job by detecting, e.g., data-flow abnormalities, current static analysis tools suffer from false positives (&quot;noise&quot;) or require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if its execution will inevitably fail, regardless of which state it is started in. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on experiments with a prototype tool."}],"intvolume":"        37","quality_controlled":"1","publication_status":"published"},{"quality_controlled":"1","ddc":["004"],"page":"94 - 108","type":"conference","_id":"4361","date_updated":"2023-09-07T11:36:36Z","publisher":"Springer","editor":[{"first_name":"Luke","last_name":"Ong","full_name":"Ong, Luke"}],"alternative_title":["LNCS"],"doi":"10.1007/978-3-642-12032-9_8","date_published":"2010-03-01T00:00:00Z","conference":{"start_date":"2010-03-20","end_date":"2010-03-28","name":"FoSSaCS: Foundations of Software Science and Computation Structures","location":"Paphos, Cyprus"},"status":"public","publist_id":"1099","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1405"}]},"year":"2010","file_date_updated":"2020-07-14T12:46:27Z","publication_status":"published","intvolume":"      6014","abstract":[{"lang":"eng","text":"Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems."}],"has_accepted_license":"1","date_created":"2018-12-11T12:08:27Z","volume":6014,"title":"Forward analysis of depth-bounded processes","oa_version":"Submitted Version","scopus_import":1,"day":"01","author":[{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas"},{"orcid":"0000-0002-3197-8736","first_name":"Damien","full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Wies T, Zufferey D, Henzinger TA. Forward analysis of depth-bounded processes. In: Ong L, ed. Vol 6014. Springer; 2010:94-108. doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>","short":"T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108.","ieee":"T. Wies, D. Zufferey, and T. A. Henzinger, “Forward analysis of depth-bounded processes,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus, 2010, vol. 6014, pp. 94–108.","chicago":"Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>.","ista":"Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded processes. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6014, 94–108.","mla":"Wies, Thomas, et al. <i>Forward Analysis of Depth-Bounded Processes</i>. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>.","apa":"Wies, T., Zufferey, D., &#38; Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>"},"pubrep_id":"50","language":[{"iso":"eng"}],"oa":1,"file":[{"creator":"system","date_updated":"2020-07-14T12:46:27Z","date_created":"2018-12-12T10:08:17Z","file_size":240766,"file_id":"4677","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf","checksum":"3e610de84937d821316362658239134a","relation":"main_file"}],"department":[{"_id":"ToHe"}],"month":"03"},{"status":"public","extern":1,"date_published":"2010-01-01T00:00:00Z","conference":{"name":"POPL: Principles of Programming Languages"},"citation":{"mla":"Podelski, Andreas, and Thomas Wies. <i>Counterexample-Guided Focus</i>. ACM, 2010, pp. 249–60, doi:<a href=\"https://doi.org/10.1145/1707801.1706330\">10.1145/1707801.1706330</a>.","apa":"Podelski, A., &#38; Wies, T. (2010). Counterexample-guided focus (pp. 249–260). Presented at the POPL: Principles of Programming Languages, ACM. <a href=\"https://doi.org/10.1145/1707801.1706330\">https://doi.org/10.1145/1707801.1706330</a>","chicago":"Podelski, Andreas, and Thomas Wies. “Counterexample-Guided Focus,” 249–60. ACM, 2010. <a href=\"https://doi.org/10.1145/1707801.1706330\">https://doi.org/10.1145/1707801.1706330</a>.","ista":"Podelski A, Wies T. 2010. Counterexample-guided focus. POPL: Principles of Programming Languages, 249–260.","short":"A. Podelski, T. Wies, in:, ACM, 2010, pp. 249–260.","ieee":"A. Podelski and T. Wies, “Counterexample-guided focus,” presented at the POPL: Principles of Programming Languages, 2010, pp. 249–260.","ama":"Podelski A, Wies T. Counterexample-guided focus. In: ACM; 2010:249-260. doi:<a href=\"https://doi.org/10.1145/1707801.1706330\">10.1145/1707801.1706330</a>"},"month":"01","year":"2010","publist_id":"1093","page":"249 - 260","quality_controlled":0,"publication_status":"published","publisher":"ACM","title":"Counterexample-guided focus","doi":"10.1145/1707801.1706330","author":[{"first_name":"Andreas","last_name":"Podelski","full_name":"Podelski,Andreas"},{"first_name":"Thomas","last_name":"Wies","full_name":"Thomas Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"}],"day":"01","type":"conference","date_created":"2018-12-11T12:08:28Z","date_updated":"2021-01-12T07:56:26Z","_id":"4364"},{"scopus_import":1,"day":"01","author":[{"first_name":"Viktor","last_name":"Kuncak","full_name":"Kuncak, Viktor"},{"first_name":"Ruzica","full_name":"Piskac, Ruzica","last_name":"Piskac"},{"last_name":"Suter","full_name":"Suter, Philippe","first_name":"Philippe"},{"first_name":"Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas"}],"oa_version":"Submitted Version","title":"Building a calculus of data structures","volume":5944,"date_created":"2018-12-11T12:08:33Z","abstract":[{"lang":"eng","text":"Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets, multisets, algebraic data types, or graphs. Consequently, formulas generated from verification also involve such data structures. To automate the proofs of such formulas we propose a logic (a “calculus”) of such data structures. We build the calculus by starting from decidable logics of individual data structures, and connecting them through functions and sets, in ways that go beyond the frameworks such as Nelson-Oppen. The result are new decidable logics that can simultaneously specify properties of different kinds of data structures and overcome the limitations of the individual logics. Several of our decidable logics include abstraction functions that map a data structure into its more abstract view (a tree into a multiset, a multiset into a set), into a numerical quantity (the size or the height), or into the truth value of a candidate data structure invariant (sortedness, or the heap property). For algebraic data types, we identify an asymptotic many-to-one condition on the abstraction function that guarantees the existence of a decision procedure. In addition to the combination based on abstraction functions, we can combine multiple data structure theories if they all reduce to the same data structure logic. As an instance of this approach, we describe a decidable logic whose formulas are propositional combinations of formulas in: weak monadic second-order logic of two successors, two-variable logic with counting, multiset algebra with Presburger arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the logic of algebraic data types with the set content function. The subformulas in this combination can share common variables that refer to sets of objects along with the common set algebra operations. Such sound and complete combination is possible because the relations on sets definable in the component logics are all expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic and its new extensions play an important role in our decidability results. In several cases, when we combine logics that belong to NP, we can prove the satisfiability for the combined logic is still in NP."}],"intvolume":"      5944","publication_status":"published","month":"01","department":[{"_id":"ToHe"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"ista":"Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944, 26–44.","chicago":"Kuncak, Viktor, Ruzica Piskac, Philippe Suter, and Thomas Wies. “Building a Calculus of Data Structures.” edited by Gilles Barthe and Manuel Hermenegildo, 5944:26–44. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">https://doi.org/10.1007/978-3-642-11319-2_6</a>.","apa":"Kuncak, V., Piskac, R., Suter, P., &#38; Wies, T. (2010). Building a calculus of data structures. In G. Barthe &#38; M. Hermenegildo (Eds.) (Vol. 5944, pp. 26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">https://doi.org/10.1007/978-3-642-11319-2_6</a>","mla":"Kuncak, Viktor, et al. <i>Building a Calculus of Data Structures</i>. Edited by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44, doi:<a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">10.1007/978-3-642-11319-2_6</a>.","ama":"Kuncak V, Piskac R, Suter P, Wies T. Building a calculus of data structures. In: Barthe G, Hermenegildo M, eds. Vol 5944. Springer; 2010:26-44. doi:<a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">10.1007/978-3-642-11319-2_6</a>","ieee":"V. Kuncak, R. Piskac, P. Suter, and T. Wies, “Building a calculus of data structures,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain, 2010, vol. 5944, pp. 26–44.","short":"V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo (Eds.), Springer, 2010, pp. 26–44."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"doi":"10.1007/978-3-642-11319-2_6","publisher":"Springer","editor":[{"full_name":"Barthe, Gilles","last_name":"Barthe","first_name":"Gilles"},{"full_name":"Hermenegildo, Manuel","last_name":"Hermenegildo","first_name":"Manuel"}],"_id":"4378","date_updated":"2021-01-12T07:56:31Z","type":"conference","page":"26 - 44","main_file_link":[{"open_access":"1","url":"https://infoscience.epfl.ch/record/161290/"}],"quality_controlled":"1","year":"2010","publist_id":"1081","status":"public","date_published":"2010-01-01T00:00:00Z","conference":{"end_date":"2010-01-19","start_date":"2010-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","location":"Madrid, Spain"}},{"citation":{"chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “A Marketplace for Cloud Resources,” 1–8. ACM, 2010. <a href=\"https://doi.org/10.1145/1879021.1879022\">https://doi.org/10.1145/1879021.1879022</a>.","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. <a href=\"https://doi.org/10.1145/1879021.1879022\">https://doi.org/10.1145/1879021.1879022</a>","mla":"Henzinger, Thomas A., et al. <i>A Marketplace for Cloud Resources</i>. ACM, 2010, pp. 1–8, doi:<a href=\"https://doi.org/10.1145/1879021.1879022\">10.1145/1879021.1879022</a>.","ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud resources. In: ACM; 2010:1-8. doi:<a href=\"https://doi.org/10.1145/1879021.1879022\">10.1145/1879021.1879022</a>","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA, 2010, pp. 1–8.","short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"pubrep_id":"48","department":[{"_id":"ToHe"}],"file":[{"access_level":"open_access","content_type":"application/pdf","file_name":"IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf","checksum":"7680dd24016810710f7c977bc94f85e9","relation":"main_file","creator":"system","date_updated":"2020-07-14T12:46:28Z","date_created":"2018-12-12T10:09:42Z","file_size":222626,"file_id":"4767"}],"month":"10","publication_status":"published","file_date_updated":"2020-07-14T12:46:28Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context."}],"date_created":"2018-12-11T12:08:33Z","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87","full_name":"Tomar, Anmol","last_name":"Tomar","first_name":"Anmol"},{"first_name":"Vasu","last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu"},{"first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies"},{"last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","first_name":"Damien","orcid":"0000-0002-3197-8736"}],"day":"24","scopus_import":1,"oa_version":"Submitted Version","title":"A marketplace for cloud resources","date_published":"2010-10-24T00:00:00Z","conference":{"location":"Arizona, USA","start_date":"2010-10-24","end_date":"2010-10-29","name":"EMSOFT: Embedded Software "},"status":"public","publist_id":"1078","year":"2010","quality_controlled":"1","page":"1 - 8","ddc":["005"],"date_updated":"2021-01-12T07:56:32Z","_id":"4380","type":"conference","doi":"10.1145/1879021.1879022","publisher":"ACM"},{"quality_controlled":"1","ddc":["004"],"page":"83 - 90","type":"conference","date_updated":"2021-01-12T07:56:33Z","_id":"4381","publisher":"IEEE","doi":"10.1109/CLOUD.2010.71","article_processing_charge":"No","date_published":"2010-08-26T00:00:00Z","conference":{"location":"Miami, USA","name":"CLOUD: Cloud Computing","start_date":"2010-07-05","end_date":"2010-07-10"},"status":"public","publist_id":"1077","year":"2010","publication_status":"published","file_date_updated":"2020-07-14T12:46:28Z","abstract":[{"lang":"eng","text":"Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases."}],"has_accepted_license":"1","date_created":"2018-12-11T12:08:33Z","title":"FlexPRICE: Flexible provisioning of resources in a cloud environment","oa_version":"Submitted Version","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Anmol","id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87","full_name":"Tomar, Anmol","last_name":"Tomar"},{"first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu","last_name":"Singh"},{"first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","first_name":"Damien"}],"day":"26","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Henzinger, Thomas A., et al. <i>FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment</i>. IEEE, 2010, pp. 83–90, doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>","chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,” 83–90. IEEE, 2010. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>.","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.","short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90.","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE: Flexible provisioning of resources in a cloud environment,” presented at the CLOUD: Cloud Computing, Miami, USA, 2010, pp. 83–90.","ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning of resources in a cloud environment. In: IEEE; 2010:83-90. doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>"},"pubrep_id":"47","language":[{"iso":"eng"}],"oa":1,"file":[{"file_id":"5188","date_created":"2018-12-12T10:16:03Z","file_size":467436,"date_updated":"2020-07-14T12:46:28Z","creator":"system","relation":"main_file","checksum":"98e534675339a8e2beca08890d048145","file_name":"IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf","content_type":"application/pdf","access_level":"open_access"}],"department":[{"_id":"ToHe"}],"month":"08"},{"extern":1,"status":"public","date_published":"2009-01-01T00:00:00Z","conference":{"name":"FroCoS: Frontiers of Combining Systems"},"citation":{"ama":"Wies T, Piskac R, Kuncak V. Combining Theories with Shared Set Operations. In: Springer; 2009:366-382. doi:<a href=\"https://doi.org/1558\">1558</a>","ieee":"T. Wies, R. Piskac, and V. Kuncak, “Combining Theories with Shared Set Operations,” presented at the FroCoS: Frontiers of Combining Systems, 2009, pp. 366–382.","short":"T. Wies, R. Piskac, V. Kuncak, in:, Springer, 2009, pp. 366–382.","chicago":"Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with Shared Set Operations,” 366–82. Springer, 2009. <a href=\"https://doi.org/1558\">https://doi.org/1558</a>.","ista":"Wies T, Piskac R, Kuncak V. 2009. Combining Theories with Shared Set Operations. FroCoS: Frontiers of Combining Systems, LNCS 5749, , 366–382.","apa":"Wies, T., Piskac, R., &#38; Kuncak, V. (2009). Combining Theories with Shared Set Operations (pp. 366–382). Presented at the FroCoS: Frontiers of Combining Systems, Springer. <a href=\"https://doi.org/1558\">https://doi.org/1558</a>","mla":"Wies, Thomas, et al. <i>Combining Theories with Shared Set Operations</i>. Springer, 2009, pp. 366–82, doi:<a href=\"https://doi.org/1558\">1558</a>."},"month":"01","year":"2009","publist_id":"1098","page":"366 - 382","quality_controlled":0,"publication_status":"published","title":"Combining Theories with Shared Set Operations","publisher":"Springer","author":[{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","last_name":"Wies","first_name":"Thomas"},{"first_name":"Ruzica","last_name":"Piskac","full_name":"Piskac, Ruzica"},{"last_name":"Kuncak","full_name":"Kuncak, Viktor","first_name":"Viktor"}],"doi":"1558","alternative_title":["LNCS 5749"],"day":"01","type":"conference","date_created":"2018-12-11T12:08:27Z","date_updated":"2021-01-12T07:56:24Z","_id":"4360"},{"title":"Abstraction Refinement for Quantified Array Assertions","publisher":"Springer","author":[{"first_name":"Mohamed","full_name":"Seghir,Mohamed Nassim","last_name":"Seghir"},{"first_name":"Andreas","last_name":"Podelski","full_name":"Podelski,Andreas"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","first_name":"Thomas"}],"doi":"1556","alternative_title":["LNCS 5673"],"day":"01","type":"conference","date_created":"2018-12-11T12:08:29Z","date_updated":"2021-01-12T07:56:26Z","_id":"4365","page":"3 - 18","publication_status":"published","quality_controlled":0,"month":"01","year":"2009","publist_id":"1094","extern":1,"status":"public","date_published":"2009-01-01T00:00:00Z","conference":{"name":"SAS: Static Analysis Symposium"},"citation":{"apa":"Seghir, M., Podelski, A., &#38; Wies, T. (2009). Abstraction Refinement for Quantified Array Assertions (pp. 3–18). Presented at the SAS: Static Analysis Symposium, Springer. <a href=\"https://doi.org/1556\">https://doi.org/1556</a>","mla":"Seghir, Mohamed, et al. <i>Abstraction Refinement for Quantified Array Assertions</i>. Springer, 2009, pp. 3–18, doi:<a href=\"https://doi.org/1556\">1556</a>.","chicago":"Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement for Quantified Array Assertions,” 3–18. Springer, 2009. <a href=\"https://doi.org/1556\">https://doi.org/1556</a>.","ista":"Seghir M, Podelski A, Wies T. 2009. Abstraction Refinement for Quantified Array Assertions. SAS: Static Analysis Symposium, LNCS 5673, , 3–18.","ieee":"M. Seghir, A. Podelski, and T. Wies, “Abstraction Refinement for Quantified Array Assertions,” presented at the SAS: Static Analysis Symposium, 2009, pp. 3–18.","short":"M. Seghir, A. Podelski, T. Wies, in:, Springer, 2009, pp. 3–18.","ama":"Seghir M, Podelski A, Wies T. Abstraction Refinement for Quantified Array Assertions. In: Springer; 2009:3-18. doi:<a href=\"https://doi.org/1556\">1556</a>"}},{"date_created":"2018-12-11T12:08:32Z","type":"conference","_id":"4375","date_updated":"2021-01-12T07:56:30Z","publisher":"Springer","title":"Intra-module Inference","day":"01","alternative_title":["LNCS 5643"],"author":[{"full_name":"Lahiri,Shuvendu K.","last_name":"Lahiri","first_name":"Shuvendu"},{"first_name":"Shaz","full_name":"Qadeer,Shaz","last_name":"Qadeer"},{"full_name":"Galeotti,Juan P.","last_name":"Galeotti","first_name":"Juan"},{"first_name":"Jan","last_name":"Voung","full_name":"Voung,Jan W."},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","first_name":"Thomas"}],"doi":"1555","publication_status":"published","quality_controlled":0,"page":"493 - 508","publist_id":"1082","month":"01","year":"2009","date_published":"2009-01-01T00:00:00Z","conference":{"name":"CAV: Computer Aided Verification"},"citation":{"mla":"Lahiri, Shuvendu, et al. <i>Intra-Module Inference</i>. Springer, 2009, pp. 493–508, doi:<a href=\"https://doi.org/1555\">1555</a>.","apa":"Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., &#38; Wies, T. (2009). Intra-module Inference (pp. 493–508). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/1555\">https://doi.org/1555</a>","chicago":"Lahiri, Shuvendu, Shaz Qadeer, Juan Galeotti, Jan Voung, and Thomas Wies. “Intra-Module Inference,” 493–508. Springer, 2009. <a href=\"https://doi.org/1555\">https://doi.org/1555</a>.","ista":"Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference. CAV: Computer Aided Verification, LNCS 5643, , 493–508.","short":"S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, Springer, 2009, pp. 493–508.","ieee":"S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, and T. Wies, “Intra-module Inference,” presented at the CAV: Computer Aided Verification, 2009, pp. 493–508.","ama":"Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. Intra-module Inference. In: Springer; 2009:493-508. doi:<a href=\"https://doi.org/1555\">1555</a>"},"extern":1,"status":"public"},{"year":"2009","month":"01","publist_id":"1079","status":"public","extern":1,"citation":{"chicago":"Hoenicke, Jochen, K Rustan Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. “It’s Doomed; We Can Prove It,” 338–53. Springer, 2009. <a href=\"https://doi.org/1557\">https://doi.org/1557</a>.","ista":"Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. 2009. It’s Doomed; We Can Prove It. FM: Formal Methods, LNCS 5850, , 338–353.","mla":"Hoenicke, Jochen, et al. <i>It’s Doomed; We Can Prove It</i>. Springer, 2009, pp. 338–53, doi:<a href=\"https://doi.org/1557\">1557</a>.","apa":"Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., &#38; Wies, T. (2009). It’s Doomed; We Can Prove It (pp. 338–353). Presented at the FM: Formal Methods, Springer. <a href=\"https://doi.org/1557\">https://doi.org/1557</a>","ama":"Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. It’s Doomed; We Can Prove It. In: Springer; 2009:338-353. doi:<a href=\"https://doi.org/1557\">1557</a>","short":"J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009, pp. 338–353.","ieee":"J. Hoenicke, K. R. Leino, A. Podelski, M. Schäf, and T. Wies, “It’s Doomed; We Can Prove It,” presented at the FM: Formal Methods, 2009, pp. 338–353."},"conference":{"name":"FM: Formal Methods"},"date_published":"2009-01-01T00:00:00Z","day":"01","alternative_title":["LNCS 5850"],"doi":"1557","author":[{"full_name":"Hoenicke,Jochen","last_name":"Hoenicke","first_name":"Jochen"},{"last_name":"Leino","full_name":"Leino, K Rustan","first_name":"K Rustan"},{"full_name":"Podelski,Andreas","last_name":"Podelski","first_name":"Andreas"},{"last_name":"Schäf","full_name":"Schäf,Martin","first_name":"Martin"},{"first_name":"Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies"}],"title":"It's Doomed; We Can Prove It","publisher":"Springer","_id":"4377","date_updated":"2021-01-12T07:56:31Z","date_created":"2018-12-11T12:08:32Z","type":"conference","page":"338 - 353","publication_status":"published","quality_controlled":0},{"type":"conference","date_created":"2018-12-11T12:08:29Z","date_updated":"2021-01-12T07:56:26Z","volume":5123,"_id":"4366","publisher":"Springer","title":"Heap Assumptions on Demand","author":[{"first_name":"Andreas","full_name":"Podelski,Andreas","last_name":"Podelski"},{"first_name":"Andrey","full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","first_name":"Thomas"}],"doi":"10.1007/978-3-540-70545-1_31","alternative_title":["LNCS"],"day":"01","quality_controlled":0,"publication_status":"published","intvolume":"      5123","abstract":[{"lang":"eng","text":"Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential."}],"page":"314 - 327","publist_id":"1091","month":"01","year":"2008","date_published":"2008-01-01T00:00:00Z","conference":{"name":"CAV: Computer Aided Verification"},"citation":{"ama":"Podelski A, Rybalchenko A, Wies T. Heap Assumptions on Demand. In: Vol 5123. Springer; 2008:314-327. doi:<a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">10.1007/978-3-540-70545-1_31</a>","ieee":"A. Podelski, A. Rybalchenko, and T. Wies, “Heap Assumptions on Demand,” presented at the CAV: Computer Aided Verification, 2008, vol. 5123, pp. 314–327.","short":"A. Podelski, A. Rybalchenko, T. Wies, in:, Springer, 2008, pp. 314–327.","ista":"Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. CAV: Computer Aided Verification, LNCS, vol. 5123, 314–327.","chicago":"Podelski, Andreas, Andrey Rybalchenko, and Thomas Wies. “Heap Assumptions on Demand,” 5123:314–27. Springer, 2008. <a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">https://doi.org/10.1007/978-3-540-70545-1_31</a>.","apa":"Podelski, A., Rybalchenko, A., &#38; Wies, T. (2008). Heap Assumptions on Demand (Vol. 5123, pp. 314–327). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">https://doi.org/10.1007/978-3-540-70545-1_31</a>","mla":"Podelski, Andreas, et al. <i>Heap Assumptions on Demand</i>. Vol. 5123, Springer, 2008, pp. 314–27, doi:<a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">10.1007/978-3-540-70545-1_31</a>."},"status":"public","extern":1},{"extern":1,"status":"public","date_published":"2007-01-01T00:00:00Z","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"citation":{"short":"C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 2007, pp. 74–88.","ieee":"C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard, “Using First-Order Theorem Provers in the Jahob Data Structure Verification System,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, 2007, pp. 74–88.","ama":"Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. Using First-Order Theorem Provers in the Jahob Data Structure Verification System. In: Springer; 2007:74-88. doi:<a href=\"https://doi.org/1552\">1552</a>","mla":"Bouillaguet, Charles, et al. <i>Using First-Order Theorem Provers in the Jahob Data Structure Verification System</i>. Springer, 2007, pp. 74–88, doi:<a href=\"https://doi.org/1552\">1552</a>.","apa":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., &#38; Rinard, M. (2007). Using First-Order Theorem Provers in the Jahob Data Structure Verification System (pp. 74–88). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. <a href=\"https://doi.org/1552\">https://doi.org/1552</a>","ista":"Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. 2007. Using First-Order Theorem Provers in the Jahob Data Structure Verification System. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS 4349, , 74–88.","chicago":"Bouillaguet, Charles, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard. “Using First-Order Theorem Provers in the Jahob Data Structure Verification System,” 74–88. Springer, 2007. <a href=\"https://doi.org/1552\">https://doi.org/1552</a>."},"month":"01","year":"2007","publist_id":"1062","page":"74 - 88","publication_status":"published","quality_controlled":0,"publisher":"Springer","title":"Using First-Order Theorem Provers in the Jahob Data Structure Verification System","day":"01","alternative_title":["LNCS 4349"],"doi":"1552","author":[{"first_name":"Charles","full_name":"Bouillaguet,Charles","last_name":"Bouillaguet"},{"full_name":"Kuncak, Viktor","last_name":"Kuncak","first_name":"Viktor"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","last_name":"Wies","first_name":"Thomas"},{"last_name":"Zee","full_name":"Zee,Karen","first_name":"Karen"},{"last_name":"Rinard","full_name":"Rinard,Martin C.","first_name":"Martin"}],"date_created":"2018-12-11T12:08:37Z","type":"conference","_id":"4394","date_updated":"2021-01-12T07:56:39Z"}]