Events

Since introduction of the IEEE 754 floating point standard in 1985, numerical methods have become ubiquitous --- and increasingly sophisticated. With growing code complexity of numerical libraries grows the need for rigorous Software Engineering methodology: as provided by Computer Science and state of the art regarding digital processing of discrete data, but lacking in the continuous realm. We apply, adapt, and extend the classical concepts --- specification, algorithmics, analysis, complexity, verification --- from discrete bit strings, integers, graphs etc. to real numbers, converging sequences, smooth/integrable functions, bounded operators, and compact subsets: A new paradigm formalizes mathematical structures as continuous Abstract Data Types with rigorous Turing-computable semantics but without the hassle of actual Turing machines.

Shared memory concurrency is the pervasive programming model for multicore architectures such as X86, Power, and ARM. Depending on the memory organization, each architecture follows a somewhat different shared memory model. All these models, however, have one common feature: they allow certain outcomes for concurrent programs that cannot be explained by interleaving execution. In addition to the complexity due to architectures, compilers like GCC and LLVM perform various program transformations, which also affect the outcomes of concurrent programs.

To be able to program these systems correctly and effectively, it is important to a define a formal language-level concurrency model. For efficiency, it is important that the model is weak enough to allow various compiler optimizations on shared memory accesses as well as efficient mappings to the architectures. For programmability, the model should be strong enough to disallow bogus "out- of-thin-air" executions and provide strong guarantees for well synchronized programs. Because of these conflicting requirements, defining such a formal model is very difficult. This is why, despite years of research, major programming languages such as C/C++ and Java do not yet have completely adequate formal models defining their concurrency semantics.

In this thesis, we address this challenge and develop a formal concurrency model that is very good both in terms of compilation efficiency and of programmability. Unlike most previous approaches, which were defined either operationally or axiomatically on single executions, our formal model is based on event structures, which represents multiple program executions, and thus gives us more structure to define the semantics of concurrency.

In more detail, our formalization has two variants: the weaker version, WEAKEST, and the stronger version, WEAKESTMO. The WEAKEST model simulates the promising semantics proposed by Kang et al., while WEAKESTMO is incomparable to the promising semantics. Moreover, WEAKESTMO discards certain questionable behaviors allowed by the promising semantics. We show that the proposed WEAKESTMO model resolve out-of-thin-air problem, provide standard data-race-freedom (DRF) guarantees, allow the desirable optimizations, and can be mapped to the architectures like X86, PowerPC, ARMv7. Additionally, our models are flexible enough to leverage existing results from the literature. In addition, in order to ensure the correctness of compilation by a major compiler, we developed a translation validator targeting LLVM’s "opt" transformations of concurrent C/C++ programs. Using the validator, we identified a few subtle compilation bugs, which were reported and were fixed. Additionally, we observe that LLVM concurrency semantics differs from that of C11; there are transformations which are justified in C11 but not in LLVM and vice versa. Considering the subtle aspects of LLVM concurrency, we formalized a fragment of LLVM’s concurrency semantics and integrated it into our WEAKESTMO model.

A growing number of domestic spaces incorporate products that collect data from cameras, microphones and other sensors, leading to privacy concerns. In this talk I report on two user studies performed to learn about perceptions of privacy and trust for sensor-enabled, connected devices such as smart home assistants. The study results suggest that users are more likely to trust devices with materially representative privacy status indicators. This means that the indicators themselves are part of what determines what sensing can take place. I will describe how we have applied the study results to the design of current devices and what the implications are for the physical design of future smart devices.

Time permitting, I will also talk about my other current passion -- design for additive manufacturing – and what researchers can do to ensure we reach the vastly exciting potential of this method of production. I will bring exotic 3D printed parts to help demonstrate my points.

Automated program repair is an emerging and exciting field of research, which allows for automated rectification of errors and vulnerabilities. The use of automated program repair can be myriad, such as (a) improving programmer productivity (b) automated fixing of security vulnerabilities as they are detected, (c) self-healing software for autonomous devices such as drones, as well as (d) use of repair in introductory programming education by grading and providing hints for programming assignments. One of the key technical challenges in achieving automated program repair, is the lack of formal specifications of intended program behavior. In this talk, we will conceptualize the use of symbolic execution approaches and tools for extracting such specifications. This is done by analyzing a buggy program against selected tests, or against reference implementations. Such specification inference capability can be combined with program synthesis techniques to automatically repair programs. The capability of specification inference also serves a novel use of symbolic execution beyond verification and navigation of large search spaces. Automated program repair via symbolic execution goes beyond search-based approaches which attempt to lift patches from elsewhere in the program. Such an approach can construct "imaginative" patches, serves as a test-bed for the grand- challenge of automated programming, and contributes to the vision of trustworthy self-healing software. Towards the end of the talk, we can put the research on automated repair in light of the overall practice of software security, by sharing some experiences gained at the Singapore Cyber-security Consortium.