Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language
Foreign function interfaces (FFIs) allow programs written in one language (called the host language) to call functions written in another language (called the guest language), and are widespread throughout modern programming languages, with C FFIs being the most prevalent. Unfortunately, reasoning about C FFIs can be very challenging, particularly when using traditional methods which necessitate a full model of the guest language in order to guarantee anything about the whole language. To address this, we propose a framework for defining whole language semantics of FFIs without needing to model the guest language, which makes reasoning about C FFIs feasible. We show that with such a semantics, one can guarantee some form of soundness of the overall language, as well as attribute errors in well-typed host language programs to the guest language. We also present an implementation of this scheme, Poseidon Lua, which shows a speedup over a traditional Lua C FFI.
Thu 18 JulDisplayed time zone: Belfast change
13:30 - 15:10 | |||
13:30 20mResearch paper | Deep Static Modeling of invokedynamic Research Papers DOI Media Attached | ||
13:50 20mResearch paper | Automated Large-scale Multi-language Dynamic Program Analysis in the Wild Research Papers Alex Villazón Universidad Privada Boliviana, Bolivia, Haiyang Sun Università della Svizzera italiana, Andrea Rosà University of Lugano, Switzerland, Eduardo Rosales University of Lugano, Switzerland, Daniele Bonetta Oracle Labs, Isabella Defilippis Universidad Privada Boliviana (UPB), Sergio Oporto Universidad Privada Boliviana (UPB), Walter Binder University of Lugano, Switzerland DOI Media Attached | ||
14:10 20mResearch paper | MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors Research Papers Linghui Luo Paderborn University, Julian Dolby IBM Research, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM DOI Pre-print Media Attached | ||
14:30 20mResearch paper | Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language Research Papers Alexi Turcotte Northeastern University, Ellen Arteca Northeastern University, Gregor Richards University of Waterloo DOI Media Attached | ||
14:50 20mResearch paper | Multiverse Debugging: Non-deterministic Debugging for Non-deterministic Programs Research Papers Carmen Torres Lopez Vrije Universiteit Brussel, Robbert Gurdeep Singh Universiteit Gent, Belgium, Stefan Marr University of Kent, Elisa Gonzalez Boix Vrije Universiteit Brussel, Belgium, Christophe Scholliers Universiteit Gent, Belgium DOI Media Attached |