[{"publisher":"ACM","quality_controlled":0,"month":"09","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"}],"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.","page":"104 - 113","date_published":"2004-09-01T00:00:00Z","doi":"10.1145/1017753.1017774","date_created":"2018-12-11T12:08:53Z","year":"2004","publication_status":"published","day":"01","type":"conference","conference":{"name":"EMSOFT: Embedded Software "},"status":"public","_id":"4445","author":[{"last_name":"Henzinger","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Christoph","full_name":"Kirsch, Christoph M","last_name":"Kirsch"}],"publist_id":"285","title":"A typed assembly language for real-time programs","citation":{"ista":"Henzinger TA, Kirsch C. 2004. A typed assembly language for real-time programs. EMSOFT: Embedded Software , 104–113.","chicago":"Henzinger, Thomas A, and Christoph Kirsch. “A Typed Assembly Language for Real-Time Programs,” 104–13. ACM, 2004. https://doi.org/10.1145/1017753.1017774.","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.","ama":"Henzinger TA, Kirsch C. A typed assembly language for real-time programs. In: ACM; 2004:104-113. doi:10.1145/1017753.1017774","apa":"Henzinger, T. A., & Kirsch, C. (2004). A typed assembly language for real-time programs (pp. 104–113). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1017753.1017774","mla":"Henzinger, Thomas A., and Christoph Kirsch. A Typed Assembly Language for Real-Time Programs. ACM, 2004, pp. 104–13, doi:10.1145/1017753.1017774."},"date_updated":"2021-01-12T07:57:01Z","extern":1},{"status":"public","type":"conference","conference":{"name":"POPL: Principles of Programming Languages"},"_id":"4458","title":"Abstractions from proofs","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ranjit","full_name":"Jhala, Ranjit","last_name":"Jhala"},{"full_name":"Majumdar, Ritankar S","last_name":"Majumdar","first_name":"Ritankar"},{"first_name":"Kenneth","last_name":"Mcmillan","full_name":"McMillan, Kenneth L"}],"publist_id":"270","extern":1,"citation":{"chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan. “Abstractions from Proofs,” 232–44. ACM, 2004. https://doi.org/10.1145/964001.964021.","ista":"Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs. POPL: Principles of Programming Languages, 232–244.","mla":"Henzinger, Thomas A., et al. Abstractions from Proofs. ACM, 2004, pp. 232–44, doi:10.1145/964001.964021.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, ACM, 2004, pp. 232–244.","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.","ama":"Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In: ACM; 2004:232-244. doi:10.1145/964001.964021","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., & Mcmillan, K. (2004). Abstractions from proofs (pp. 232–244). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/10.1145/964001.964021"},"date_updated":"2021-01-12T07:57:06Z","month":"04","quality_controlled":0,"publisher":"ACM","abstract":[{"lang":"eng","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."}],"doi":"10.1145/964001.964021","date_published":"2004-04-01T00:00:00Z","date_created":"2018-12-11T12:08:57Z","page":"232 - 244","day":"01","year":"2004","publication_status":"published"},{"alternative_title":["LNCS"],"publisher":"Springer","quality_controlled":0,"intvolume":" 2772","month":"02","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"}],"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. ","page":"332 - 358","date_created":"2018-12-11T12:08:58Z","date_published":"2004-02-24T00:00:00Z","doi":"10.1007/978-3-540-39910-0_16","volume":2772,"year":"2004","publication_status":"published","publication":"Verification: Theory and Practice","day":"24","type":"book_chapter","status":"public","_id":"4461","publist_id":"269","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Jhala","full_name":"Jhala, Ranjit","first_name":"Ranjit"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"first_name":"Marco","last_name":"Sanvido","full_name":"Sanvido, Marco A"}],"title":"Extreme model checking","date_updated":"2021-01-12T07:57:08Z","citation":{"short":"T.A. Henzinger, R. Jhala, R. Majumdar, M. Sanvido, in:, Verification: Theory and Practice, Springer, 2004, pp. 332–358.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and M. Sanvido, “Extreme model checking,” in Verification: Theory and Practice, vol. 2772, Springer, 2004, pp. 332–358.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., & Sanvido, M. (2004). Extreme model checking. In Verification: Theory and Practice (Vol. 2772, pp. 332–358). Springer. https://doi.org/10.1007/978-3-540-39910-0_16","ama":"Henzinger TA, Jhala R, Majumdar R, Sanvido M. Extreme model checking. In: Verification: Theory and Practice. Vol 2772. Springer; 2004:332-358. doi:10.1007/978-3-540-39910-0_16","mla":"Henzinger, Thomas A., et al. “Extreme Model Checking.” Verification: Theory and Practice, vol. 2772, Springer, 2004, pp. 332–58, doi:10.1007/978-3-540-39910-0_16.","ista":"Henzinger TA, Jhala R, Majumdar R, Sanvido M. 2004.Extreme model checking. In: Verification: Theory and Practice. LNCS, vol. 2772, 332–358.","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Marco Sanvido. “Extreme Model Checking.” In Verification: Theory and Practice, 2772:332–58. Springer, 2004. https://doi.org/10.1007/978-3-540-39910-0_16."},"extern":1},{"date_published":"2004-06-01T00:00:00Z","doi":"10.1145/996841.996844","date_created":"2018-12-11T12:08:57Z","page":"1 - 13","day":"01","publication_status":"published","year":"2004","month":"06","publisher":"ACM","quality_controlled":0,"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."}],"title":"Race checking by context inference","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"},{"full_name":"Majumdar, Ritankar S","last_name":"Majumdar","first_name":"Ritankar"}],"publist_id":"271","extern":1,"date_updated":"2021-01-12T07:57:07Z","citation":{"mla":"Henzinger, Thomas A., et al. Race Checking by Context Inference. ACM, 2004, pp. 1–13, doi:10.1145/996841.996844.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2004, pp. 1–13.","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.","ama":"Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In: ACM; 2004:1-13. doi:10.1145/996841.996844","apa":"Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). Race checking by context inference (pp. 1–13). Presented at the PLDI: Programming Languages Design and Implementation, ACM. https://doi.org/10.1145/996841.996844","chicago":"Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking by Context Inference,” 1–13. ACM, 2004. https://doi.org/10.1145/996841.996844.","ista":"Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference. PLDI: Programming Languages Design and Implementation, 1–13."},"status":"public","type":"conference","conference":{"name":"PLDI: Programming Languages Design and Implementation"},"_id":"4459"},{"day":"12","year":"2004","publication_status":"published","doi":"10.1007/978-3-540-24743-2_24","volume":2993,"date_published":"2004-03-12T00:00:00Z","date_created":"2018-12-11T12:09:18Z","page":"167 - 170","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.","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"}],"month":"03","intvolume":" 2993","publisher":"Springer","quality_controlled":0,"alternative_title":["LNCS"],"extern":1,"citation":{"mla":"Ghosal, Arkadeb, et al. Event-Driven Programming with Logical Execution Times. Vol. 2993, Springer, 2004, pp. 167–70, doi:10.1007/978-3-540-24743-2_24.","apa":"Ghosal, A., Henzinger, T. A., Kirsch, C., & 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. https://doi.org/10.1007/978-3-540-24743-2_24","ama":"Ghosal A, Henzinger TA, Kirsch C, Sanvido M. Event-driven programming with logical execution times. In: Vol 2993. Springer; 2004:167-170. doi:10.1007/978-3-540-24743-2_24","short":"A. Ghosal, T.A. Henzinger, C. Kirsch, M. Sanvido, in:, Springer, 2004, pp. 167–170.","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.","chicago":"Ghosal, Arkadeb, Thomas A Henzinger, Christoph Kirsch, and Marco Sanvido. “Event-Driven Programming with Logical Execution Times,” 2993:167–70. Springer, 2004. https://doi.org/10.1007/978-3-540-24743-2_24.","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."},"date_updated":"2021-01-12T07:59:26Z","title":"Event-driven programming with logical execution times","author":[{"last_name":"Ghosal","full_name":"Ghosal, Arkadeb","first_name":"Arkadeb"},{"full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Kirsch","full_name":"Kirsch, Christoph M","first_name":"Christoph"},{"first_name":"Marco","last_name":"Sanvido","full_name":"Sanvido, Marco A"}],"publist_id":"200","_id":"4525","status":"public","type":"conference","conference":{"name":"HSCC: Hybrid Systems - Computation and Control"}}]