hh.sePublications
Change search
Refine search result
12 1 - 50 of 92
Cite
Citation style
• apa
• harvard1
• ieee
• modern-language-association-8th-edition
• vancouver
• Other style
More styles
Language
• de-DE
• en-GB
• en-US
• fi-FI
• nn-NO
• nn-NB
• sv-SE
• Other locale
More languages
Output format
• html
• text
• asciidoc
• rtf
Rows per page
• 5
• 10
• 20
• 50
• 100
• 250
Sort
• Standard (Relevance)
• Author A-Ö
• Author Ö-A
• Title A-Ö
• Title Ö-A
• Publication type A-Ö
• Publication type Ö-A
• Issued (Oldest first)
• Created (Oldest first)
• Last updated (Oldest first)
• Disputation date (earliest first)
• Disputation date (latest first)
• Standard (Relevance)
• Author A-Ö
• Author Ö-A
• Title A-Ö
• Title Ö-A
• Publication type A-Ö
• Publication type Ö-A
• Issued (Oldest first)
• Created (Oldest first)
• Last updated (Oldest first)
• Disputation date (earliest first)
• Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
• 1.
Centre de Recherche INRIA, Rennes, France.
Rice University, Houston, Texas, United States. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Centre de Recherche INRIA, Rennes, France. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, United States.
Chattering-Free Simulation for Hybrid Dynamical Systems: Semantics and Prototype Implementation2016In: 2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES) / [ed] Randall Bilof, Los Alamitos: IEEE Computer Society, 2016, p. 412-422, article id 7982279Conference paper (Refereed)

Chattering is a fundamental phenomenon that is unique to hybrid systems, due to the complex interaction between discrete dynamics (in the form of discrete transitions) and continuous dynamics (in the form of time). In practice, simulating chattering hybrid systems is challenging in that simulation effectively halts near the chattering time point, as an infinite number of discrete transitions would need to be simulated. In this paper, formal conditions are provided for when the simulated models of hybrid systems display chattering behavior, and methods are proposed for avoiding chattering “on the fly” in runtime. We utilize dynamical behavior analysis to derive conditions for detecting chattering without enumeration of modes. We also present a new iterative algorithm to allow for solutions to be carried past the chattering point, and we show by a prototypical implementation how to generate the equivalent chattering-free dynamics internally by the simulator in the main simulation loop. The concepts are illustrated with examples throughout the paper. © 2016 IEEE.

• 2.
Kaunas University of Technology, Kaunas, Lithuania.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, TX, USA.
DSLs Should be Online Applications2014In: Joint International Conference on Engineering Education & International Conference on Information Technology: ICEE/ICIT-2014: June 2 - 6, 2014: Riga, Latvia: Conference proceedings, 2014, p. 314-319Conference paper (Refereed)

Domain-Specific Languages (DSLs) play an important role in both practice and education. But developing them is challenging, because a DSL must ultimately satisfy a large and complex set of user/customer requirements to fulfil its intended role, and neither requirements nor users are fully available at all times during the development process. Requirements can be elicited using agile methods but such methods assume the availability of the users. The situation is further complicated when the user base is primarily students and when enhanced learning is a key requirement. In this paper we propose developing DSLs, especially educational ones, as online applications. We analyze how this can help requirement elicitation and learning. Being online brings language development closer to the user, yielding new opportunities to improve and accelerate the language design process. It is also well-matched to agile methods, since web- based analytics provide an abundant source of data that integrates naturally into the development process. As an example, we consider applying the method to Acumen, a DSL designed to support teaching Cyber-Physical Systems.

• 3.
Dept. of Computer Science, University of Houston, Houston, USA.
Dept. of Computer Science, University of Houston, Houston, USA. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Release Offset Bounds for Response Time Analysis of P-FRP using Exhaustive Enumeration2011In: 2011 IEEE 10th International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom), Piscataway, N.J.: IEEE Press, 2011, p. 950-957Conference paper (Refereed)

• 4.
Department of Computer Science, University of Houston, Houston, Texas, USA.
Department of Computer Science, University of Houston, Houston, Texas, USA. Department of Computer Science, University of Houston, Houston, Texas, USA. Department of Computer Science, University of Houston, Houston, Texas, USA.
Timing Analysis of the Priority based FRP System2008In: Proceedings Work-In-Progress Session of the 14th Real-Time and Embedded Technology and Applications Symposium: 22-24 April, 2008: St. Louis, USA / [ed] Ying Lu, Lincoln, NE: University of Nebraska–Lincoln, Computer Science and Engineering , 2008, p. 89-92Conference paper (Refereed)

Kaiabachev, Taha, Zhu [1] have presented a declarative programming paradigm called Functional Reactive Programming, which is based on behaviors and events. An improved system called P-FRP uses fixed priority scheduling for tasks. The system allows for the currently executing lower priority tasks to be rolled back to restoring the original state and allowing a higher priority task to run. These aborted tasks will restart again when no tasks of higher priority are in the queue. Since P-FRP has many applications in the real time domain it is critical to understand the time bound in which the tasks which have been aborted are guaranteed to run, and if the task set is schedulable. In this paper we provide an analysis of the unique execution paradigm of the P-FRP system and study the timing bounds using different constraint variables.

1. R. Kaiabachev, W. Taha, A. Zhu, E-FRP with priorities, In the Proceedings of the 7th ACM & IEEE international conference on Embedded software, Pages: 221 - 230, 2007.

• 5.
Oregon Graduate Institute, Portland, OR, USA.
DISI, University of Genoa, Genoa, Italy. Oregon Graduate Institute, Portland, OR, USA. Oregon Graduate Institute, Portland, OR, USA.
Logical Modalities and Multi-Stage Programming1999Conference paper (Refereed)

Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. This paper makes a case for multi-stage programming with open code and closed values. We argue that a simple language exploiting interactions between two logical modalities is well suited for multi-stage programming, and report the results from our study of categorical models for multi-stage languages.

• 6.
Rice University, Houston, United States.
Halmstad University, School of Information Science, Computer and Electrical Engineering (IDE), Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Globally Parallel, Locally Sequential: A Preliminary Proposal for Acumen Objects2010In: POOSC'10, Proceedings of the 9th Workshop on Parallel/High-Performance Object-Oriented Scientific Computing, New York, NY: ACM Press, 2010Conference paper (Refereed)

An important and resource-intensive class of computation codes consists of simulators for physical systems. Today, most simulation codes are written in general-purpose imperative languages such as C or FORTRAN. Unfortunately, such languages encourage the programmer to focus her attention on details of how the computation is performed, rather than on the system being modeled.

This paper reports the design and implementation of a novel notion of an object for a physical modeling language called Acumen. A key idea underlying the language's design is encouraging a programming style that enables a "globally parallel, locally imperative" view of the world. The language is also being designed to preserve deterministic execution even when the underlying computation is performed on a highly parallel platform. Our main observation with the initial study is that extensive and continual experimental evaluation is crucial for keeping the language design process informed about bottlenecks for parallel execution.

• 7.
INRIA, Bordeaux, France.
INRIA, Bordeaux, France. Rice University, Houston, TX, United States. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, TX, United States. HVAC Consultant, Cairo, Egypt.
Preliminary results in virtual testing for smart buildings2012In: Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, ISSN 1867-8211, E-ISSN 1867-822X, Vol. 73, p. 347-349Article in journal (Refereed)

Smart buildings promise to revolutionize the way we live. Applications ranging from climate control to fire management can have significant impact on the quality and cost of these services. However, a smart building and any technology with direct effect on the safety of its occupants must undergo extensive testing. Virtual testing by means of computer simulation can significantly reduce the cost of testing and, as a result, accelerate the development of novel applications. Unfortunately, building physically-accurate simulation codes can be labor intensive. To address this problem, we propose a framework for rapid, physically-accurate virtual testing of smart building systems. The proposed framework supports analytical modeling and simulation of both a discrete distributed system as well as the physical environment that hosts it. © 2012 Springer-Verlag Berlin Heidelberg.

• 8.
INRIA Bordeaux Sud-Ouest Talence, Talence, France.
INRIA Bordeaux Sud-Ouest Talence, Talence, France. Rice University Houston, Houston, USA. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). HVAC Consultant Cairo, Cairo, Egypt.
Virtual Testing for Smart Buildings2012In: 2012 Eighth International Conference on Intelligent Environments / [ed] Randall Bilof, Piscataway, N.J.: IEEE Press, 2012, p. 282-289, article id 6258534Conference paper (Refereed)

Smart buildings promise to revolutionize the way we live. Applications ranging from climate control to fire management can have significant impact on the quality and cost of these services. However, smart buildings and any technology with direct effect on human safety and life mustundergo extensive testing. Virtual testing by means of computer simulation can significantly reduce the cost of testing and, as a result, accelerate the development of novel applications. Unfortunately, building physically-accurate simulation codes can be labor intensive.To address this problem, we propose a framework for rapid, physically-accurate virtual testing. The proposed framework supports analytical modeling of both a discrete distributed system as well as the physical environment that hosts it. The discrete models supported are accurate enough to allow the automatic generation of a dedicated programming framework that will help the developer in the implementation of these systems. The physical environment models supported are equational specifications that are accurate enough to produce running simulation codes. Combined, these two frameworks enable simulating both active systems and physical environments. These simulations can be used to monitor the behavior and gather statistics about the performance of an application in the context of precise virtual experiments. To illustrate the approach, we present models of Heating, Ventilating and Air-Conditioning (HVAC) systems. Using these models, we construct virtual experiments that illustrate how the approach can be used to optimize energy and cost of climate control for a building. © 2012 IEEE.

• 9.
INRIA, Bordeaux, France.
INRIA, Bordeaux, France. Rice University, Houston, Texas, USA. Rice University, Houston, Texas, USA. HVAC Consultant, Cairo, Egypt.
Preliminary Results in Virtual Testing for Smart Building2010In: Proceedings of MOBIQUITOUS 2010, 7th International ICST Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (2010), 2010, p. 2-Conference paper (Refereed)

Smart buildings promise to revolutionize the way we live. Applications ranging from climate control to fire management can have significant impact on the quality and cost of these services. However, a smart building and any technology with direct effect on the safety of its occupants must undergo extensive testing. Virtual testing by means of computer simulation can significantly reduce the cost of testing and, as a result, accelerate the development of novel applications. Unfortunately, building physically-accurate simulation codes can be labor intensive. To address this problem, we propose a framework for rapid, physically-accurate virtual testing of smart building systems. The proposed framework supports analytical modeling and simulation of both a discrete distributed system as well as the physical environment that hosts it.

• 10.
DISI, University of Genoa, Genoa, Italy.
DISI, University of Genoa, Genoa, Italy. Department of Computing Sciences, Chalmers, Göteborg, Sweden.
Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming2000In: Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings / [ed] Ugo Montanari, José D. P. Rolim & Emo Welzl, Heidelberg: Springer, 2000, p. 25-36Conference paper (Refereed)

Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of closed type as a simple approach to safely introducing computational effects into multi-stage languages. We demonstrate this approach formally in a core language called Mini-MLref BN. This core language combines safely multi-stage constructs and ML-style references. In addition to incorporating state, Mini-ML ref BN also embodies a number of technical improvements over previously proposed core languages for multi-stage programming.

• 11.
Imperial College London, London, United Kingdom.
DISI, University of Genoa, Genoa, Italy. Rice University, Texas, USA.
ML-like Inference for Classiﬁers2004In: Programming Languages and Systems: 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings / [ed] David Schmidt, Heidelberg: Springer Berlin/Heidelberg, 2004, Vol. 2986, p. 79-93Conference paper (Refereed)

Environment classifiers were proposed as a new approach to typing multi-stage languages. Safety was established in the simply-typed and let-polymorphic settings. While the motivation for classifiers was the feasibility of inference, this was in fact not established. This paper starts with the observation that inference for the full classifier-based system fails. We then identify a subset of the original system for which inference is possible. This subset, which uses implicit classifiers, retains significant expressivity (e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were needed to make an existing test suite acceptable by the new type checker. © Springer-Verlag 2004.

• 12.
Imperial College London, London, United Kingdom.
Rice University, Houston, TX, USA. Yale University, New Haven, CT, USA. INRIA, Roquencourt, France.
Implementing Multi-stage Languages Using ASTs, Gensym, and Reﬂection2003In: Generative Programming and Component Engineering: Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003. Proceedings / [ed] Frank Pfenning & Yannis Smaragdakis, Heidelberg: Springer Berlin/Heidelberg, 2003, Vol. 2830, p. 57-76Conference paper (Refereed)

The paper addresses theoretical and practical aspects of implementing multi-stage languages using abstract syntax trees (ASTs), gensym, and reflection. We present an operational account of the correctness of this approach, and report on our experience with a bytecode compiler called MetaOCaml that is based on this strategy. Current performance measurements reveal interesting characteristics of the underlying OCaml compiler, and illustrate why this strategy can be particularly useful for implementing domain-specific languages in a typed, functional setting. © Springer-Verlag Berlin Heidelberg 2003.

• 13.
Department of Computer Science and Technology, Anhui Normal University, Wuhu Anhui 241000, China.
Integrated M. Tech, Mathematics and Computing, India Institute of Technology, New Delhi 110016, India . Department of Computer Science, Rice University, Houston, Texas 77005, USA . Department of Computer Science, Rice University, Houston, Texas 77005, USA .
Implicitly Heterogeneous Multi-Stage Programming for FPGAs2011In: Journal of Computational Information Systems, ISSN 1553-9105, Vol. 6, no 14, p. 4915-4922Article in journal (Refereed)

Previous work on semantics-based multi-state programming language design focused on homogeneous and heterogeneous software designs. In homogenous software design, the source and the target software programming languages are the same. In heterogeneous software design, they are different software languages. This paper proposes a practical means to circuit design by providing specialized offshoring translations from subsets of the source software programming language to subsets of the target hardware description language (HDL). This approach avoids manually writing codes for specifying the circuit of the given algorithm. To illustrate the proposed approach, we design and implement a translation to a subset of Verilog suitable numerical and logical computation. Through the translator, programmers can specify abstract algorithms in high level languages and automatically convert them into circuit descriptions in low level languages.© 2010 Binary Information Press.

• 14.
Department of Computer Science Anhui Normal University Wuhu, Anhui, China.
Department of Computer Science Rice University Houston, Texas, USA. School of Computer Northwestern Polytechnical University Xi’an, Shaanxi, China.
Multi-Stage Programming for High-Level Description of Circuit Families2010In: CISP 2010: 2010 3rd International Congress on Image and Signal Processing, 16-18 October 2010, Yantai, China, Piscataway, N.J.: IEEE Press, 2010, p. 3003-3007Conference paper (Refereed)

Hardware description languages use a low level of abstraction making the task of hardware designers error-prone and time consuming. The resulting descriptions tend to be lengthy and hard to reason about. This paper presents a minimal functional language for describing hardware circuits. Using multistage programming concepts, Fast Fourier Transform circuit descriptions can be generated in this language from a higher level generic description. It bridges the gap between the generated code and the required low-level hardware description by presenting the translator to automatically convert the generated code into Verilog, a streamline hardware description language.

• 15.
University of Glasgow, Glasgow, United Kingdom. Research Centre Jülich, Jülich, Germany. Rice University, Houston, Texas, USA.
DSL Implementation in MetaOCaml, Template Haskell, and C++2004In: Domain-Specific Program Generation: International Seminar, Dagstuhl Castle, Germany, March 23-28, 2003. Revised Papers / [ed] Christian Lengauer, Don Batory, Charles Consel & Martin Odersky, Berlin: Springer Berlin/Heidelberg, 2004, Vol. 3016, p. 51-72Conference paper (Refereed)

A wide range of domain-specific languages (DSLs) has been implemented successfully by embedding them in general purpose languages. This paper reviews embedding, and summarizes how two alternative techniques - staged interpreters and templates - can be used to overcome the limitations of embedding. Both techniques involve a form of generative programming. The paper reviews and compares three programming languages that have special support for generative programming. Two of these languages (MetaOCaml and Template Haskell) are research languages, while the third (C++) is already in wide industrial use. The paper identifies several dimensions that can serve as a basis for comparing generative languages.

• 16.
Curtin University of Technology, Bentley, Australia.
Rutgers University, New Jersey, USA. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Suzhou University, Jiangsu Sheng, China. University of Sydney, Sydney, Australia. Georgia State University, Georgia, USA.
Message from U-Science 2014 general chairs2014In: 2014 IEEE 12th International Conference on Dependable, Autonomic and Secure Computing, Piscataway: IEEE, 2014, article id 6945646Conference paper (Other (popular science, discussion, etc.))

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.© 2014 IEEE

• 17.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Rice University, Houston, TX, USA. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, TX, USA.
Accurate Rigorous Simulation Should be Possible for Good Designs2016In: Proceedings of the 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) / [ed] Erika Ábrahám & Sergiy Bogomolov, Piscataway, NJ: IEEE conference proceedings, 2016, article id 7479376Conference paper (Refereed)

The development of Cyber-Physical Systems benefits from better methods and tools to support the simulation and verification of hybrid (continuous/discrete) models. Acumen is an open source testbed for exploring the design space of what rigorous-but-practical next-generation tools can deliver to developers. Central to Acumen is the notion of rigorous simulation. Like verification tools, rigorous simulation is intended to provide guarantees about the behavior of the system. Like traditional simulation tools, it is intended to be intuitive, practical, and scalable. Whether these two goals can be achieved simultaneously is an important, long-term challenge.

This paper proposes a design principle that can play an important role in meeting this challenge. The principle addresses the criticism that accumulating numerical errors is a serious impediment to practical rigorous simulation. It is inspired by a twofold insight: one relating to the nature of systems engineered in the real world, and the other relating to how numerical errors in the simulation of a model can be recast as errors in the state or parameters of the model in the simulation. We present a suite of small, concrete benchmarks that can be used to assess the extent to which a rigorous simulator upholds the proposed principle. We also report on which benchmarks Acumen's current rigorous simulator already succeeds and which ones remain challenging.

• 18.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
SP Technical Research Institute of Sweden, Borås, Sweden. Rice University, Houston TX, USA. Rice University, Houston TX, USA. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston TX, USA.
Using Rigorous Simulation to Support ISO 26262 Hazard Analysis and Risk Assessment2015In: 2015 IEEE 12th International Conference on Embedded Software and Systems (ICESS) / [ed] Meikang Qiu, Yongxin Zhu, Daikai Zhu & Fengling Han, Piscataway, N.J.: IEEE Press, 2015, p. 1093-1096Conference paper (Refereed)

Rigorous simulation is a new technology that can play a key role in managing uncertainty in the design of safety-critical cyber-physical systems. One of its important applications is the analysis and evaluation of functional safety for road vehicles according to international standards such as ISO 26262. Previous work  presented preliminary evidence to support the feasibility of using rigorous simulation for this purpose. Here we report on advances in our implementation of rigorous simulation and show how they enable the rigorous simulation of more refined and more complete models. A larger case study highlights the benefits of these advances and helps us identify new challenges that should be addressed by future work. © 2015 IEEE.

• 19.
Rice University, Houston, TX, United States.
DIBRIS, Genova University, Genova, Italy. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Zhejiang University, Hangzhou, China.
A Semantic Account of Rigorous Simulation2018In: Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday / [ed] Marten LohstrohPatricia DerlerMarjan Sirjani, Amsterdam: Springer Berlin/Heidelberg, 2018, Vol. 10760, p. 223-239Chapter in book (Refereed)

Hybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct w.r.t. a clearly defined notion of reachability, which captures what is intuitively reachable in finite time. As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial. © 2018, Springer International Publishing AG, part of Springer Nature.

• 20. Duracz, Jan
University of Nottingham Ningbo China, Ningbo, China. Aston University, Birmingham, United Kingdom. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, USA.
Function Interval Arithmetic2014In: Mathematical software -- ICMS 2014: 4th International Congress, Seoul, South Korea, August 5-9, 2014. Proceedings / [ed] Hoon Hong & Chee Yap, Berlin, Heidelberg: Springer, 2014, p. 677-684Conference paper (Refereed)

We propose an arithmetic of function intervals as a basis for convenient rigorous numerical computation. Function intervals can be used as mathematical objects in their own right or as enclosures of functions over the reals. We present two areas of application of function interval arithmetic and associated software that implements the arithmetic: (1) Validated ordinary differential equation solving using the AERN library and within the Acumen hybrid system modeling tool. (2) Numerical theorem proving using the PolyPaver prover. © 2014 Springer-Verlag.

• 21.
Rice University, Houston, TX 77005, USA.
Rice University, Houston, TX 77005, USA. Rice University, Houston, TX 77005, USA. Rice University, Houston, TX 77005, USA. Rice University, Houston, TX 77005, USA.
Implicitly Heterogeneous Multi-Stage Programming2005In: Generative Programming and Component Engineering: 4th International Conference, GPCE 2005, Tallinn, Estonia, September 29 - October 1, 2005. Proceedings / [ed] Robert Glück, Michael Lowry, Heidelberg: Springer, 2005, p. 275-292Conference paper (Refereed)

Previous work on semantics-based multi-stage programming(MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designssimply add a hygienic quasi-quotation and evaluation mechanism to abase language. An apparent disadvantage of this approach is that theprogrammer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means toavoid this by providing specialized translations from subsets of the baselanguage to diﬀerent target languages. This approach preserves the homogeneous “look” of multi-stage programs, and, more importantly, thestatic guarantees about the generated code. In addition, compared to anexplicitly heterogeneous approach, it promotes reuse of generator sourcecode and systematic exploration of the performance characteristics of thetarget languages.To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show thatit preserves static typing. The translation is implemented, and evaluatedwith several benchmarks. The implementation is available in the onlinedistribution of MetaOCaml.

• 22.
Rice University, Department of Computer Science, Houston, TX.
Rice University, Department of Computer Science, Houston, TX. Rice University, Department of Computer Science, Houston, TX. Rice University, Department of Computer Science, Houston, TX. Rice University, Department of Computer Science, Houston, TX.
Implicitly Heterogeneous Multi-stage Programming2007In: New generation computing, ISSN 0288-3635, E-ISSN 1882-7055, Vol. 25, no 3, p. 305-336Article in journal (Refereed)

Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designs simply add a hygienic quasi-quotation and evaluation mechanism to a base language. An apparent disadvantage of this approach is that the programmer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means to avoid this by providing specialized translations from subsets of the base language to different target languages. This approach preserves the homogeneous “look” of multi-stage programs, and, more importantly, the static guarantees about the generated code. In addition, compared to an explicitly heterogeneous approach, it promotes reuse of generator source code and systematic exploration of the performance characteristics of the target languages.

To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show that it preserves static typing. The translation is implemented, and evaluated with several benchmarks. The implementation is available in the online distribution of MetaOCaml.

• 23.
Rice University Houston, Houston, USA.
The Semantics of Graphical Languages2007In: PEPM 2007: proceedings of the Workshop on Partial Evaluation and Program Manipulation : Nice, France, January 15-16, 2007, New York, NY: ACM Press, 2007, p. 122-133Conference paper (Refereed)

Visual notations are pervasive in circuit design, control systems, and increasingly in mainstream programming environments. Yet many of the foundational advances in programming language theory are taking place in the context of textual notations. In order to map such advances to the graphical world, and to take the concerns of the graphical world into account when working with textual formalisms, there is a need for rigorous connections between textual and graphical expressions of computation. To this end, this paper presents a graphical calculus called Uccello. Our key insight is that Ariola and Blom's work on sharing in the cyclic lambda calculus provides an excellent foundation for formalizing the semantics of graphical languages. As an example of what can be done with this foundation, we use it to extend a graphical language with staging constructs. In doing so, we provide the first formal account of sharing in a multi-stage calculus. Copyright © 2007 ACM.

• 24.
Rice University, Houston, United States.
Rice University, Houston, United States. University of Colorado, Boulder, United States. Rice University, Houston, United States.
Concoqtion: Indexed Types Now!2007In: PEPM 2007: proceedings of the Workshop on Partial Evaluation and Program Manipulation : Nice, France, January 15-16, 2007, New York, NY: ACM Press, 2007, p. 112-121Conference paper (Refereed)

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate Fω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

• 25.
Computer Science Department, Indiana University, Bloomington, Indiana, United States.
Computer Science Department, Indiana University, Bloomington, Indiana, United States. Department of Computer Science, Yale University, New Haven, United States.
Macros as Multi-Stage Computations: Type-Safe, Generative, Binding Macros in MacroML2001In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01): Florence, Italy, Sept. 3-5, 2001, New York, N.Y.: ACM Press, 2001, p. 74-85Conference paper (Refereed)

With few exceptions, macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed functional languages: static typing and static scoping. At a deeper level, there is a need for a simple, usable semantics for macros. This paper argues that these problems can be addressed by formally viewing macros as multi-stage computations. This view eliminates the need for freshness conditions and tests on variable names, and provides a compositional interpretation that can serve as a basis for designing a sound type system for languages supporting macros, or even for compilation. To illustrate our approach, we develop and present MacroML, an extension of ML that supports inlining, recursive macros, and the definition of new binding constructs. The latter is subtle, and is the most novel addition in a statically typed setting. The semantics of a core subset of MacroML is given by an interpretation into MetaML, a statically-typed multi-stage programming language. It is then easy to show that MacroML is stage- and type-safe: macro expansion does not depend on runtime evaluation, and both stages do not "go wrong.

• 26.
Rice University, Houston, TX.
Rice University, Houston, TX. Rice University, Houston, TX. Rice University, Houston, TX. Rice University, Houston, TX. Intel Strategic CAD Labs, Portland, OR. Intel Strategic CAD Labs, Portland, OR.
Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability2008In: PEPM '08: proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, San Francisco, California, USA, January 7-8, 2008, New York, NY, USA: ACM Press, 2008, p. 13-20Conference paper (Refereed)

Modern hardware description languages support code-generation constructs like generate/endgenerate in Verilog. These constructs are intended to describe regular or parameterized hardware designs and, when used effectively, can make hardware descriptions shorter, more understandable, and more reusable. In practice, however, designers avoid these constructs because it is difficult to understand and predict the properties of the generated code. Is the generated code even type safe? Is it synthesizable? What physical resources (e.g. combinatorial gates and flip-flops) does it require? It is often impossible to answer these questions without first generating the fully-expanded code. In the Verilog and VHDL communities, this generation process is referred to as elaboration.

This paper proposes a disciplined approach to elaboration in Verilog. By viewing Verilog as a statically typed two-level language, we are able to reflect the distinction between values that are known at elaboration time and values that are part of the circuit computation. This distinction is crucial for determining whether abstractions such as iteration and module parameters are used in a synthesizable manner. To illustrate this idea, we develop a core calculus for Verilog that we call Featherweight Verilog (FV) and an associated static type system. We formally define a preprocessing step analogous to the elaboration phase of Verilog, and the kinds of errors that can occur during this phase. Finally, we show that a well-typed design cannot cause preprocessing errors, and that the result of its expansion is always a synthesizable circuit.

• 27.
Rice University, 6100 Main St, Houston, TX 77005, United States.
Rice University, 6100 Main St, Houston, TX 77005, United States. Rice University, 6100 Main St, Houston, TX 77005, United States. Rice University, 6100 Main St, Houston, TX 77005, United States. Rice University. Intel Strategic CAD Labs, 2501 NW 229th Ave, Hillsboro, OR 97124, United States. Intel Strategic CAD Labs, 2501 NW 229th Ave, Hillsboro, OR 97124, United States.
Synthesizable High Level Hardware Descriptions2010In: New generation computing, ISSN 0288-3635, E-ISSN 1882-7055, Vol. 28, no 4, p. 339-369Article in journal (Refereed)

Modern hardware description languages support code generation constructs like generate/endgenerate in Verilog. These constructs are used to describe regular or parameterized hardware designsand, when used eﬀectively, can make hardware descriptions shorter, moreunderstandable, and more reusable. In practice, however, designers avoidthese abstractions because it is diﬃcult to understand and predict theproperties of the generated code. Is the generated code even type safe?Is it synthesizable? What physical resources (e.g. combinatorial gatesand ﬂip-ﬂops) does it require? It is often impossible to answer thesequestions without ﬁrst generating the fully-expanded code. In the Verilog and VHDL communities, this generation process is referred to as elaboration.This paper proposes a disciplined approach to elaboration in Verilog.∗1 By viewing Verilog as a statically typed two-level language, we are able to reﬂect the distinction between values that are known at elaborationtime and values that are part of the circuit computation. This distinctionis crucial for determining whether generative constructs, such as iterationand module parameters, are used in a synthesizable manner. This allowsus to develop a static type system that guarantees synthesizability. Thetype system achieves safety by performing additional checking on generative constructs and array indices. To illustrate this approach, we developa core calculus for Verilog that we call Featherweight Verilog (FV) andan associated static type system. We formally deﬁne a preprocessing stepanalogous to the elaboration phase of Verilog, and the kinds of errors thatcan occur during this phase. Finally, we show that a well-typed designcannot cause preprocessing errors, and that the result of its elaborationis always a synthesizable circuit.

• 28.
National Institute of Advanced Industrial Science and Technology, Ikeda, Osaka, Japan.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Reasoning about multi-stage programs2016In: Journal of functional programming (Print), ISSN 0956-7968, E-ISSN 1469-7653, Vol. 26, article id e22Article in journal (Refereed)

We settle three basic questions that naturally arise when verifying code generators written in multi-stage functional programming languages. First, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more care is needed to reason about terms with free variables. Second, staging annotations, as the name "annotations" suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be true? We give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy useful, standard extensional properties, for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such properties or, in principle, any valid program equivalence. These results yield important insights into staging and allow us to prove the correctness of quite complicated multi-stage programs. © Cambridge University Press 2016.

• 29.
Rice University, Houston, Texas, USA.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, USA.
Reasoning About Multi-Stage Programs2012In: Programming Languages and Systems: 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings / [ed] Helmut Seidl, Berlin: Springer Publishing Company, 2012, Vol. 7211, p. 357-376Conference paper (Refereed)

We settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more care is needed to reason about terms with free variables. Secondly, staging annotations, as the name “annotations” suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be true? We give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy useful, standard extensional facts—for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such facts or, in principle, any valid program equivalence. These results greatly improve our understanding of staging, and allow us to prove the correctness of quite complicated multi-stage programs. © 2012 Springer-Verlag.

• 30.
Rice University, Houston, TX, USA.
Rice University, Houston, TX, USA. Rice University, Houston, TX, USA.
E-FRP with Priorities2007In: EMSOFT '07: Proceedings of the Seventh ACM and IEEE International Conference on Embedded Software / [ed] Christoph M Kirsch & Reinhard Wilhelm, New York, NY: ACM Press, 2007, p. 221-230Conference paper (Other academic)

E-FRP is declarative language for programming resourcebounded,event-driven systems. The original high-level semanticsof E-FRP requires that each event handler executeatomically. This requirement facilitates reasoning about EFRPprograms, and therefore it is a desirable feature of thelanguage. But the original compilation strategy requiresthat each handler complete execution before another eventcan occur. This implementation choice treats all eventsequally, in that it forces the upper bound on the time neededto respond to any event to be the same. While this is acceptablefor many applications, it is often the case that someevents are more urgent than others.In this paper, we show that we can improve the compilationstrategy without altering the high-level semantics.With this new compilation strategy, we give the programmermore control over responsiveness without taking awaythe ability to reason about programs at a high level. Theprogrammer controls responsiveness by declaring prioritiesfor events, and the compilation strategy produces code thatuses preemption to enforce these priorities. We show thatthe compilation strategy enjoys the same properties as theoriginal strategy, with the only change being that the programmerreasons modulo permutations on the order of eventarrivals.

• 31.
Fleet Numerical Meteorology and Oceanography Center, Monterey, USA.
Department of Computer Science, Rice University, Houston, TX, USA. Department of Computer Science, Rice University, Houston, TX, USA.
A Methodology for Generating Veriﬁed Combinatorial Circuits2004In: EMSOFT '04: Proceedings of the 4th ACM international conference on Embedded software, New York, NY: ACM Press, 2004, p. 249-258Conference paper (Refereed)

High-level programming languages offer significant expressivity but provide little or no guarantees about resource use. Resource-bounded languages --- such as hardware-description languages --- provide strong guarantees about the runtime behavior of computations but often lack mechanisms that allow programmers to write more structured, modular, and reusable programs. To overcome this basic tension in language design, recent work advocated the use of Resource-aware Programming (RAP) languages, which take into account the natural distinction between the development platform and the deployment platform for resource-constrained software.This paper investigates the use of RAP languages for the generation of combinatorial circuits. The key challenge that we encounter is that the RAP approach does not safely admit a mechanism to express a posteriori (post-generation) optimizations. The paper proposes and studies the use of abstract interpretation to overcome this problem. The approach is illustrated using an in-depth analysis of the Fast Fourier Transform (FFT). The generated computations are comparable to those generated by FFTW.

• 32.
Monterey, CA, USA.
Rice University, Houston, TX, USA.
Relating FFTW and Split-Radix2004In: Embedded Software and Systems: First International Conference, ICESS 2004, Hangzhou, China, December 9-10, 2004, Revised Selected Papers / [ed] Zhaohui Wu, Chun Chen, Minyi Guo & Jiajun Bu, Berlin: Springer Berlin/Heidelberg, 2004, p. 488-493Conference paper (Refereed)

Recent work showed that staging and abstract interpretation can be used to derive correct families of combinatorial circuits, and illustrated this technique with an in-depth analysis of the Fast Fourier Transform (FFT) for sizes 2n. While the quality of the generated code was promising, it used more floating-point operations than the well-known FFTW codelets and split-radix algorithm. This paper shows that staging and abstract interpretation can in fact be used to produce circuits with the same number of floating-point operations as each of split-radix and FFTW. In addition, choosing between two standard implementations of complex multiplication produces results that match each of the two algorithms. Thus, we provide a constructive method for deriving the two distinct algorithms. © Springer-Verlag Berlin Heidelberg 2005.

• 33.
Aston University, Birmingham, United Kingdom.
University of Nottingham Ningbo China, Ningbo, China. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Picard Method for Enclosing ODEs with Uncertain Initial Values2014In: 11th International Conference on Computability and Complexity in Analysis: July 21 - 24, 2014: Proceedings, 2014, p. 41-42Conference paper (Refereed)
• 34.
Computer Science Group, Aston University, Birmingham, United Kingdom.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Department of Computer Science, Rice University, Houston, Texas, USA. Department of Computer Science, Rice University, Houston, Texas, USA. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Woodruff School of Mechanical Engineering, School of Electrical & Computer Engineering, Georgia Institute of Technology, Atlanta, Georgia, USA.
Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point2016In: Nonlinear Analysis: Hybrid Systems, ISSN 1751-570X, E-ISSN 1878-7460, Vol. 20, p. 1-20Article in journal (Refereed)

Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution. ©2015 The Authors. Published by Elsevier Ltd.

• 35.
Aston University, Birmingham, United Kingdom.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Texas A&M University, College Station, USA.
Enclosing the Behavior of a Hybrid System up to and Beyond a Zeno Point2013In: 2013 IEEE 1st International Conference on Cyber-Physical Systems, Networks, and Applications, CPSNA 2013, Piscataway, N.J.: IEEE Press, 2013, p. 120-125Conference paper (Refereed)

Even simple hybrid systems like the classic bouncing ball can exhibit Zeno behaviors. The existence of this type ofbehavior has so far forced simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad hoc restrictions to circumvent Zeno behavior or to abandon hybrid modeling. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independently of the occurrence of agiven event. Such an event can then even occur an unbounded number of times, thus making it possible to handle certain types of Zeno behavior. © 2013 IEEE.

• 36.
Halmstad University, School of Information Science, Computer and Electrical Engineering (IDE), Halmstad Embedded and Intelligent Systems Research (EIS).
Rice University, USA. Lund University, Sweden.
Dependable Automotive Systems based on Model Certified Components2011Conference paper (Refereed)

Advances in Intelligent Transport Systems (ITS), intelligent vehicles and cooperative systems are enabling traffic and transport solutions that are both safer and more environmentally acceptable. While it is well known that high dependability is a desirable feature it has a price, and the level of dependability needed varies from application to application. Typical examples are cooperative safety applications, in particular traffic situation aware vehicle driver warning and assisting systems, enabled by vehicle-to-vehicle and vehicle-to-infrastructure wireless communication in combination with the use of geographical map information, Differential Global Positioning System (DGPS) and vehicle-carried sensors. This kind of applications depend on the reception of satellite data (combined with on-board sensor data from, e.g. odometer and accelerometer) for positioning of the own vehicle and on periodic broadcasting of this information to all neighbors in range. Both the wireless communication with satellites and the one between vehicles can have severe difficulties, for example due to hills or high buildings directly hindering both kinds of radio transmission. There are techniques to make the solutions more robust, e.g. by information fusion for temporary or local communication outage compensation. However, further development is needed and since coverage problems can be made known in advance and related to geographical areas, such information can also be explored.

• 37.
University of Passau, Germany.
Rice University, Computer Science, Houston, United States.
Preface2006In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 62, no 1, p. 1-2Article in journal (Other academic)
• 38.
Taha, WalidHalmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, USA.
Practical Aspects of Declarative Languages: 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017, Proceedings2017Conference proceedings (editor) (Refereed)

The proceedings contain 14 papers. The special focus in this conference is on Practical Aspects of Declarative Languages. The topics include: Eliminating irrelevant non determinism in functional logic programs; canonicalizing high-level constructs in picat; integrating answer set programming with object-oriented languages; extending answer set programs with interpreted functions as first-class citizens; lowering the learning curve for declarative programming; overlapping patterns for property-based testing; Boltzmann samplers for closed simply-typed lambda terms; selection equilibria of higher-order games; principles and prototype implementation; declarative programming of full-fledged musical applications; a domain-specific language for software-defined radio; a declarative DSL for customizing ASCII art and using iterative deepening for probabilistic logic inference. © Copyright 2017 Elsevier B.V., All rights reserved

• 39.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS).
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), CAISR - Center for Applied Intelligent Systems Research. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, USA. SP Technical Research Institute, Borås, Sweden. Volvo Group Trucks Technology, Göteborg, Sweden.
Domain Analysis for Standardised Functional Safety: A Case Study on Design-Time Verification of Automatic Emergency Breaking2014In: FISITA World Automotive Congress 2014: Maastricht, The Netherlands 2-6 June 2014: Volume 2 of 5, Hague: Royal Netherlands Society of Engineers (KIVI) , 2014, p. 845-854Conference paper (Refereed)

Simulation traditionally computes individual trajectories, which severely limits the assessment of overall system behaviour. To address this fundamental shortcoming, we rely on computing enclosures to determine bounds on system behaviour instead of individual traces. In the present case study, we investigate the enclosures of a generic Automatic Emergency Braking (AEB) system and demonstrate how this creates a direct link between requirement specification and standardized safety criteria as put forward by ISO 26262. The case study strongly supports that a methodology based on enclosures can provide a missing link across the engineering process, from design to compliance testing. This result is highly relevant for ongoing efforts to virtualize testing and create a unified tool-chain for the development of next generation Advanced Driver Assistance Systems.

• 40.
DIBRIS, Genova Univ., v. Dodecaneso 35, Genova, 16146, Italy.
University of Nottingham Ningbo, China. Rice University, Houston, TX, United States. Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Safe & robust reachability analysis of hybrid systems2018In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 747, p. 75-99Article in journal (Refereed)

Hybrid systems—more precisely, their mathematical models—can exhibit behaviors, like Zeno behaviors, that are absent in purely discrete or purely continuous systems. First, we observe that, in this context, the usual definition of reachability—namely, the reflexive and transitive closure of a transition relation—can be unsafe, i.e., it may compute a proper subset of the set of states reachable in finite time from a set of initial states. Therefore, we propose safe reachability, which always computes a superset of the set of reachable states. Second, in safety analysis of hybrid and continuous systems, it is important to ensure that a reachability analysis is also robust w.r.t. small perturbations to the set of initial states and to the system itself, since discrepancies between a system and its mathematical models are unavoidable. We show that, under certain conditions, the best Scott continuous approximation of an analysis A is also its best robust approximation. Finally, we exemplify the gap between the set of reachable states and the supersets computed by safe reachability and its best robust approximation. © 2018 The Authors

• 41.
University of Genoa, Genova, Italy.
Oregon Graduate Institute, Portland, OR, USA. Oregon Graduate Institute, Portland, OR, USA. Oregon Graduate Institute, Portland, OR, USA.
An Idealized MetaML: Simpler, and More Expressive1999In: Programming Languages and Systems: 8th European Symposium on Programming, ESOP'99, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999 : proceedings / [ed] S. Doaitse Swierstra, Berlin: Springer Berlin/Heidelberg, 1999, p. 193-207Conference paper (Refereed)

MetaML is a multi-stage functional programming language featuring three constructs that can be viewed as statically-typed refinements of the back-quote, comma, and eval of Scheme. Thus it provides special support for writing code generators and serves as a semanticallysound basis for systems involving multiple interdependent computational stages. In previous work, we reported on an implementation of MetaML, and on a reduction semantics and type-system for MetaML. In this paper, we present An Idealized MetaML (AIM) that is the result of our study of a categorical model for MetaML. An important outstanding problem is finding a type system that provides the user with a means for manipulating both open and closed code. This problem has eluded efforts by us and other researchers for over three years. AIM solves the issue by providing two type constructors, one classifies closed code and the other open code, and exploiting the way they interact. We point out that AIM can be verbose, and outline a possible remedy relating to the strictness of the closed code type. © Springer International Publishing AG, Part of Springer Science+Business Media 1999

• 42.
School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, USA.
Conformance Testing of Cyber-Physical Systems: A Comparative Study2014In: Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014) / [ed] Marieke Huisman, Jaco van de Pol, Tiziana Margaria, Julia Padberg & Gabriele Taentzer, Berlin: European Association of Software Science and Technology , 2014Conference paper (Refereed)

For systematic and automatic testing of cyber-physical systems, in which a set of test cases is generated based on a formal specification, a number of notions of conformance testing have been proposed. In this paper, we review two existing theories of conformance testing for cyber-physical systems and compare them. We point out their fundamental differences, and prove under which assumptions they coincide.

• 43.
Department of Computing Science, Chalmers University of Technology, Gothenburg, Sweden.
Department of Computing Science, Chalmers University of Technology, Gothenburg, Sweden. Department of Computer Science, Rice University, Houston, TX, USA.
Towards a Primitive Higher Order Calculus of Broadcasting Systems2002In: PPDP '02: Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, New York, NY: ACM Press, 2002, p. 2-13Conference paper (Refereed)

Ethernet-style broadcast is a pervasive style of computer communication. In this style, the medium is a single nameless channel. Previous work on modelling such systems proposed a first order process calculus called CBS. In this paper, we propose a fundamentally different calculus called HOBS. Compared to CBS, HOBS 1) is higher order rather than first order, 2) supports dynamic subsystem encapsulation rather than static, and 3) does not require an "underlying language" to be Turing-complete. Moving to a higher order calculus is key to increasing the expressivity of the primitive calculus and alleviating the need for an underlying language. The move, however, raises the need for significantly more machinery to establish the basic properties of the new calculus. This paper develops the basic theory for HOBS and presents two example programs that illustrate programming in this language. The key technical underpinning is an adaptation of Howe's method to HOBS to prove that bisimulation is a congruence. From this result, HOBS is shown to embed the lazy λ-calculus.

• 44.
OGI School of Science & Engineering, Oregon Health & Science University, Hillsboro, Oregon, USA.
Computer Science Department, Rice University, Houston, TX, USA. OGI School of Science & Engineering, Oregon Health & Science University, Portland, Oregon, USA.
Tagless Staged Interpreters for Typed Languages2002In: ICFP '02: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, New York, NY: ACM Press, 2002, Vol. 37, p. 218-229Conference paper (Refereed)

Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or more. Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (called Meta-D) and prove its type safety. To formalize Meta-D, we extend Shao, Saha, Trifonov and Papaspyrou's λH language to a multilevel setting. Building on λH allows us to demonstrate type safety in a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work needed for establishing the soundness of that system.

• 45.
Rice University, Houston, TX, USA.
Rice University, Houston, TX, USA. Rice University, Houston, TX, USA. Intel Strategic CAD Labs, Hillsboro, OR, USA. Intel Strategic CAD Labs, Hillsboro, OR, USA.
Static Consistency Checking for Verilog Wire Interconnects: Using dependent types to check the sanity of Verilog descriptions2011In: Higher-Order and Symbolic Computation, ISSN 1388-3690, E-ISSN 2212-0793, Vol. 24, no 1-2, p. 81-114Article in journal (Refereed)

The Verilog hardware description language has padding semantics that allow designers to write descriptions where wires of different bit widths can be interconnected. However, many of these connections are nothing more than bugs inadvertently introduced by the designer and often result in circuits that behave incorrectly or use more resources than required. A similar problem occurs when wires are incorrectly indexed by values (or ranges) that exceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the use of generate blocks to describe circuit families only makes the situation worse as it hides such inconsistencies making them harder to detect. Inconsistencies in the generated code are only exposed after elaboration when the code is fully-expanded.

In this paper we show that these inconsistencies can be pinned down prior to elaboration using static analysis. We combine dependent types and constraint generation to reduce the problem of detecting the aforementioned inconsistencies to a satisfiability problem. Once reduced, the problem can easily be solved with a standard satisfiability modulo theories (SMT) solver. In addition, this technique allows us to detect unreachable code when it resides in a block guarded by an unsatisfiable set of constraints. To illustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with generative constructs and previously defined elaboration semantics. We prove that a well-typed FV description will always elaborate into an inconsistency-free description. We also provide a freely-available implementation demonstrating our approach. © 2011 Springer Science+Business Media, LLC.

• 46.
Rice University, Houston, TX, USA.
Rice University, Houston, TX, USA. Rice University, Houston, TX, USA. Intel Strategic CAD Labs, Portland, OR, USA. Intel Strategic CAD Labs, Portland, OR, USA.
Static Consistency Checking for Verilog Wire Interconnects: Using dependent types to check the sanity of verilog descriptions2009In: PEPM '09: Proceedings of the 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, New York, NY: ACM Press, 2009, p. 121-130Conference paper (Refereed)

The Verilog hardware description language has padding semantics that allow designers to write descriptions where wires of different bit widths can be interconnected. However, many of these connections are nothing more than bugs inadvertently introduced by the designer and often result in circuits that behave incorrectly or use more resources than required. A similar problem occurs when wires are incorrectly indexed by values (or ranges) that exceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the use of generate blocks to describe circuit families only makes the situation worse as it hides such inconsistencies making them harder to detect. Inconsistencies in the generated code are only exposed after elaboration when the code is fully-expanded.

In this paper we show that these inconsistencies can be pinned down prior to elaboration using static analysis. We combine dependent types and constraint generation to reduce the problem of detecting the aforementioned inconsistencies to a satisfiability problem. Once reduced, the problem can easily be solved with a standard satisfiability modulo theories (SMT) solver. In addition, this technique allows us to detect unreachable code when it resides in a block guarded by an unsatisfiable set of constraints. To illustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with generative constructs and previously defined elaboration semantics. We prove that a well-typed FV description will always elaborate into an inconsistency-free description. We also provide a freely-available implementation demonstrating our approach. © 2009 ACM, Inc.

• 47.
Ain Shams University, Cairo, Egypt.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, USA.
Increasing Verilog’s Generative Power2014Conference paper (Refereed)

To cope with more complex circuits, well-understood higher-level abstraction mechanisms are needed. Verilog is already equipped with promising generative constructs making it possible to concisely describe a family of circuits as a parameterized module; however these constructs suffer from limited expressivity even in the latest IEEE standard. In this paper, we address generative constructs expressivity limitations, identifying the key extensions needed to overcome these limitations, and showing how to incorporate them in Verilog in a disciplined, backward-compatible way.

• 48.
University of Colorado at Boulder, Department of Electrical & Computer Engineering, Boulder City United States .
Rice University, Houston United States . Rice University, Department of Computer Science, Houston United States .
Exploring the Design Space of Higher-Order Casts2009In: Programming languages and systems: 18th European symposium on programming, ESOP 2009, held as part of the joint european conferences on theory and practice of software, ETAPS 2009, York, UK : proceedings, Berlin: Springer Berlin/Heidelberg, 2009, p. 17-31Conference paper (Refereed)

This paper explores the surprisingly rich design space for the simplytyped lambda calculus with casts and a dynamic type. Such a calculus is the targetintermediate language of the gradually typed lambda calculus but it is alsointeresting in its own right. In light of diverse requirements for casts, we developa modular semantic framework, based on Henglein’s Coercion Calculus, that instantiatesa number of space-efficient, blame-tracking calculi, varying in whaterrors they detect and how they assign blame. Several of the resulting calculi extendwork from the literature with either blame tracking or space efficiency, andin doing so reveal previously unknown connections. Furthermore, we introduce anew strategy for assigning blame under which casts that respect traditional subtypingare statically guaranteed to never fail. One particularly appealing outcomeof this work is a novel cast calculus that is well-suited to gradual typing.

• 49.
Rice University, Houston, TX 77005, United States.
Rice University, Houston, TX 77005, United States.
A Semantic Analysis of C++ Templates2006In: ECOOP 2006 - Object-Oriented Programming: 20th European Conference, Nantes, France, July 3-7, 2006, Proceedings / [ed] Dave Thomas, Heidelberg: Springer, 2006, p. 304-327Conference paper (Refereed)

Templates are a powerful but poorly understood feature ofthe C++ language. Their syntax resembles the parameterized classes ofother languages (e.g., of Java). But because C++ supports template specialization, their semantics is quite diﬀerent from that of parameterizedclasses. Template specialization provides a Turing-complete sub-languagewithin C++ that executes at compile-time. Programmers put this powerto many uses. For example, templates are a popular tool for writingprogram generators.The C++ Standard deﬁnes the semantics of templates using natural language, so it is prone to misinterpretation. The meta-theoretic propertiesof C++ templates have not been studied, so the semantics of templateshas not been systematically checked for errors. In this paper we presentthe ﬁrst formal account of C++ templates including some of the morecomplex aspects, such as template partial specialization. We validate oursemantics by proving type safety and verify the proof with the Isabelleproof assistant. Our formalization reveals two interesting issues in theC++ Standard: the ﬁrst is a problem with member instantiation and thesecond concerns the generation of unnecessary template specializations.

• 50.
University of Colorado, Boulder, CO, USA.
Rice University, Houston, TX, USA.
Gradual Typing for Functional Languages2007Conference paper (Refereed)

Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a gradual type system for a functional calculus named $\lambda^?_\to$. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops $\mathbf{Ob}^{?}_{<:}$, a gradual type system for object-based languages, extending the Ob < : calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.

12 1 - 50 of 92
Cite
Citation style
• apa
• harvard1
• ieee
• modern-language-association-8th-edition
• vancouver
• Other style
More styles
Language
• de-DE
• en-GB
• en-US
• fi-FI
• nn-NO
• nn-NB
• sv-SE
• Other locale
More languages
Output format
• html
• text
• asciidoc
• rtf