Over the past decade, the Scala community has shown great interest in using type-level programming to obtain additional type safety.
Unfortunately, the lack of support from the Scala compiler has been a barrier to the adoption of that technique, notably du ...
Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...
Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
With the widespread deployment of Control-Flow Integrity (CFI), control-flow hijacking attacks, and consequently code reuse attacks, are significantly more difficult. CFI limits control flow to well-known locations, severely restricting arbitrary code exec ...
Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...
Concurrency bugs are at the heart of some of the worst bugs that
plague software. Concurrency bugs slow down software development
because it can take weeks or even months before developers
can identify and fix them.
In-production detection, root cause ...
Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. In many domains, roundoff errors are not the only source of inaccuracy and measurement as ...
Compile-time metaprogramming has been proven immensely useful enabling programming techniques such as language virtualization, embedding of external DSLs, self-optimization, and boilerplate generation amongst many others. In the recent production release o ...
As the classic transactional abstraction is sometimes considered too restrictive in leveraging parallelism, a lot of work has been devoted to devising relaxed transactional models with the goal of improving concurrency. Nevertheless, the quest for improvin ...
Statically-typed languages offer type systems that are less and less comprehensible for programmers as the language grows in complexity. In this paper, we present a type debugger, a tool that enables analysis of type-related problems as well as exploration ...
Subtyping tests are essential in typed publish/subscribe infrastructures, especially when the underlying programming language supports subtype conformance, as in Java or C#. These tests are particularly challenging when the publish/subscribe infrastructure ...
The aim of this thesis is to construct toolsets that support the Synchronous Java programming language, an extension to the Java language that introduces a new method of synchronization between threads. The contributions of this thesis include a State Spac ...
The execution of formal specifications is important for verification, validation and animation purposes. This thesis describes transformation of CO-OPN specifications in executable code. The original goal of this transformation was validation by prototypin ...
