[{"type":"conference","conference":{"name":"EMSOFT: Embedded Software "},"year":"2004","publication_status":"published","day":"01","publisher":"ACM","date_updated":"2021-01-12T07:57:01Z","title":"A typed assembly language for real-time programs","doi":"10.1145/1017753.1017774","quality_controlled":0,"acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327 and by the NSF grants CCR- 0208875 and CCR-0225610.","_id":"4445","abstract":[{"text":"We present a type system for E code, which is an assembly language that manages the release, interaction, and termination of real-time tasks. E code specifies a deadline for each task, and the type system ensures that the deadlines are path-insensitive. We show that typed E programs allow, for given worst-case execution times of tasks, a simple schedulability analysis. Moreover, the real-time programming language Giotto can be compiled into typed E~code. This shows that typed E~code identifies an easily schedulable yet expressive class of real-time programs. We have extended the Giotto compiler to generate typed E code, and enabled the run-time system for E code to perform a type and schedulability check before executing the code.","lang":"eng"}],"page":"104 - 113","date_published":"2004-09-01T00:00:00Z","status":"public","publist_id":"285","extern":1,"date_created":"2018-12-11T12:08:53Z","citation":{"apa":"Henzinger, T. A., &#38; Kirsch, C. (2004). A typed assembly language for real-time programs (pp. 104–113). Presented at the EMSOFT: Embedded Software , ACM. <a href=\"https://doi.org/10.1145/1017753.1017774\">https://doi.org/10.1145/1017753.1017774</a>","ista":"Henzinger TA, Kirsch C. 2004. A typed assembly language for real-time programs. EMSOFT: Embedded Software , 104–113.","ama":"Henzinger TA, Kirsch C. A typed assembly language for real-time programs. In: ACM; 2004:104-113. doi:<a href=\"https://doi.org/10.1145/1017753.1017774\">10.1145/1017753.1017774</a>","mla":"Henzinger, Thomas A., and Christoph Kirsch. <i>A Typed Assembly Language for Real-Time Programs</i>. ACM, 2004, pp. 104–13, doi:<a href=\"https://doi.org/10.1145/1017753.1017774\">10.1145/1017753.1017774</a>.","short":"T.A. Henzinger, C. Kirsch, in:, ACM, 2004, pp. 104–113.","ieee":"T. A. Henzinger and C. Kirsch, “A typed assembly language for real-time programs,” presented at the EMSOFT: Embedded Software , 2004, pp. 104–113.","chicago":"Henzinger, Thomas A, and Christoph Kirsch. “A Typed Assembly Language for Real-Time Programs,” 104–13. ACM, 2004. <a href=\"https://doi.org/10.1145/1017753.1017774\">https://doi.org/10.1145/1017753.1017774</a>."},"month":"09","author":[{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kirsch, Christoph M","first_name":"Christoph","last_name":"Kirsch"}]},{"month":"04","author":[{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"first_name":"Kenneth","last_name":"Mcmillan","full_name":"McMillan, Kenneth L"}],"extern":1,"citation":{"chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan. “Abstractions from Proofs,” 232–44. ACM, 2004. <a href=\"https://doi.org/10.1145/964001.964021\">https://doi.org/10.1145/964001.964021</a>.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, “Abstractions from proofs,” presented at the POPL: Principles of Programming Languages, 2004, pp. 232–244.","mla":"Henzinger, Thomas A., et al. <i>Abstractions from Proofs</i>. ACM, 2004, pp. 232–44, doi:<a href=\"https://doi.org/10.1145/964001.964021\">10.1145/964001.964021</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, ACM, 2004, pp. 232–244.","ama":"Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In: ACM; 2004:232-244. doi:<a href=\"https://doi.org/10.1145/964001.964021\">10.1145/964001.964021</a>","ista":"Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs. POPL: Principles of Programming Languages, 232–244.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Mcmillan, K. (2004). Abstractions from proofs (pp. 232–244). Presented at the POPL: Principles of Programming Languages, ACM. <a href=\"https://doi.org/10.1145/964001.964021\">https://doi.org/10.1145/964001.964021</a>"},"date_created":"2018-12-11T12:08:57Z","abstract":[{"text":"The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define the past and the future segment of the trace. Each interpolant is a relationship between current values of program variables, and is relevant only at that particular program location. It can be found by a linear scan of the proof of infeasibility of the trace.We develop our method for programs with arithmetic and pointer expressions, and call-by-value function calls. For function calls, Craig interpolation offers a systematic way of generating relevant predicates that contain only the local variables of the function and the values of the formal parameters when the function was called. We have extended our model checker Blast with predicate discovery by Craig interpolation, and applied it successfully to C programs with more than 130,000 lines of code, which was not possible with approaches that build less parsimonious abstractions.","lang":"eng"}],"page":"232 - 244","status":"public","date_published":"2004-04-01T00:00:00Z","publist_id":"270","_id":"4458","title":"Abstractions from proofs","doi":"10.1145/964001.964021","quality_controlled":0,"publication_status":"published","day":"01","publisher":"ACM","date_updated":"2021-01-12T07:57:06Z","conference":{"name":"POPL: Principles of Programming Languages"},"year":"2004","type":"conference"},{"extern":1,"date_created":"2018-12-11T12:08:57Z","citation":{"ista":"Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference. PLDI: Programming Languages Design and Implementation, 1–13.","apa":"Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). Race checking by context inference (pp. 1–13). Presented at the PLDI: Programming Languages Design and Implementation, ACM. <a href=\"https://doi.org/10.1145/996841.996844\">https://doi.org/10.1145/996841.996844</a>","ama":"Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In: ACM; 2004:1-13. doi:<a href=\"https://doi.org/10.1145/996841.996844\">10.1145/996841.996844</a>","mla":"Henzinger, Thomas A., et al. <i>Race Checking by Context Inference</i>. ACM, 2004, pp. 1–13, doi:<a href=\"https://doi.org/10.1145/996841.996844\">10.1145/996841.996844</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2004, pp. 1–13.","chicago":"Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking by Context Inference,” 1–13. ACM, 2004. <a href=\"https://doi.org/10.1145/996841.996844\">https://doi.org/10.1145/996841.996844</a>.","ieee":"T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,” presented at the PLDI: Programming Languages Design and Implementation, 2004, pp. 1–13."},"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"}],"month":"06","_id":"4459","page":"1 - 13","abstract":[{"lang":"eng","text":"Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. This algorithm, called CIRC, has been implemented in BLAST and succeeds in checking many examples of NESC code for data races. In particular, BLAST proves the absence of races in several cases where previous race checkers give false positives."}],"publist_id":"271","status":"public","date_published":"2004-06-01T00:00:00Z","day":"01","publication_status":"published","date_updated":"2021-01-12T07:57:07Z","publisher":"ACM","doi":"10.1145/996841.996844","title":"Race checking by context inference","quality_controlled":0,"type":"conference","conference":{"name":"PLDI: Programming Languages Design and Implementation"},"year":"2004"},{"year":"2004","volume":2772,"type":"book_chapter","quality_controlled":0,"title":"Extreme model checking","doi":"10.1007/978-3-540-39910-0_16","publisher":"Springer","date_updated":"2021-01-12T07:57:08Z","publication_status":"published","day":"24","status":"public","date_published":"2004-02-24T00:00:00Z","publist_id":"269","publication":"Verification: Theory and Practice","abstract":[{"text":"One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i.e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expensive verification tasks. We show that the lazy-abstraction algorithm, and its implementation in Blast, can be extended to support the fully automatic and incremental checking of temporal safety properties during software development.","lang":"eng"}],"page":"332 - 358","acknowledgement":"This work was supported in part by the NSF grants CCR-9988172, CCR-0085949, and CCR-0234690, the ONR grant N00014-02-1-0671, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660. ","_id":"4461","intvolume":"      2772","month":"02","author":[{"full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"full_name":"Sanvido, Marco A","last_name":"Sanvido","first_name":"Marco"}],"citation":{"ama":"Henzinger TA, Jhala R, Majumdar R, Sanvido M. Extreme model checking. In: <i>Verification: Theory and Practice</i>. Vol 2772. Springer; 2004:332-358. doi:<a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">10.1007/978-3-540-39910-0_16</a>","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sanvido, M. (2004). Extreme model checking. In <i>Verification: Theory and Practice</i> (Vol. 2772, pp. 332–358). Springer. <a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">https://doi.org/10.1007/978-3-540-39910-0_16</a>","ista":"Henzinger TA, Jhala R, Majumdar R, Sanvido M. 2004.Extreme model checking. In: Verification: Theory and Practice. LNCS, vol. 2772, 332–358.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and M. Sanvido, “Extreme model checking,” in <i>Verification: Theory and Practice</i>, vol. 2772, Springer, 2004, pp. 332–358.","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Marco Sanvido. “Extreme Model Checking.” In <i>Verification: Theory and Practice</i>, 2772:332–58. Springer, 2004. <a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">https://doi.org/10.1007/978-3-540-39910-0_16</a>.","mla":"Henzinger, Thomas A., et al. “Extreme Model Checking.” <i>Verification: Theory and Practice</i>, vol. 2772, Springer, 2004, pp. 332–58, doi:<a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">10.1007/978-3-540-39910-0_16</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, M. Sanvido, in:, Verification: Theory and Practice, Springer, 2004, pp. 332–358."},"date_created":"2018-12-11T12:08:58Z","alternative_title":["LNCS"],"extern":1},{"publication_status":"published","day":"12","publisher":"Springer","date_updated":"2021-01-12T07:59:26Z","title":"Event-driven programming with logical execution times","doi":"10.1007/978-3-540-24743-2_24","quality_controlled":0,"volume":2993,"type":"conference","conference":{"name":"HSCC: Hybrid Systems - Computation and Control"},"year":"2004","alternative_title":["LNCS"],"extern":1,"citation":{"ama":"Ghosal A, Henzinger TA, Kirsch C, Sanvido M. Event-driven programming with logical execution times. In: Vol 2993. Springer; 2004:167-170. doi:<a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">10.1007/978-3-540-24743-2_24</a>","ista":"Ghosal A, Henzinger TA, Kirsch C, Sanvido M. 2004. Event-driven programming with logical execution times. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 2993, 167–170.","apa":"Ghosal, A., Henzinger, T. A., Kirsch, C., &#38; Sanvido, M. (2004). Event-driven programming with logical execution times (Vol. 2993, pp. 167–170). Presented at the HSCC: Hybrid Systems - Computation and Control, Springer. <a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">https://doi.org/10.1007/978-3-540-24743-2_24</a>","chicago":"Ghosal, Arkadeb, Thomas A Henzinger, Christoph Kirsch, and Marco Sanvido. “Event-Driven Programming with Logical Execution Times,” 2993:167–70. Springer, 2004. <a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">https://doi.org/10.1007/978-3-540-24743-2_24</a>.","ieee":"A. Ghosal, T. A. Henzinger, C. Kirsch, and M. Sanvido, “Event-driven programming with logical execution times,” presented at the HSCC: Hybrid Systems - Computation and Control, 2004, vol. 2993, pp. 167–170.","mla":"Ghosal, Arkadeb, et al. <i>Event-Driven Programming with Logical Execution Times</i>. Vol. 2993, Springer, 2004, pp. 167–70, doi:<a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">10.1007/978-3-540-24743-2_24</a>.","short":"A. Ghosal, T.A. Henzinger, C. Kirsch, M. Sanvido, in:, Springer, 2004, pp. 167–170."},"date_created":"2018-12-11T12:09:18Z","month":"03","author":[{"first_name":"Arkadeb","last_name":"Ghosal","full_name":"Ghosal, Arkadeb"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph M"},{"full_name":"Sanvido, Marco A","first_name":"Marco","last_name":"Sanvido"}],"acknowledgement":"This research is supported by the AFOSR MURI grant F49620-00-1-0327, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, and the NSF grants CCR-0208875 and CCR-0225610.","intvolume":"      2993","_id":"4525","abstract":[{"text":"We present a new high-level programming language, called xGiotto, for programming applications with hard real-time constraints. Like its predecessor, xGiotto is based on the LET (logical execution time) assumption: the programmer specifies when the outputs of a task become available, and the compiler checks if the specification can be implemented on a given platform. However, while the predecessor language xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events. Indeed, through a mechanism called event scoping, events are the main structuring principle of the new language. The xGiotto compiler and run-time system implement event scoping through a tree-based event filter. The compiler also checks programs for determinism (absence of race conditions).","lang":"eng"}],"page":"167 - 170","date_published":"2004-03-12T00:00:00Z","status":"public","publist_id":"200"},{"extern":1,"citation":{"ama":"Chatterjee K, De Alfaro L, Henzinger TA. Trading memory for randomness. In: IEEE; 2004:206-217. doi:<a href=\"https://doi.org/10.1109/QEST.2004.10051\">10.1109/QEST.2004.10051</a>","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2004. Trading memory for randomness. QEST: Quantitative Evaluation of Systems, 206–217.","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2004). Trading memory for randomness (pp. 206–217). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. <a href=\"https://doi.org/10.1109/QEST.2004.10051\">https://doi.org/10.1109/QEST.2004.10051</a>","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Trading Memory for Randomness,” 206–17. IEEE, 2004. <a href=\"https://doi.org/10.1109/QEST.2004.10051\">https://doi.org/10.1109/QEST.2004.10051</a>.","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Trading memory for randomness,” presented at the QEST: Quantitative Evaluation of Systems, 2004, pp. 206–217.","mla":"Chatterjee, Krishnendu, et al. <i>Trading Memory for Randomness</i>. IEEE, 2004, pp. 206–17, doi:<a href=\"https://doi.org/10.1109/QEST.2004.10051\">10.1109/QEST.2004.10051</a>.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2004, pp. 206–217."},"date_created":"2018-12-11T12:09:27Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"de Alfaro, Luca"},{"full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"month":"09","_id":"4555","page":"206 - 217","abstract":[{"lang":"eng","text":"Strategies in repeated games can be classified as to whether or not they use memory and/or randomization. We consider Markov decision processes and 2-player graph games, both of the deterministic and probabilistic varieties. We characterize when memory and/or randomization are required for winning with respect to various classes of w-regular objectives, noting particularly when the use of memory can be traded for the use of randomization. In particular, we show that Markov decision processes allow randomized memoryless optimal strategies for all M?ller objectives. Furthermore, we show that 2-player probabilistic graph games allow randomized memoryless strategies for winning with probability 1 those M?ller objectives which are upward-closed. Upward-closure means that if a set α of infinitely repeating vertices is winning, then all supersets of α are also winning."}],"publist_id":"155","status":"public","date_published":"2004-09-30T00:00:00Z","day":"30","publication_status":"published","date_updated":"2021-01-12T07:59:40Z","publisher":"IEEE","doi":"10.1109/QEST.2004.10051","title":"Trading memory for randomness","quality_controlled":0,"type":"conference","conference":{"name":"QEST: Quantitative Evaluation of Systems"},"year":"2004"},{"_id":"4556","intvolume":"       194","page":"144 - 174","abstract":[{"lang":"eng","text":"We study the problem of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in a cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we show that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we consider, the two problems are PSPACE-hard and can be solved in exponential time. While the complexities are high, our algorithms are exponential only in the number of handlers, and polynomial in the size of the program."}],"publist_id":"156","publication":"Information and Computation","issue":"2","date_published":"2004-08-11T00:00:00Z","status":"public","extern":1,"date_created":"2018-12-11T12:09:28Z","citation":{"ama":"Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. Stack size analysis for interrupt-driven programs. <i>Information and Computation</i>. 2004;194(2):144-174. doi:<a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">10.1016/j.ic.2004.06.001</a>","apa":"Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., &#38; Palsberg, J. (2004). Stack size analysis for interrupt-driven programs. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">https://doi.org/10.1016/j.ic.2004.06.001</a>","ista":"Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. 2004. Stack size analysis for interrupt-driven programs. Information and Computation. 194(2), 144–174.","ieee":"K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg, “Stack size analysis for interrupt-driven programs,” <i>Information and Computation</i>, vol. 194, no. 2. Elsevier, pp. 144–174, 2004.","chicago":"Chatterjee, Krishnendu, Di Ma, Ritankar Majumdar, Tian Zhao, Thomas A Henzinger, and Jens Palsberg. “Stack Size Analysis for Interrupt-Driven Programs.” <i>Information and Computation</i>. Elsevier, 2004. <a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">https://doi.org/10.1016/j.ic.2004.06.001</a>.","short":"K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, J. Palsberg, Information and Computation 194 (2004) 144–174.","mla":"Chatterjee, Krishnendu, et al. “Stack Size Analysis for Interrupt-Driven Programs.” <i>Information and Computation</i>, vol. 194, no. 2, Elsevier, 2004, pp. 144–74, doi:<a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">10.1016/j.ic.2004.06.001</a>."},"author":[{"full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Ma, Di","last_name":"Ma","first_name":"Di"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"last_name":"Zhao","first_name":"Tian","full_name":"Zhao, Tian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"last_name":"Palsberg","first_name":"Jens","full_name":"Palsberg, Jens"}],"month":"08","type":"journal_article","volume":194,"year":"2004","day":"11","publication_status":"published","date_updated":"2021-01-12T07:59:40Z","publisher":"Elsevier","doi":"10.1016/j.ic.2004.06.001","title":"Stack size analysis for interrupt-driven programs","quality_controlled":0},{"conference":{"name":"SODA: Symposium on Discrete Algorithms"},"year":"2004","type":"conference","title":"Quantitative stochastic parity games","quality_controlled":0,"publication_status":"published","day":"01","publisher":"SIAM","date_updated":"2021-01-12T07:59:41Z","abstract":[{"lang":"eng","text":"We study perfect-information stochastic parity games. These are two-player nonterminating games which are played on a graph with turn-based probabilistic transitions. A play results in an infinite path and the conflicting goals of the two players are ω-regular path properties, formalized as parity winning conditions. The qualitative solution of such a game amounts to computing the set of vertices from which a player has a strategy to win with probability 1 (or with positive probability). The quantitative solution amounts to computing the value of the game in every vertex, i.e., the highest probability with which a player can guarantee satisfaction of his own objective in a play that starts from the vertex.For the important special case of one-player stochastic parity games (parity Markov decision processes) we give polynomial-time algorithms both for the qualitative and the quantitative solution. The running time of the qualitative solution is O(d · m3/2) for graphs with m edges and d priorities. The quantitative solution is based on a linear-programming formulation.For the two-player case, we establish the existence of optimal pure memoryless strategies. This has several important ramifications. First, it implies that the values of the games are rational. This is in contrast to the concurrent stochastic parity games of de Alfaro et al.; there, values are in general algebraic numbers, optimal strategies do not exist, and ε-optimal strategies have to be mixed and with infinite memory. Second, the existence of optimal pure memoryless strategies together with the polynomial-time solution forone-player case implies that the quantitative two-player stochastic parity game problem is in NP ∩ co-NP. This generalizes a result of Condon for stochastic games with reachability objectives. It also constitutes an exponential improvement over the best previous algorithm, which is based on a doubly exponential procedure of de Alfaro and Majumdar for concurrent stochastic parity games and provides only ε-approximations of the values."}],"page":"121 - 130","status":"public","date_published":"2004-01-01T00:00:00Z","publist_id":"153","_id":"4558","month":"01","author":[{"orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Jurdziński","first_name":"Marcin","full_name":"Jurdziński, Marcin"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"extern":1,"date_created":"2018-12-11T12:09:28Z","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Stochastic Parity Games</i>. SIAM, 2004, pp. 121–30.","short":"K. Chatterjee, M. Jurdziński, T.A. Henzinger, in:, SIAM, 2004, pp. 121–130.","ieee":"K. Chatterjee, M. Jurdziński, and T. A. Henzinger, “Quantitative stochastic parity games,” presented at the SODA: Symposium on Discrete Algorithms, 2004, pp. 121–130.","chicago":"Chatterjee, Krishnendu, Marcin Jurdziński, and Thomas A Henzinger. “Quantitative Stochastic Parity Games,” 121–30. SIAM, 2004.","apa":"Chatterjee, K., Jurdziński, M., &#38; Henzinger, T. A. (2004). Quantitative stochastic parity games (pp. 121–130). Presented at the SODA: Symposium on Discrete Algorithms, SIAM.","ista":"Chatterjee K, Jurdziński M, Henzinger TA. 2004. Quantitative stochastic parity games. SODA: Symposium on Discrete Algorithms, 121–130.","ama":"Chatterjee K, Jurdziński M, Henzinger TA. Quantitative stochastic parity games. In: SIAM; 2004:121-130."}},{"publisher":"IEEE","date_updated":"2021-01-12T07:59:50Z","publication_status":"published","day":"12","quality_controlled":0,"title":"An eclipse plug-in for model checking","doi":"10.1109/WPC.2004.1311069  ","type":"conference","year":"2004","conference":{"name":"IWPC: Program Comprehension"},"date_created":"2018-12-11T12:09:34Z","citation":{"ama":"Beyer D, Henzinger TA, Jhala R, Majumdar R. An eclipse plug-in for model checking. In: IEEE; 2004:251-255. doi:<a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">10.1109/WPC.2004.1311069  </a>","apa":"Beyer, D., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). An eclipse plug-in for model checking (pp. 251–255). Presented at the IWPC: Program Comprehension, IEEE. <a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">https://doi.org/10.1109/WPC.2004.1311069  </a>","ista":"Beyer D, Henzinger TA, Jhala R, Majumdar R. 2004. An eclipse plug-in for model checking. IWPC: Program Comprehension, 251–255.","ieee":"D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “An eclipse plug-in for model checking,” presented at the IWPC: Program Comprehension, 2004, pp. 251–255.","chicago":"Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “An Eclipse Plug-in for Model Checking,” 251–55. IEEE, 2004. <a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">https://doi.org/10.1109/WPC.2004.1311069  </a>.","short":"D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, IEEE, 2004, pp. 251–255.","mla":"Beyer, Dirk, et al. <i>An Eclipse Plug-in for Model Checking</i>. IEEE, 2004, pp. 251–55, doi:<a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">10.1109/WPC.2004.1311069  </a>."},"extern":1,"month":"07","author":[{"full_name":"Beyer, Dirk","first_name":"Dirk","last_name":"Beyer"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar S"}],"acknowledgement":"This research was supported in part by the NSF grants CCR-0085949, CCR-0234690, and ITR-0326577.","_id":"4577","status":"public","date_published":"2004-07-12T00:00:00Z","publist_id":"129","abstract":[{"lang":"eng","text":"While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems - assertion checking, reachability analysis, dead code analysis, and test generation - directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code."}],"page":"251 - 255"},{"author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"last_name":"Chlipala","first_name":"Adam","full_name":"Chlipala, Adam J"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"}],"month":"08","extern":1,"alternative_title":["LNCS"],"date_created":"2018-12-11T12:09:34Z","citation":{"mla":"Beyer, Dirk, et al. <i>The BLAST Query Language for Software Verification</i>. Vol. 3148, Springer, 2004, pp. 2–18, doi:<a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">10.1007/978-3-540-27864-1_2</a>.","short":"D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Springer, 2004, pp. 2–18.","chicago":"Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “The BLAST Query Language for Software Verification,” 3148:2–18. Springer, 2004. <a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">https://doi.org/10.1007/978-3-540-27864-1_2</a>.","ieee":"D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “The BLAST query language for software verification,” presented at the SAS: Static Analysis Symposium, 2004, vol. 3148, pp. 2–18.","ista":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. The BLAST query language for software verification. SAS: Static Analysis Symposium, LNCS, vol. 3148, 2–18.","apa":"Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). The BLAST query language for software verification (Vol. 3148, pp. 2–18). Presented at the SAS: Static Analysis Symposium, Springer. <a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">https://doi.org/10.1007/978-3-540-27864-1_2</a>","ama":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. The BLAST query language for software verification. In: Vol 3148. Springer; 2004:2-18. doi:<a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">10.1007/978-3-540-27864-1_2</a>"},"page":"2 - 18","abstract":[{"lang":"eng","text":"BLAST is an automatic verification tool for checking temporal safety properties of C programs. Blast is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the Blast specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications. "}],"publist_id":"130","status":"public","date_published":"2004-08-17T00:00:00Z","_id":"4578","intvolume":"      3148","acknowledgement":"This research was supported in part by the NSF grants CCR-0085949, CCR-0234690, and ITR-0326577.","doi":"10.1007/978-3-540-27864-1_2","title":"The BLAST query language for software verification","quality_controlled":0,"day":"17","publication_status":"published","date_updated":"2021-01-12T07:59:50Z","publisher":"Springer","conference":{"name":"SAS: Static Analysis Symposium"},"year":"2004","type":"conference","volume":3148},{"publication_status":"published","day":"26","publisher":"IEEE","date_updated":"2021-01-12T07:59:52Z","title":"Generating tests from counterexamples","doi":"10.1109/ICSE.2004.1317455","quality_controlled":0,"type":"conference","conference":{"name":"ICSE: Software Engineering"},"year":"2004","extern":1,"date_created":"2018-12-11T12:09:35Z","citation":{"short":"D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, IEEE, 2004, pp. 326–335.","mla":"Beyer, Dirk, et al. <i>Generating Tests from Counterexamples</i>. IEEE, 2004, pp. 326–35, doi:<a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">10.1109/ICSE.2004.1317455</a>.","chicago":"Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Generating Tests from Counterexamples,” 326–35. IEEE, 2004. <a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">https://doi.org/10.1109/ICSE.2004.1317455</a>.","ieee":"D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “Generating tests from counterexamples,” presented at the ICSE: Software Engineering, 2004, pp. 326–335.","ista":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. Generating tests from counterexamples. ICSE: Software Engineering, 326–335.","apa":"Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). Generating tests from counterexamples (pp. 326–335). Presented at the ICSE: Software Engineering, IEEE. <a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">https://doi.org/10.1109/ICSE.2004.1317455</a>","ama":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. Generating tests from counterexamples. In: IEEE; 2004:326-335. doi:<a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">10.1109/ICSE.2004.1317455</a>"},"month":"07","author":[{"last_name":"Beyer","first_name":"Dirk","full_name":"Beyer, Dirk"},{"full_name":"Chlipala, Adam J","first_name":"Adam","last_name":"Chlipala"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"full_name":"Majumdar, Ritankar S","first_name":"Ritankar","last_name":"Majumdar"}],"_id":"4581","abstract":[{"lang":"eng","text":"We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test vector generation is fully automatic (no user intervention) and exact (no false positives)."}],"page":"326 - 335","status":"public","date_published":"2004-07-26T00:00:00Z","publist_id":"128"},{"page":"77 - 92","abstract":[{"lang":"eng","text":"Temporal logic is two-valued: a property is either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic Ctl which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. We interpret the resulting logic Dctl over transition systems, Markov chains, and Markov decision processes. We present two semantics for Dctl: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for Dctl, and we provide model-checking algorithms for both semantics."}],"publist_id":"79","status":"public","date_published":"2004-03-18T00:00:00Z","intvolume":"      2988","_id":"4629","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the ONR grant N00014-02-1-0671, and the NSF grants CCR-0132780, CCR-9988172, CCR-0225610, and CCR-0234690.","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"de Alfaro, Luca"},{"full_name":"Faella, Marco","first_name":"Marco","last_name":"Faella"},{"full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar S"},{"last_name":"Stoelinga","first_name":"Mariëlle","full_name":"Stoelinga, Mariëlle"}],"month":"03","extern":1,"alternative_title":["LNCS"],"date_created":"2018-12-11T12:09:50Z","citation":{"ama":"De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Model checking discounted temporal properties. In: Vol 2988. Springer; 2004:77-92. doi:<a href=\"https://doi.org/10.1007/978-3-540-24730-2_6\">10.1007/978-3-540-24730-2_6</a>","apa":"De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga, M. (2004). Model checking discounted temporal properties (Vol. 2988, pp. 77–92). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. <a href=\"https://doi.org/10.1007/978-3-540-24730-2_6\">https://doi.org/10.1007/978-3-540-24730-2_6</a>","ista":"De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2004. Model checking discounted temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 2988, 77–92.","ieee":"L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Model checking discounted temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2004, vol. 2988, pp. 77–92.","chicago":"De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and Mariëlle Stoelinga. “Model Checking Discounted Temporal Properties,” 2988:77–92. Springer, 2004. <a href=\"https://doi.org/10.1007/978-3-540-24730-2_6\">https://doi.org/10.1007/978-3-540-24730-2_6</a>.","short":"L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:, Springer, 2004, pp. 77–92.","mla":"De Alfaro, Luca, et al. <i>Model Checking Discounted Temporal Properties</i>. Vol. 2988, Springer, 2004, pp. 77–92, doi:<a href=\"https://doi.org/10.1007/978-3-540-24730-2_6\">10.1007/978-3-540-24730-2_6</a>."},"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"year":"2004","type":"conference","volume":2988,"doi":"10.1007/978-3-540-24730-2_6","title":"Model checking discounted temporal properties","quality_controlled":0,"day":"18","publication_status":"published","date_updated":"2021-01-12T08:00:38Z","publisher":"Springer"},{"year":"2003","type":"journal_article","volume":12,"quality_controlled":0,"doi":"10.1093/hmg/ddg359","title":"Impact of selection, mutation rate and genetic drift on human genetic variation","date_updated":"2021-01-12T08:19:29Z","publisher":"Oxford University Press","day":"15","publication_status":"published","publication":"Human Molecular Genetics","issue":"24","publist_id":"6803","date_published":"2003-12-15T00:00:00Z","status":"public","page":"3325 - 3330","abstract":[{"lang":"eng","text":"The accumulation of genome-wide information on single nucleotide polymorphisms in humans provides an unprecedented opportunity to detect the evolutionary forces responsible for heterogeneity of the level of genetic variability across loci. Previous studies have shown that history of recombination events has produced long haplotype blocks in the human genome, which contribute to this heterogeneity. Other factors, however, such as natural selection or the heterogeneity of mutation rates across loci, may also lead to heterogeneity of genetic variability. We compared synonymous and non-synonymous variability within human genes with their divergence from murine orthologs. We separately analyzed the non-synonymous variants predicted to damage protein structure or function and the variants predicted to be functionally benign. The predictions were based on comparative sequence analysis and, in some cases, on the analysis of protein structure. A strong correlation between non-synonymous, benign variability and non-synonymous human-mouse divergence suggests that selection played an important role in shaping the pattern of variability in coding regions of human genes. However, the lack of correlation between deleterious variability and evolutionary divergence shows that a substantial proportion of the observed non-synonymous single-nucleotide polymorphisms reduces fitness and never reaches fixation. Evolutionary and medical implications of the impact of selection on human polymorphisms are discussed."}],"_id":"847","intvolume":"        12","acknowledgement":"We are grateful to Alexey Kondrashov and Alison Wellman for the careful reading of the manuscript and providing us with their valuable comments.","author":[{"full_name":"Sunyaev, Shamil R","first_name":"Shamil","last_name":"Sunyaev"},{"orcid":"0000-0001-8243-4694","full_name":"Fyodor Kondrashov","last_name":"Kondrashov","first_name":"Fyodor","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Bork, Peer","first_name":"Peer","last_name":"Bork"},{"full_name":"Ramensky, Vasily","first_name":"Vasily","last_name":"Ramensky"}],"month":"12","citation":{"ama":"Sunyaev S, Kondrashov F, Bork P, Ramensky V. Impact of selection, mutation rate and genetic drift on human genetic variation. <i>Human Molecular Genetics</i>. 2003;12(24):3325-3330. doi:<a href=\"https://doi.org/10.1093/hmg/ddg359\">10.1093/hmg/ddg359</a>","ista":"Sunyaev S, Kondrashov F, Bork P, Ramensky V. 2003. Impact of selection, mutation rate and genetic drift on human genetic variation. Human Molecular Genetics. 12(24), 3325–3330.","apa":"Sunyaev, S., Kondrashov, F., Bork, P., &#38; Ramensky, V. (2003). Impact of selection, mutation rate and genetic drift on human genetic variation. <i>Human Molecular Genetics</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/hmg/ddg359\">https://doi.org/10.1093/hmg/ddg359</a>","chicago":"Sunyaev, Shamil, Fyodor Kondrashov, Peer Bork, and Vasily Ramensky. “Impact of Selection, Mutation Rate and Genetic Drift on Human Genetic Variation.” <i>Human Molecular Genetics</i>. Oxford University Press, 2003. <a href=\"https://doi.org/10.1093/hmg/ddg359\">https://doi.org/10.1093/hmg/ddg359</a>.","ieee":"S. Sunyaev, F. Kondrashov, P. Bork, and V. Ramensky, “Impact of selection, mutation rate and genetic drift on human genetic variation,” <i>Human Molecular Genetics</i>, vol. 12, no. 24. Oxford University Press, pp. 3325–3330, 2003.","mla":"Sunyaev, Shamil, et al. “Impact of Selection, Mutation Rate and Genetic Drift on Human Genetic Variation.” <i>Human Molecular Genetics</i>, vol. 12, no. 24, Oxford University Press, 2003, pp. 3325–30, doi:<a href=\"https://doi.org/10.1093/hmg/ddg359\">10.1093/hmg/ddg359</a>.","short":"S. Sunyaev, F. Kondrashov, P. Bork, V. Ramensky, Human Molecular Genetics 12 (2003) 3325–3330."},"date_created":"2018-12-11T11:48:49Z","extern":1},{"author":[{"full_name":"Kaloshin, Vadim","orcid":"0000-0002-6051-2628","last_name":"Kaloshin","first_name":"Vadim","id":"FE553552-CDE8-11E9-B324-C0EBE5697425"}],"oa_version":"None","month":"03","extern":"1","article_type":"original","citation":{"chicago":"Kaloshin, Vadim. “The Existential Hilbert 16-Th Problem and an Estimate for Cyclicity of Elementary Polycycles.” <i>Inventiones Mathematicae</i>. Springer Nature, 2003. <a href=\"https://doi.org/10.1007/s00222-002-0244-9\">https://doi.org/10.1007/s00222-002-0244-9</a>.","ieee":"V. Kaloshin, “The existential Hilbert 16-th problem and an estimate for cyclicity of elementary polycycles,” <i>Inventiones mathematicae</i>, vol. 151, no. 3. Springer Nature, pp. 451–512, 2003.","mla":"Kaloshin, Vadim. “The Existential Hilbert 16-Th Problem and an Estimate for Cyclicity of Elementary Polycycles.” <i>Inventiones Mathematicae</i>, vol. 151, no. 3, Springer Nature, 2003, pp. 451–512, doi:<a href=\"https://doi.org/10.1007/s00222-002-0244-9\">10.1007/s00222-002-0244-9</a>.","short":"V. Kaloshin, Inventiones Mathematicae 151 (2003) 451–512.","ama":"Kaloshin V. The existential Hilbert 16-th problem and an estimate for cyclicity of elementary polycycles. <i>Inventiones mathematicae</i>. 2003;151(3):451-512. doi:<a href=\"https://doi.org/10.1007/s00222-002-0244-9\">10.1007/s00222-002-0244-9</a>","ista":"Kaloshin V. 2003. The existential Hilbert 16-th problem and an estimate for cyclicity of elementary polycycles. Inventiones mathematicae. 151(3), 451–512.","apa":"Kaloshin, V. (2003). The existential Hilbert 16-th problem and an estimate for cyclicity of elementary polycycles. <i>Inventiones Mathematicae</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00222-002-0244-9\">https://doi.org/10.1007/s00222-002-0244-9</a>"},"keyword":["General Mathematics"],"date_created":"2020-09-18T10:49:26Z","page":"451-512","publication":"Inventiones mathematicae","issue":"3","status":"public","date_published":"2003-03-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"8519","intvolume":"       151","language":[{"iso":"eng"}],"doi":"10.1007/s00222-002-0244-9","title":"The existential Hilbert 16-th problem and an estimate for cyclicity of elementary polycycles","quality_controlled":"1","day":"01","publication_status":"published","publication_identifier":{"issn":["0020-9910","1432-1297"]},"date_updated":"2021-01-12T08:19:50Z","publisher":"Springer Nature","year":"2003","type":"journal_article","volume":151,"article_processing_charge":"No"},{"year":"2003","type":"journal_article","volume":19,"quality_controlled":0,"doi":"10.1016/S0168-9525(02)00029-X","title":"Evolution of alternative splicing: Deletions, insertions and origin of functional parts of proteins from intron sequences","date_updated":"2021-01-12T08:20:58Z","publisher":"Elsevier","day":"01","publication_status":"published","issue":"3","publist_id":"6776","publication":"Trends in Genetics","date_published":"2003-01-01T00:00:00Z","status":"public","page":"115 - 119","abstract":[{"lang":"eng","text":"Alternative splicing is thought to be a major source of functional diversity in animal proteins. We analyzed the evolutionary conservation of proteins encoded by alternatively spliced genes and predicted the ancestral state for 73 cases of alternative splicing (25 insertions and 48 deletions). The amino acid sequences of most of the inserts in proteins produced by alternative splicing are as conserved as the surrounding sequences. Thus, alternative splicing often creates novel isoforms by the insertion of new, functional protein sequences that probably originated from noncoding sequences of introns."}],"intvolume":"        19","_id":"876","acknowledgement":"We thank Peer Bork, Mikhail Gelfand, Alexey Kondrashov, David Lipman and Shamil Sunyaev for critical reading of the manuscript and useful suggestions and the Koonin group members for helpful discussions.","author":[{"id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","last_name":"Kondrashov","first_name":"Fyodor","full_name":"Fyodor Kondrashov","orcid":"0000-0001-8243-4694"},{"first_name":"Eugene","last_name":"Koonin","full_name":"Koonin, Eugene V"}],"month":"01","date_created":"2018-12-11T11:48:58Z","citation":{"ama":"Kondrashov F, Koonin E. Evolution of alternative splicing: Deletions, insertions and origin of functional parts of proteins from intron sequences. <i>Trends in Genetics</i>. 2003;19(3):115-119. doi:<a href=\"https://doi.org/10.1016/S0168-9525(02)00029-X\">10.1016/S0168-9525(02)00029-X</a>","ista":"Kondrashov F, Koonin E. 2003. Evolution of alternative splicing: Deletions, insertions and origin of functional parts of proteins from intron sequences. Trends in Genetics. 19(3), 115–119.","apa":"Kondrashov, F., &#38; Koonin, E. (2003). Evolution of alternative splicing: Deletions, insertions and origin of functional parts of proteins from intron sequences. <i>Trends in Genetics</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0168-9525(02)00029-X\">https://doi.org/10.1016/S0168-9525(02)00029-X</a>","chicago":"Kondrashov, Fyodor, and Eugene Koonin. “Evolution of Alternative Splicing: Deletions, Insertions and Origin of Functional Parts of Proteins from Intron Sequences.” <i>Trends in Genetics</i>. Elsevier, 2003. <a href=\"https://doi.org/10.1016/S0168-9525(02)00029-X\">https://doi.org/10.1016/S0168-9525(02)00029-X</a>.","ieee":"F. Kondrashov and E. Koonin, “Evolution of alternative splicing: Deletions, insertions and origin of functional parts of proteins from intron sequences,” <i>Trends in Genetics</i>, vol. 19, no. 3. Elsevier, pp. 115–119, 2003.","mla":"Kondrashov, Fyodor, and Eugene Koonin. “Evolution of Alternative Splicing: Deletions, Insertions and Origin of Functional Parts of Proteins from Intron Sequences.” <i>Trends in Genetics</i>, vol. 19, no. 3, Elsevier, 2003, pp. 115–19, doi:<a href=\"https://doi.org/10.1016/S0168-9525(02)00029-X\">10.1016/S0168-9525(02)00029-X</a>.","short":"F. Kondrashov, E. Koonin, Trends in Genetics 19 (2003) 115–119."},"extern":1},{"type":"journal_article","volume":360,"oa":1,"year":"2003","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1311.1665"}],"day":"01","publication_status":"published","date_updated":"2021-01-12T06:52:20Z","publisher":"Mathematisches Institut der Universität Bonn","title":"Counting rational points on del Pezzo surfaces of degree 5","external_id":{"arxiv":["1311.1665"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"166","intvolume":"       360","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"For any number field k, upper bounds are established for the number of k-rational points of bounded height on non-singular del Pezzo surfaces defined over k, which are equipped with suitable conic bundle structures over k."}],"publist_id":"7755","publication":"Proceedings of the Bonn session in analytic number theory and diophantine equations","status":"public","date_published":"2003-01-01T00:00:00Z","extern":"1","alternative_title":["Bonner mathematische Schriften"],"citation":{"apa":"Browning, T. D., &#38; Swarbick Jones, M. (2003). Counting rational points on del Pezzo surfaces of degree 5. <i>Proceedings of the Bonn Session in Analytic Number Theory and Diophantine Equations</i>. Mathematisches Institut der Universität Bonn.","ista":"Browning TD, Swarbick Jones M. 2003. Counting rational points on del Pezzo surfaces of degree 5. Proceedings of the Bonn session in analytic number theory and diophantine equations. 360.","ama":"Browning TD, Swarbick Jones M. Counting rational points on del Pezzo surfaces of degree 5. <i>Proceedings of the Bonn session in analytic number theory and diophantine equations</i>. 2003;360.","mla":"Browning, Timothy D., and M. Swarbick Jones. “Counting Rational Points on Del Pezzo Surfaces of Degree 5.” <i>Proceedings of the Bonn Session in Analytic Number Theory and Diophantine Equations</i>, vol. 360, Mathematisches Institut der Universität Bonn, 2003.","short":"T.D. Browning, M. Swarbick Jones, Proceedings of the Bonn Session in Analytic Number Theory and Diophantine Equations 360 (2003).","ieee":"T. D. Browning and M. Swarbick Jones, “Counting rational points on del Pezzo surfaces of degree 5,” <i>Proceedings of the Bonn session in analytic number theory and diophantine equations</i>, vol. 360. Mathematisches Institut der Universität Bonn, 2003.","chicago":"Browning, Timothy D, and M Swarbick Jones. “Counting Rational Points on Del Pezzo Surfaces of Degree 5.” <i>Proceedings of the Bonn Session in Analytic Number Theory and Diophantine Equations</i>. Mathematisches Institut der Universität Bonn, 2003."},"arxiv":1,"date_created":"2018-12-11T11:44:58Z","oa_version":"None","author":[{"full_name":"Browning, Timothy D","orcid":"0000-0002-8314-0177","last_name":"Browning","first_name":"Timothy D","id":"35827D50-F248-11E8-B48F-1D18A9856A87"},{"first_name":"M","last_name":"Swarbick Jones","full_name":"Swarbick Jones, M"}],"month":"01"},{"quality_controlled":0,"title":"The location of NuoL and NuoM subunits in the membrane domain of the Escherichia coli Complex I: implications for the mechanism of proton pumping","doi":"10.1074/jbc.M308247200","publisher":"American Society for Biochemistry and Molecular Biology","date_updated":"2021-01-12T06:54:21Z","publication_status":"published","day":"31","year":"2003","volume":278,"type":"journal_article","month":"10","author":[{"full_name":"Holt, Peter J","last_name":"Holt","first_name":"Peter"},{"full_name":"Morgan, David J","last_name":"Morgan","first_name":"David"},{"orcid":"0000-0002-0977-7989","full_name":"Leonid Sazanov","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","first_name":"Leonid A","last_name":"Sazanov"}],"citation":{"short":"P. Holt, D. Morgan, L.A. Sazanov, Journal of Biological Chemistry 278 (2003) 43114–43120.","mla":"Holt, Peter, et al. “The Location of NuoL and NuoM Subunits in the Membrane Domain of the Escherichia Coli Complex I: Implications for the Mechanism of Proton Pumping.” <i>Journal of Biological Chemistry</i>, vol. 278, no. 44, American Society for Biochemistry and Molecular Biology, 2003, pp. 43114–20, doi:<a href=\"https://doi.org/10.1074/jbc.M308247200\">10.1074/jbc.M308247200</a>.","ieee":"P. Holt, D. Morgan, and L. A. Sazanov, “The location of NuoL and NuoM subunits in the membrane domain of the Escherichia coli Complex I: implications for the mechanism of proton pumping,” <i>Journal of Biological Chemistry</i>, vol. 278, no. 44. American Society for Biochemistry and Molecular Biology, pp. 43114–43120, 2003.","chicago":"Holt, Peter, David Morgan, and Leonid A Sazanov. “The Location of NuoL and NuoM Subunits in the Membrane Domain of the Escherichia Coli Complex I: Implications for the Mechanism of Proton Pumping.” <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology, 2003. <a href=\"https://doi.org/10.1074/jbc.M308247200\">https://doi.org/10.1074/jbc.M308247200</a>.","apa":"Holt, P., Morgan, D., &#38; Sazanov, L. A. (2003). The location of NuoL and NuoM subunits in the membrane domain of the Escherichia coli Complex I: implications for the mechanism of proton pumping. <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology. <a href=\"https://doi.org/10.1074/jbc.M308247200\">https://doi.org/10.1074/jbc.M308247200</a>","ista":"Holt P, Morgan D, Sazanov LA. 2003. The location of NuoL and NuoM subunits in the membrane domain of the Escherichia coli Complex I: implications for the mechanism of proton pumping. Journal of Biological Chemistry. 278(44), 43114–43120.","ama":"Holt P, Morgan D, Sazanov LA. The location of NuoL and NuoM subunits in the membrane domain of the Escherichia coli Complex I: implications for the mechanism of proton pumping. <i>Journal of Biological Chemistry</i>. 2003;278(44):43114-43120. doi:<a href=\"https://doi.org/10.1074/jbc.M308247200\">10.1074/jbc.M308247200</a>"},"date_created":"2018-12-11T11:54:55Z","extern":1,"status":"public","date_published":"2003-10-31T00:00:00Z","publication":"Journal of Biological Chemistry","publist_id":"5124","issue":"44","abstract":[{"lang":"eng","text":"The molecular organization of bacterial NADH: ubiquinone oxidoreductase (complex I or NDH-1) is not established, apart from a rough separation into dehydrogenase, connecting and membrane domains. In this work, complex I was purified from Escherichia coli and fragmented by replacing dodecylmaltoside with other detergents. Exchange into decyl maltoside led to the removal of the hydrophobic subunit NuoL from the otherwise intact complex. Diheptanoyl phosphocholine led to the loss of NuoL and NuoM subunits, whereas other subunits remained in the complex. The presence of N,N-dimethyldodecylamine N-oxide or Triton X-100 led to further disruption of the membrane domain into fragments containing NuoL/M/N, NuoA/K/N, and NuoH/J subunits. Among the hydrophilic subunits, NuoCD was most readily dissociated from the complex, whereas NuoB was partially dissociated from the peripheral arm assembly in N,N-dimethyldodecylamine N-oxide. A model of subunit arrangement in bacterial complex I based on these data is proposed. Subunits NuoL and NuoM, which are homologous to antiporters and are implicated in proton pumping, are located at the distal end of the membrane arm, spatially separated from the redox centers of the peripheral arm. This is consistent with proposals that the mechanism of proton pumping by complex I is likely to involve long range conformational changes."}],"page":"43114 - 43120","acknowledgement":"his work was supported by the Medical Research Council.","_id":"1959","intvolume":"       278"},{"page":"19483 - 19491","abstract":[{"text":"NADH-ubiquinone oxidoreductase (complex I or NDH-1) was purified from the BL21 strain of Escherichia coli using an improved procedure. The complex was effectively stabilized by addition of divalent cations and lipids, making the preparation suitable for structural studies. The ubiquinone reductase activity of the enzyme was fully restored by addition of native E. coli lipids. Two different two-dimensional crystal forms, with p2 and p3 symmetry, were obtained using lipids containing native E. coli extracts. Analysis of the crystals showed that they are formed by fully intact complex I in an L-shaped conformation. Activity assays and single particle analysis indicated that complex I maintains this structure in detergent solution and does not adopt a different conformation in the active state. Thus, we provide the first experimental evidence that complex I from E. coli has an L-shape in a lipid bilayer and confirm that this is also the case for the active enzyme in solution. This suggests strongly that bacterial complex I exists in an L-shaped conformation in vivo. Our results also indicate that native lipids play an important role in the activation, stabilization and, as a consequence, crystallization of purified complex I from E. coli.","lang":"eng"}],"publication":"Journal of Biological Chemistry","issue":"21","publist_id":"5125","status":"public","date_published":"2003-05-23T00:00:00Z","intvolume":"       278","_id":"1960","author":[{"id":"338D39FE-F248-11E8-B48F-1D18A9856A87","last_name":"Sazanov","first_name":"Leonid A","orcid":"0000-0002-0977-7989","full_name":"Leonid Sazanov"},{"full_name":"Carroll, Joe D","last_name":"Carroll","first_name":"Joe"},{"full_name":"Holt, Peter J","last_name":"Holt","first_name":"Peter"},{"full_name":"Toime, Laurence J","first_name":"Laurence","last_name":"Toime"},{"full_name":"Fearnley, Ian M","first_name":"Ian","last_name":"Fearnley"}],"month":"05","extern":1,"date_created":"2018-12-11T11:54:55Z","citation":{"ieee":"L. A. Sazanov, J. Carroll, P. Holt, L. Toime, and I. Fearnley, “A role for native lipids in the stabilization and two dimensional crystallization of the Escherichia coli NADH ubiquinone oxidoreductase (complex I),” <i>Journal of Biological Chemistry</i>, vol. 278, no. 21. American Society for Biochemistry and Molecular Biology, pp. 19483–19491, 2003.","chicago":"Sazanov, Leonid A, Joe Carroll, Peter Holt, Laurence Toime, and Ian Fearnley. “A Role for Native Lipids in the Stabilization and Two Dimensional Crystallization of the Escherichia Coli NADH Ubiquinone Oxidoreductase (Complex I).” <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology, 2003. <a href=\"https://doi.org/10.1074/jbc.M208959200\">https://doi.org/10.1074/jbc.M208959200</a>.","mla":"Sazanov, Leonid A., et al. “A Role for Native Lipids in the Stabilization and Two Dimensional Crystallization of the Escherichia Coli NADH Ubiquinone Oxidoreductase (Complex I).” <i>Journal of Biological Chemistry</i>, vol. 278, no. 21, American Society for Biochemistry and Molecular Biology, 2003, pp. 19483–91, doi:<a href=\"https://doi.org/10.1074/jbc.M208959200\">10.1074/jbc.M208959200</a>.","short":"L.A. Sazanov, J. Carroll, P. Holt, L. Toime, I. Fearnley, Journal of Biological Chemistry 278 (2003) 19483–19491.","ama":"Sazanov LA, Carroll J, Holt P, Toime L, Fearnley I. A role for native lipids in the stabilization and two dimensional crystallization of the Escherichia coli NADH ubiquinone oxidoreductase (complex I). <i>Journal of Biological Chemistry</i>. 2003;278(21):19483-19491. doi:<a href=\"https://doi.org/10.1074/jbc.M208959200\">10.1074/jbc.M208959200</a>","apa":"Sazanov, L. A., Carroll, J., Holt, P., Toime, L., &#38; Fearnley, I. (2003). A role for native lipids in the stabilization and two dimensional crystallization of the Escherichia coli NADH ubiquinone oxidoreductase (complex I). <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology. <a href=\"https://doi.org/10.1074/jbc.M208959200\">https://doi.org/10.1074/jbc.M208959200</a>","ista":"Sazanov LA, Carroll J, Holt P, Toime L, Fearnley I. 2003. A role for native lipids in the stabilization and two dimensional crystallization of the Escherichia coli NADH ubiquinone oxidoreductase (complex I). Journal of Biological Chemistry. 278(21), 19483–19491."},"year":"2003","type":"journal_article","volume":278,"doi":"10.1074/jbc.M208959200","title":"A role for native lipids in the stabilization and two dimensional crystallization of the Escherichia coli NADH ubiquinone oxidoreductase (complex I)","quality_controlled":0,"day":"23","publication_status":"published","date_updated":"2021-01-12T06:54:21Z","publisher":"American Society for Biochemistry and Molecular Biology"},{"year":"2003","volume":108,"type":"journal_article","title":"Counting rational points on cubic and quartic surfaces","doi":"10.4064/aa108-3-7","quality_controlled":0,"publication_status":"published","day":"01","publisher":"Instytut Matematyczny","date_updated":"2021-01-12T06:54:58Z","page":"275 - 295","status":"public","date_published":"2003-01-01T00:00:00Z","publication":"Acta Arithmetica","issue":"3","publist_id":"7707","_id":"205","intvolume":"       108","month":"01","author":[{"full_name":"Timothy Browning","orcid":"0000-0002-8314-0177","first_name":"Timothy D","last_name":"Browning","id":"35827D50-F248-11E8-B48F-1D18A9856A87"}],"extern":1,"citation":{"apa":"Browning, T. D. (2003). Counting rational points on cubic and quartic surfaces. <i>Acta Arithmetica</i>. Instytut Matematyczny. <a href=\"https://doi.org/10.4064/aa108-3-7\">https://doi.org/10.4064/aa108-3-7</a>","ista":"Browning TD. 2003. Counting rational points on cubic and quartic surfaces. Acta Arithmetica. 108(3), 275–295.","ama":"Browning TD. Counting rational points on cubic and quartic surfaces. <i>Acta Arithmetica</i>. 2003;108(3):275-295. doi:<a href=\"https://doi.org/10.4064/aa108-3-7\">10.4064/aa108-3-7</a>","mla":"Browning, Timothy D. “Counting Rational Points on Cubic and Quartic Surfaces.” <i>Acta Arithmetica</i>, vol. 108, no. 3, Instytut Matematyczny, 2003, pp. 275–95, doi:<a href=\"https://doi.org/10.4064/aa108-3-7\">10.4064/aa108-3-7</a>.","short":"T.D. Browning, Acta Arithmetica 108 (2003) 275–295.","ieee":"T. D. Browning, “Counting rational points on cubic and quartic surfaces,” <i>Acta Arithmetica</i>, vol. 108, no. 3. Instytut Matematyczny, pp. 275–295, 2003.","chicago":"Browning, Timothy D. “Counting Rational Points on Cubic and Quartic Surfaces.” <i>Acta Arithmetica</i>. Instytut Matematyczny, 2003. <a href=\"https://doi.org/10.4064/aa108-3-7\">https://doi.org/10.4064/aa108-3-7</a>."},"date_created":"2018-12-11T11:45:12Z"},{"author":[{"full_name":"Timothy Browning","orcid":"0000-0002-8314-0177","first_name":"Timothy D","last_name":"Browning","id":"35827D50-F248-11E8-B48F-1D18A9856A87"}],"month":"03","citation":{"ama":"Browning TD. A note on the distribution of rational points on threefolds. <i>Quarterly Journal of Mathematics</i>. 2003;54(1):33-39. doi:<a href=\"https://doi.org/10.1093/qjmath/54.1.33\">10.1093/qjmath/54.1.33</a>","apa":"Browning, T. D. (2003). A note on the distribution of rational points on threefolds. <i>Quarterly Journal of Mathematics</i>. Unknown. <a href=\"https://doi.org/10.1093/qjmath/54.1.33\">https://doi.org/10.1093/qjmath/54.1.33</a>","ista":"Browning TD. 2003. A note on the distribution of rational points on threefolds. Quarterly Journal of Mathematics. 54(1), 33–39.","ieee":"T. D. Browning, “A note on the distribution of rational points on threefolds,” <i>Quarterly Journal of Mathematics</i>, vol. 54, no. 1. Unknown, pp. 33–39, 2003.","chicago":"Browning, Timothy D. “A Note on the Distribution of Rational Points on Threefolds.” <i>Quarterly Journal of Mathematics</i>. Unknown, 2003. <a href=\"https://doi.org/10.1093/qjmath/54.1.33\">https://doi.org/10.1093/qjmath/54.1.33</a>.","mla":"Browning, Timothy D. “A Note on the Distribution of Rational Points on Threefolds.” <i>Quarterly Journal of Mathematics</i>, vol. 54, no. 1, Unknown, 2003, pp. 33–39, doi:<a href=\"https://doi.org/10.1093/qjmath/54.1.33\">10.1093/qjmath/54.1.33</a>.","short":"T.D. Browning, Quarterly Journal of Mathematics 54 (2003) 33–39."},"date_created":"2018-12-11T11:45:12Z","extern":1,"issue":"1","publication":"Quarterly Journal of Mathematics","publist_id":"7706","date_published":"2003-03-01T00:00:00Z","status":"public","page":"33 - 39","abstract":[{"lang":"eng","text":"Let T ⊂ ℙ 4 be a non-singular threefold of degree at least four. Then we show that the number of points in T(ℚ), with height at most B, is o(B 3) or B → ∞."}],"intvolume":"        54","_id":"206","quality_controlled":0,"doi":"10.1093/qjmath/54.1.33","title":"A note on the distribution of rational points on threefolds","date_updated":"2021-01-12T06:55:02Z","publisher":"Unknown","day":"01","publication_status":"published","year":"2003","type":"journal_article","volume":54}]