Publications related to Formal Verification of Just-in-Time Compilation

Related publications (13)

Adaptive Recursive Query Optimization

Anastasia Ailamaki, Martin Odersky, Guillaume André Fradji Martres, Anna Patricia Herlihy

Performance-critical industrial applications, including large-scale program, network, and distributed system analyses, are increasingly reliant on recursive queries for data analysis. Yet traditional relational algebra-based query optimization techniques d ...

IEEE2024

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Yichen Xu

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

Smart Proofs via Recursive Information Gathering: Decentralized Refereeing by Smart Contracts

Clément Hongler

We introduce the SPRIG (Smart Proofs via Recursive Information Gathering) protocol. SPRIG allows agents to propose, question, and defend mathematical proofs in a decentralized fashion. A structure of stakes and bounties aims at producing debates in good fa ...

Association for Computing Machinery (ACM)2024

Johann Sebastian Bach – The Chorales

Martin Alois Rohrmeier, Johannes Hentschel, Ioannis Rammos

This is a README file for a data repository originating from the DCML corpus initiative and serves as welcome page for both the GitHub repo

Zenodo2023

Optimized Memory Access For Dynamically Scheduled High Level Synthesis

Paolo Ienne, Atri Bhattacharyya

Dynamically-scheduled elastic circuits generated by High-Level Synthesis (HLS) tools are inherently out-of-order, following the flow of data rather than the evolution of an instruction pointer. Components of the circuit which access memory need to be conne ...

2018

CFIXX: Object Type Integrity for C++

Mathias Josef Payer

C++ relies on object type information for dynamic dispatch and casting. The association of type information to an object is implemented via the virtual table pointer, which is stored in the object itself. As C++ has neither memory nor type safety, adversar ...

The Internet Society2018

Detailed Heap Profiling

James Richard Larus, Stuart Anthony Byma

Modern software systems heavily use the memory heap. As systems grow more complex and compute with increasing amounts of data, it can be difficult for developers to understand how their programs actually use the bytes that they allocate on the heap and whe ...

ACM2018

Proactive Synthesis of Recursive Tree-to-String Functions from Examples

Viktor Kuncak, Mikaël Mayer, Jad Hamza

Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute t ...

2017

Higher-Order Subtyping with Type Intervals

Sandro Stucki

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

EPFL2017

Decrypting Local Type Inference

Hubert Plociniczak

Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...

EPFL2016

Automating Ad hoc Data Representation Transformations

Martin Odersky, Vlad Ureche

To maximize run-time performance, programmers often specialize their code by hand, replacing library collections and containers by custom objects in which data is restructured for efficient access. However, changing the data representation is a tedious and ...

Assoc Computing Machinery2015

ScalaDyno: Making Name Resolution and Type Checking Fault-tolerant

Martin Odersky, Vlad Ureche

The ScalaDyno compiler plugin allows fast prototyping with the Scala programming language, in a way that combines the benefits of both statically and dynamically typed languages. Static name resolution and type checking prevent partially-correct code from ...

ACM2014

Language Virtualization for Heterogeneous Parallel Computing

Martin Odersky, Tiark Rompf

As heterogeneous parallel systems become dominant, application developers are being forced to turn to an incompatible mix of low level programming models (e.g. OpenMP, MPI, CUDA, OpenCL). However, these models do little to shield developers from the diffic ...

2010