--- _id: '2447' 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" alternative_title: - LNCS article_processing_charge: No author: - first_name: Ruzica full_name: Piskac, Ruzica last_name: Piskac - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: Piskac R, Wies T, Zufferey D. Automating separation logic using SMT. 2013;8044:773-789. doi:10.1007/978-3-642-39799-8_54 apa: 'Piskac, R., Wies, T., & Zufferey, D. (2013). Automating separation logic using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_54' chicago: Piskac, Ruzica, Thomas Wies, and Damien Zufferey. “Automating Separation Logic Using SMT.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_54. ieee: R. Piskac, T. Wies, and D. Zufferey, “Automating separation logic using SMT,” vol. 8044. Springer, pp. 773–789, 2013. ista: Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT. 8044, 773–789. mla: Piskac, Ruzica, et al. Automating Separation Logic Using SMT. Vol. 8044, Springer, 2013, pp. 773–89, doi:10.1007/978-3-642-39799-8_54. short: R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789. conference: end_date: 2013-07-19 location: St. Petersburg, Russia name: 'CAV: Computer Aided Verification' start_date: 2013-07-13 date_created: 2018-12-11T11:57:43Z date_published: 2013-07-01T00:00:00Z date_updated: 2020-08-11T10:09:47Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-642-39799-8_54 file: - access_level: open_access checksum: 2e866932ab688f47ecd504acb4d5c7d4 content_type: application/pdf creator: dernst date_created: 2020-05-15T11:13:01Z date_updated: 2020-07-14T12:45:41Z file_id: '7859' file_name: 2013_CAV_Piskac.pdf file_size: 309182 relation: main_file file_date_updated: 2020-07-14T12:45:41Z has_accepted_license: '1' intvolume: ' 8044' language: - iso: eng month: '07' oa: 1 oa_version: Submitted Version page: 773 - 789 publication_status: published publisher: Springer publist_id: '4456' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Automating separation logic using SMT type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8044 year: '2013' ... --- _id: '2847' 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. alternative_title: - LNCS author: - first_name: Kshitij full_name: Bansal, Kshitij last_name: Bansal - first_name: Eric full_name: Koskinen, Eric last_name: Koskinen - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: Bansal K, Koskinen E, Wies T, Zufferey D. Structural Counter Abstraction. Piterman N, Smolka S, eds. 2013;7795:62-77. doi:10.1007/978-3-642-36742-7_5 apa: 'Bansal, K., Koskinen, E., Wies, T., & Zufferey, D. (2013). Structural Counter Abstraction. (N. Piterman & S. Smolka, Eds.). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy: Springer. https://doi.org/10.1007/978-3-642-36742-7_5' 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. https://doi.org/10.1007/978-3-642-36742-7_5. ieee: K. Bansal, E. Koskinen, T. Wies, and D. Zufferey, “Structural Counter Abstraction,” vol. 7795. Springer, pp. 62–77, 2013. ista: Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman & S. Smolka). 7795, 62–77. mla: Bansal, Kshitij, et al. Structural Counter Abstraction. Edited by Nir Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:10.1007/978-3-642-36742-7_5. short: K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77. conference: end_date: 2013-03-24 location: Rome, Italy name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2013-03-16 date_created: 2018-12-11T11:59:54Z date_published: 2013-03-01T00:00:00Z date_updated: 2023-09-07T11:36:36Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-642-36742-7_5 ec_funded: 1 editor: - first_name: Nir full_name: Piterman, Nir last_name: Piterman - first_name: Scott full_name: Smolka, Scott last_name: Smolka intvolume: ' 7795' language: - iso: eng main_file_link: - open_access: '1' url: http://arise.or.at/pubpdf/Structural_Counter_Abstraction.pdf month: '03' oa: 1 oa_version: Submitted Version page: 62 - 77 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '3947' quality_controlled: '1' related_material: record: - id: '1405' relation: dissertation_contains status: public scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Structural Counter Abstraction type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 7795 year: '2013' ... --- _id: '3251' abstract: - lang: eng 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. 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. alternative_title: - LNCS author: - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition systems. In: Vol 7148. Springer; 2012:445-460. doi:10.1007/978-3-642-27940-9_29' apa: 'Zufferey, D., Wies, T., & 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. https://doi.org/10.1007/978-3-642-27940-9_29' chicago: Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_29. 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.' 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.' mla: Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29. short: D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460. conference: end_date: 2012-01-24 location: Philadelphia, PA, USA name: 'VMCAI: Verification, Model Checking and Abstract Interpretation' start_date: 2012-01-22 date_created: 2018-12-11T12:02:16Z date_published: 2012-01-01T00:00:00Z date_updated: 2023-09-07T11:36:36Z day: '01' ddc: - '000' - '005' department: - _id: ToHe doi: 10.1007/978-3-642-27940-9_29 ec_funded: 1 file: - access_level: open_access checksum: f2f0d55efa32309ad1fe65a5fcaad90c content_type: application/pdf creator: system date_created: 2018-12-12T10:09:35Z date_updated: 2020-07-14T12:46:05Z file_id: '4759' file_name: IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf file_size: 217104 relation: main_file file_date_updated: 2020-07-14T12:46:05Z has_accepted_license: '1' intvolume: ' 7148' language: - iso: eng month: '01' oa: 1 oa_version: Submitted Version page: 445 - 460 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '3406' pubrep_id: '100' quality_controlled: '1' related_material: record: - id: '1405' relation: dissertation_contains status: public status: public title: Ideal abstractions for well structured transition systems type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 7148 year: '2012' ... --- _id: '3302' 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. author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Anmol full_name: Singh, Anmol id: 72A86902-E99F-11E9-9F62-915534D1B916 last_name: Singh - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.' apa: 'Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.' chicago: Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds,” 1–6. USENIX, 2011. 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.' 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.' mla: Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6. short: T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6. conference: end_date: 2011-06-15 name: 'HotCloud: Workshop on Hot Topics in Cloud Computing' start_date: 2011-06-14 date_created: 2018-12-11T12:02:33Z date_published: 2011-06-14T00:00:00Z date_updated: 2021-01-12T07:42:31Z day: '14' ddc: - '000' - '005' department: - _id: ToHe file: - access_level: open_access checksum: 21a461ac004bb535c83320fe79b30375 content_type: application/pdf creator: system date_created: 2018-12-12T10:18:14Z date_updated: 2020-07-14T12:46:06Z file_id: '5333' file_name: IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf file_size: 232770 relation: main_file file_date_updated: 2020-07-14T12:46:06Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 1 - 6 publication_status: published publisher: USENIX publist_id: '3338' pubrep_id: '90' quality_controlled: '1' status: public title: Static scheduling in clouds type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3324' 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.' alternative_title: - LNCS author: - first_name: Ruzica full_name: Piskac, Ruzica last_name: Piskac - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: 'Piskac R, Wies T. Decision procedures for automating termination proofs. In: Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:10.1007/978-3-642-18275-4_26' apa: 'Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26' chicago: Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011. https://doi.org/10.1007/978-3-642-18275-4_26. 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.' ista: 'Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.' mla: Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:10.1007/978-3-642-18275-4_26. short: R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386. conference: end_date: 2011-01-25 location: Texas, USA name: 'VMCAI: Verification Model Checking and Abstract Interpretation' start_date: 2011-01-23 date_created: 2018-12-11T12:02:40Z date_published: 2011-01-01T00:00:00Z date_updated: 2021-01-12T07:42:39Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-642-18275-4_26 editor: - first_name: Ranjit full_name: Jhala, Ranjit last_name: Jhala - first_name: David full_name: Schmidt, David last_name: Schmidt intvolume: ' 6538' language: - iso: eng main_file_link: - open_access: '1' url: https://infoscience.epfl.ch/record/170697/ month: '01' oa: 1 oa_version: Submitted Version page: 371 - 386 publication_status: published publisher: Springer publist_id: '3311' quality_controlled: '1' scopus_import: 1 status: public title: Decision procedures for automating termination proofs type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6538 year: '2011' ... --- _id: '3358' 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. article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Singh V, Wies T, Zufferey D. Scheduling large jobs by abstraction refinement. In: ACM; 2011:329-342. doi:10.1145/1966445.1966476' apa: 'Henzinger, T. A., Singh, V., Wies, T., & Zufferey, D. (2011). Scheduling large jobs by abstraction refinement (pp. 329–342). Presented at the EuroSys, Salzburg, Austria: ACM. https://doi.org/10.1145/1966445.1966476' chicago: Henzinger, Thomas A, Vasu Singh, Thomas Wies, and Damien Zufferey. “Scheduling Large Jobs by Abstraction Refinement,” 329–42. ACM, 2011. https://doi.org/10.1145/1966445.1966476. 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. ista: Henzinger TA, Singh V, Wies T, Zufferey D. 2011. Scheduling large jobs by abstraction refinement. EuroSys, 329–342. mla: Henzinger, Thomas A., et al. Scheduling Large Jobs by Abstraction Refinement. ACM, 2011, pp. 329–42, doi:10.1145/1966445.1966476. short: T.A. Henzinger, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2011, pp. 329–342. conference: end_date: 2011-04-13 location: Salzburg, Austria name: EuroSys start_date: 2011-04-10 date_created: 2018-12-11T12:02:53Z date_published: 2011-04-10T00:00:00Z date_updated: 2021-01-12T07:42:55Z day: '10' department: - _id: ToHe doi: 10.1145/1966445.1966476 language: - iso: eng main_file_link: - open_access: '1' url: http://cs.nyu.edu/wies/publ/scheduling_large_jobs_by_abstraction_refinement.pdf month: '04' oa: 1 oa_version: Published Version page: 329 - 342 publication_status: published publisher: ACM publist_id: '3257' quality_controlled: '1' scopus_import: 1 status: public title: Scheduling large jobs by abstraction refinement type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '5383' 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. alternative_title: - IST Austria Technical Report author: - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Marco full_name: Muñiz, Marco last_name: Muñiz - first_name: Viktor full_name: Kuncak, Viktor last_name: Kuncak citation: ama: Wies T, Muñiz M, Kuncak V. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria; 2011. doi:10.15479/AT:IST-2011-0005 apa: Wies, T., Muñiz, M., & Kuncak, V. (2011). On an efficient decision procedure for imperative tree data structures. IST Austria. https://doi.org/10.15479/AT:IST-2011-0005 chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0005. ieee: T. Wies, M. Muñiz, and V. Kuncak, On an efficient decision procedure for imperative tree data structures. IST Austria, 2011. ista: Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative tree data structures, IST Austria, 25p. mla: Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005. short: T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative Tree Data Structures, IST Austria, 2011. date_created: 2018-12-12T11:39:01Z date_published: 2011-04-26T00:00:00Z date_updated: 2023-02-23T11:22:16Z day: '26' ddc: - '000' - '006' department: - _id: ToHe doi: 10.15479/AT:IST-2011-0005 file: - access_level: open_access checksum: b20029184c4a819c5f4466a4a3d238b5 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:01Z date_updated: 2020-07-14T12:46:40Z file_id: '5462' file_name: IST-2011-0005_IST-2011-0005.pdf file_size: 619053 relation: main_file file_date_updated: 2020-07-14T12:46:40Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '25' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '19' related_material: record: - id: '3323' relation: later_version status: public status: public title: On an efficient decision procedure for imperative tree data structures type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3323' 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. alternative_title: - 'LNAI ' author: - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Marco full_name: Muñiz, Marco last_name: Muñiz - first_name: Viktor full_name: Kuncak, Viktor last_name: Kuncak citation: 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:10.1007/978-3-642-22438-6_36' apa: 'Wies, T., Muñiz, M., & 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. https://doi.org/10.1007/978-3-642-22438-6_36' chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36. 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.' 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.' mla: Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36. short: T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491. conference: end_date: 2011-08-05 location: Wrocław, Poland name: 'CADE 23: Automated Deduction ' start_date: 2011-07-31 date_created: 2018-12-11T12:02:40Z date_published: 2011-07-19T00:00:00Z date_updated: 2023-02-23T12:23:48Z day: '19' department: - _id: ToHe doi: 10.1007/978-3-642-22438-6_36 intvolume: ' 6803' language: - iso: eng month: '07' oa_version: None page: 476 - 491 publication_status: published publisher: Springer publist_id: '3312' quality_controlled: '1' related_material: record: - id: '5383' relation: earlier_version status: public scopus_import: 1 status: public title: An efficient decision procedure for imperative tree data structures type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6803 year: '2011' ... --- _id: '4364' author: - first_name: Andreas full_name: Podelski,Andreas last_name: Podelski - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: 'Podelski A, Wies T. Counterexample-guided focus. In: ACM; 2010:249-260. doi:10.1145/1707801.1706330' apa: 'Podelski, A., & Wies, T. (2010). Counterexample-guided focus (pp. 249–260). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/10.1145/1707801.1706330' chicago: Podelski, Andreas, and Thomas Wies. “Counterexample-Guided Focus,” 249–60. ACM, 2010. https://doi.org/10.1145/1707801.1706330. ieee: 'A. Podelski and T. Wies, “Counterexample-guided focus,” presented at the POPL: Principles of Programming Languages, 2010, pp. 249–260.' ista: 'Podelski A, Wies T. 2010. Counterexample-guided focus. POPL: Principles of Programming Languages, 249–260.' mla: Podelski, Andreas, and Thomas Wies. Counterexample-Guided Focus. ACM, 2010, pp. 249–60, doi:10.1145/1707801.1706330. short: A. Podelski, T. Wies, in:, ACM, 2010, pp. 249–260. conference: name: 'POPL: Principles of Programming Languages' date_created: 2018-12-11T12:08:28Z date_published: 2010-01-01T00:00:00Z date_updated: 2021-01-12T07:56:26Z day: '01' doi: 10.1145/1707801.1706330 extern: 1 month: '01' page: 249 - 260 publication_status: published publisher: ACM publist_id: '1093' quality_controlled: 0 status: public title: Counterexample-guided focus type: conference year: '2010' ... --- _id: '4378' 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.' alternative_title: - LNCS author: - first_name: Viktor full_name: Kuncak, Viktor last_name: Kuncak - first_name: Ruzica full_name: Piskac, Ruzica last_name: Piskac - first_name: Philippe full_name: Suter, Philippe last_name: Suter - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: 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:10.1007/978-3-642-11319-2_6' apa: 'Kuncak, V., Piskac, R., Suter, P., & Wies, T. (2010). Building a calculus of data structures. In G. Barthe & M. Hermenegildo (Eds.) (Vol. 5944, pp. 26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-642-11319-2_6' 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. https://doi.org/10.1007/978-3-642-11319-2_6. 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.' 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.' mla: Kuncak, Viktor, et al. Building a Calculus of Data Structures. Edited by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44, doi:10.1007/978-3-642-11319-2_6. short: V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo (Eds.), Springer, 2010, pp. 26–44. conference: end_date: 2010-01-19 location: Madrid, Spain name: 'VMCAI: Verification, Model Checking and Abstract Interpretation' start_date: 2010-01-17 date_created: 2018-12-11T12:08:33Z date_published: 2010-01-01T00:00:00Z date_updated: 2021-01-12T07:56:31Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-642-11319-2_6 editor: - first_name: Gilles full_name: Barthe, Gilles last_name: Barthe - first_name: Manuel full_name: Hermenegildo, Manuel last_name: Hermenegildo intvolume: ' 5944' language: - iso: eng main_file_link: - open_access: '1' url: https://infoscience.epfl.ch/record/161290/ month: '01' oa: 1 oa_version: Submitted Version page: 26 - 44 publication_status: published publisher: Springer publist_id: '1081' quality_controlled: '1' scopus_import: 1 status: public title: Building a calculus of data structures type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 5944 year: '2010' ... --- _id: '4381' 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. article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Anmol full_name: Tomar, Anmol id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87 last_name: Tomar - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: 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:10.1109/CLOUD.2010.71' apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71' 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. https://doi.org/10.1109/CLOUD.2010.71.' 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.' 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.' mla: 'Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.' short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90. conference: end_date: 2010-07-10 location: Miami, USA name: 'CLOUD: Cloud Computing' start_date: 2010-07-05 date_created: 2018-12-11T12:08:33Z date_published: 2010-08-26T00:00:00Z date_updated: 2021-01-12T07:56:33Z day: '26' ddc: - '004' department: - _id: ToHe doi: 10.1109/CLOUD.2010.71 file: - access_level: open_access checksum: 98e534675339a8e2beca08890d048145 content_type: application/pdf creator: system date_created: 2018-12-12T10:16:03Z date_updated: 2020-07-14T12:46:28Z file_id: '5188' file_name: IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf file_size: 467436 relation: main_file file_date_updated: 2020-07-14T12:46:28Z has_accepted_license: '1' language: - iso: eng month: '08' oa: 1 oa_version: Submitted Version page: 83 - 90 publication_status: published publisher: IEEE publist_id: '1077' pubrep_id: '47' quality_controlled: '1' scopus_import: 1 status: public title: 'FlexPRICE: Flexible provisioning of resources in a cloud environment' type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2010' ... --- _id: '4380' 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. author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Anmol full_name: Tomar, Anmol id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87 last_name: Tomar - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud resources. In: ACM; 2010:1-8. doi:10.1145/1879021.1879022' apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022' chicago: Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “A Marketplace for Cloud Resources,” 1–8. ACM, 2010. https://doi.org/10.1145/1879021.1879022. 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.' ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.' mla: Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM, 2010, pp. 1–8, doi:10.1145/1879021.1879022. short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8. conference: end_date: 2010-10-29 location: Arizona, USA name: 'EMSOFT: Embedded Software ' start_date: 2010-10-24 date_created: 2018-12-11T12:08:33Z date_published: 2010-10-24T00:00:00Z date_updated: 2021-01-12T07:56:32Z day: '24' ddc: - '005' department: - _id: ToHe doi: 10.1145/1879021.1879022 file: - access_level: open_access checksum: 7680dd24016810710f7c977bc94f85e9 content_type: application/pdf creator: system date_created: 2018-12-12T10:09:42Z date_updated: 2020-07-14T12:46:28Z file_id: '4767' file_name: IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf file_size: 222626 relation: main_file file_date_updated: 2020-07-14T12:46:28Z has_accepted_license: '1' language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 1 - 8 publication_status: published publisher: ACM publist_id: '1078' pubrep_id: '48' quality_controlled: '1' scopus_import: 1 status: public title: A marketplace for cloud resources type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2010' ... --- _id: '533' 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 ("noise") 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. author: - first_name: Jochen full_name: Hoenicke, Jochen last_name: Hoenicke - first_name: Kari full_name: Leino, Kari last_name: Leino - first_name: Andreas full_name: Podelski, Andreas last_name: Podelski - first_name: Martin full_name: Schäf, Martin last_name: Schäf - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. Doomed program points. Formal Methods in System Design. 2010;37(2-3):171-199. doi:10.1007/s10703-010-0102-0 apa: Hoenicke, J., Leino, K., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed program points. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-010-0102-0 chicago: Hoenicke, Jochen, Kari Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. “Doomed Program Points.” Formal Methods in System Design. Springer, 2010. https://doi.org/10.1007/s10703-010-0102-0. ieee: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, and T. Wies, “Doomed program points,” Formal Methods in System Design, vol. 37, no. 2–3. Springer, pp. 171–199, 2010. 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. mla: Hoenicke, Jochen, et al. “Doomed Program Points.” Formal Methods in System Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0. short: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in System Design 37 (2010) 171–199. date_created: 2018-12-11T11:47:01Z date_published: 2010-12-01T00:00:00Z date_updated: 2021-01-12T08:01:28Z day: '01' department: - _id: ToHe doi: 10.1007/s10703-010-0102-0 intvolume: ' 37' issue: 2-3 language: - iso: eng month: '12' oa_version: None page: 171 - 199 publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '7284' quality_controlled: '1' scopus_import: 1 status: public title: Doomed program points type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 37 year: '2010' ... --- _id: '4361' 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. alternative_title: - LNCS author: - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 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:10.1007/978-3-642-12032-9_8' apa: 'Wies, T., Zufferey, D., & 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. https://doi.org/10.1007/978-3-642-12032-9_8' chicago: Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010. https://doi.org/10.1007/978-3-642-12032-9_8. 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.' 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. Forward Analysis of Depth-Bounded Processes. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:10.1007/978-3-642-12032-9_8. short: T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108. conference: end_date: 2010-03-28 location: Paphos, Cyprus name: 'FoSSaCS: Foundations of Software Science and Computation Structures' start_date: 2010-03-20 date_created: 2018-12-11T12:08:27Z date_published: 2010-03-01T00:00:00Z date_updated: 2023-09-07T11:36:36Z day: '01' ddc: - '004' department: - _id: ToHe doi: 10.1007/978-3-642-12032-9_8 editor: - first_name: Luke full_name: Ong, Luke last_name: Ong file: - access_level: open_access checksum: 3e610de84937d821316362658239134a content_type: application/pdf creator: system date_created: 2018-12-12T10:08:17Z date_updated: 2020-07-14T12:46:27Z file_id: '4677' file_name: IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf file_size: 240766 relation: main_file file_date_updated: 2020-07-14T12:46:27Z has_accepted_license: '1' intvolume: ' 6014' language: - iso: eng month: '03' oa: 1 oa_version: Submitted Version page: 94 - 108 publication_status: published publisher: Springer publist_id: '1099' pubrep_id: '50' quality_controlled: '1' related_material: record: - id: '1405' relation: dissertation_contains status: public scopus_import: 1 status: public title: Forward analysis of depth-bounded processes type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6014 year: '2010' ... --- _id: '4365' alternative_title: - LNCS 5673 author: - first_name: Mohamed full_name: Seghir,Mohamed Nassim last_name: Seghir - first_name: Andreas full_name: Podelski,Andreas last_name: Podelski - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: 'Seghir M, Podelski A, Wies T. Abstraction Refinement for Quantified Array Assertions. In: Springer; 2009:3-18. doi:1556' apa: 'Seghir, M., Podelski, A., & Wies, T. (2009). Abstraction Refinement for Quantified Array Assertions (pp. 3–18). Presented at the SAS: Static Analysis Symposium, Springer. https://doi.org/1556' chicago: Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement for Quantified Array Assertions,” 3–18. Springer, 2009. https://doi.org/1556. 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.' ista: 'Seghir M, Podelski A, Wies T. 2009. Abstraction Refinement for Quantified Array Assertions. SAS: Static Analysis Symposium, LNCS 5673, , 3–18.' mla: Seghir, Mohamed, et al. Abstraction Refinement for Quantified Array Assertions. Springer, 2009, pp. 3–18, doi:1556. short: M. Seghir, A. Podelski, T. Wies, in:, Springer, 2009, pp. 3–18. conference: name: 'SAS: Static Analysis Symposium' date_created: 2018-12-11T12:08:29Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:56:26Z day: '01' doi: '1556' extern: 1 month: '01' page: 3 - 18 publication_status: published publisher: Springer publist_id: '1094' quality_controlled: 0 status: public title: Abstraction Refinement for Quantified Array Assertions type: conference year: '2009' ... --- _id: '4360' alternative_title: - LNCS 5749 author: - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Ruzica full_name: Piskac, Ruzica last_name: Piskac - first_name: Viktor full_name: Kuncak, Viktor last_name: Kuncak citation: ama: 'Wies T, Piskac R, Kuncak V. Combining Theories with Shared Set Operations. In: Springer; 2009:366-382. doi:1558' apa: 'Wies, T., Piskac, R., & Kuncak, V. (2009). Combining Theories with Shared Set Operations (pp. 366–382). Presented at the FroCoS: Frontiers of Combining Systems, Springer. https://doi.org/1558' chicago: Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with Shared Set Operations,” 366–82. Springer, 2009. https://doi.org/1558. 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.' ista: 'Wies T, Piskac R, Kuncak V. 2009. Combining Theories with Shared Set Operations. FroCoS: Frontiers of Combining Systems, LNCS 5749, , 366–382.' mla: Wies, Thomas, et al. Combining Theories with Shared Set Operations. Springer, 2009, pp. 366–82, doi:1558. short: T. Wies, R. Piskac, V. Kuncak, in:, Springer, 2009, pp. 366–382. conference: name: 'FroCoS: Frontiers of Combining Systems' date_created: 2018-12-11T12:08:27Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:56:24Z day: '01' doi: '1558' extern: 1 month: '01' page: 366 - 382 publication_status: published publisher: Springer publist_id: '1098' quality_controlled: 0 status: public title: Combining Theories with Shared Set Operations type: conference year: '2009' ... --- _id: '4375' alternative_title: - LNCS 5643 author: - first_name: Shuvendu full_name: Lahiri,Shuvendu K. last_name: Lahiri - first_name: Shaz full_name: Qadeer,Shaz last_name: Qadeer - first_name: Juan full_name: Galeotti,Juan P. last_name: Galeotti - first_name: Jan full_name: Voung,Jan W. last_name: Voung - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: 'Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. Intra-module Inference. In: Springer; 2009:493-508. doi:1555' apa: 'Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., & Wies, T. (2009). Intra-module Inference (pp. 493–508). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1555' chicago: Lahiri, Shuvendu, Shaz Qadeer, Juan Galeotti, Jan Voung, and Thomas Wies. “Intra-Module Inference,” 493–508. Springer, 2009. https://doi.org/1555. 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.' ista: 'Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference. CAV: Computer Aided Verification, LNCS 5643, , 493–508.' mla: Lahiri, Shuvendu, et al. Intra-Module Inference. Springer, 2009, pp. 493–508, doi:1555. short: S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, Springer, 2009, pp. 493–508. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:32Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:56:30Z day: '01' doi: '1555' extern: 1 month: '01' page: 493 - 508 publication_status: published publisher: Springer publist_id: '1082' quality_controlled: 0 status: public title: Intra-module Inference type: conference year: '2009' ... --- _id: '4377' alternative_title: - LNCS 5850 author: - first_name: Jochen full_name: Hoenicke,Jochen last_name: Hoenicke - first_name: K Rustan full_name: Leino, K Rustan last_name: Leino - first_name: Andreas full_name: Podelski,Andreas last_name: Podelski - first_name: Martin full_name: Schäf,Martin last_name: Schäf - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: 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:1557' apa: 'Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., & Wies, T. (2009). It’s Doomed; We Can Prove It (pp. 338–353). Presented at the FM: Formal Methods, Springer. https://doi.org/1557' 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. https://doi.org/1557. 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.' 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. It’s Doomed; We Can Prove It. Springer, 2009, pp. 338–53, doi:1557. short: J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009, pp. 338–353. conference: name: 'FM: Formal Methods' date_created: 2018-12-11T12:08:32Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:56:31Z day: '01' doi: '1557' extern: 1 month: '01' page: 338 - 353 publication_status: published publisher: Springer publist_id: '1079' quality_controlled: 0 status: public title: It's Doomed; We Can Prove It type: conference year: '2009' ... --- _id: '4366' 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. alternative_title: - LNCS author: - first_name: Andreas full_name: Podelski,Andreas last_name: Podelski - first_name: Andrey full_name: Rybalchenko, Andrey last_name: Rybalchenko - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: 'Podelski A, Rybalchenko A, Wies T. Heap Assumptions on Demand. In: Vol 5123. Springer; 2008:314-327. doi:10.1007/978-3-540-70545-1_31' apa: 'Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap Assumptions on Demand (Vol. 5123, pp. 314–327). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-540-70545-1_31' chicago: Podelski, Andreas, Andrey Rybalchenko, and Thomas Wies. “Heap Assumptions on Demand,” 5123:314–27. Springer, 2008. https://doi.org/10.1007/978-3-540-70545-1_31. 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.' ista: 'Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. CAV: Computer Aided Verification, LNCS, vol. 5123, 314–327.' mla: Podelski, Andreas, et al. Heap Assumptions on Demand. Vol. 5123, Springer, 2008, pp. 314–27, doi:10.1007/978-3-540-70545-1_31. short: A. Podelski, A. Rybalchenko, T. Wies, in:, Springer, 2008, pp. 314–327. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:29Z date_published: 2008-01-01T00:00:00Z date_updated: 2021-01-12T07:56:26Z day: '01' doi: 10.1007/978-3-540-70545-1_31 extern: 1 intvolume: ' 5123' month: '01' page: 314 - 327 publication_status: published publisher: Springer publist_id: '1091' quality_controlled: 0 status: public title: Heap Assumptions on Demand type: conference volume: 5123 year: '2008' ... --- _id: '4394' alternative_title: - LNCS 4349 author: - first_name: Charles full_name: Bouillaguet,Charles last_name: Bouillaguet - first_name: Viktor full_name: Kuncak, Viktor last_name: Kuncak - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Karen full_name: Zee,Karen last_name: Zee - first_name: Martin full_name: Rinard,Martin C. last_name: Rinard citation: 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:1552' apa: 'Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & 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. https://doi.org/1552' 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. https://doi.org/1552. 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.' 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.' mla: Bouillaguet, Charles, et al. Using First-Order Theorem Provers in the Jahob Data Structure Verification System. Springer, 2007, pp. 74–88, doi:1552. short: C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 2007, pp. 74–88. conference: name: 'VMCAI: Verification, Model Checking and Abstract Interpretation' date_created: 2018-12-11T12:08:37Z date_published: 2007-01-01T00:00:00Z date_updated: 2021-01-12T07:56:39Z day: '01' doi: '1552' extern: 1 month: '01' page: 74 - 88 publication_status: published publisher: Springer publist_id: '1062' quality_controlled: 0 status: public title: Using First-Order Theorem Provers in the Jahob Data Structure Verification System type: conference year: '2007' ...