Abstract: The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.

Abstract: The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which model-level control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.

Abstract: The verification of hybrid systems requires ways of handling both the discrete and continuous dynamics, e.g., by proofs, abstraction, or approximation. Fundamentally, however, the study of the safety of hybrid systems can be shown to reduce constructively to the problem of generating invariants for their differ- ential equations. We recently focused on this core problem. We study the case of algebraic invariant equation, i.e. invariants described by a polynomial equation of the form p = 0 for a polynomial p.

Abstract: We are at the end of a four­year effort that has dramatically improved the capability of the use of RF sensors, particularly those that measure received signal strength (RSS) to sense the locations and context of people in buildings and homes.  We have investigated both systems which use RFID tags to identify a person or object, and those which use a static deployed network of transceivers for device­free localization, to locate people moving in the environment who do not carry any tag or device.  Locating people who don’t wear a de

Abstract: Cyber-­Physical Systems comprise richly heterogeneous collections of devices (mobile devices, home electronics, taxis, robotic drones, etc.) that together gather sensor data, analyze it, and coordinate large-­‐scale actions in response to it.

Abstract: The objective of this project is to develop a theoretical framework for stochastic learning, decision-making, and control in high-dimensional cyber-physical systems. In our general framework, decision makers dynamically refine their estimates of the time-varying physical system based on acquired information, which may be obtained by distributed sensors.

Abstract: During the development process of CPS, an analysis of whether the system operates safely in its target environment is of utmost importance. This entails two interconnected research goals in the research areas of system design and system verification, which tie together research in formal verification of CPS with research on knowledge representation and reasoning in multi-agent systems:

Abstract: Central to the operation of cyber-physical systems (CPS) is accurate and reliable knowledge of time, both for meaningfully sensing and controlling the physical world state and for correct, high-performance and energy-efficient orchestration of computing and communication operations. Emerging applications that seek to control agile physical processes or depend on precise knowledge of time to infer location and coordinate communication, make use of time with diverse semantics and dynamic quality requirements.

Abstract: Motivation: