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 Jul Times are displayed in time zone: Greenwich Mean Time : Belfast change
13:30 - 15:10: Program Analysis 2Research Papers at Mancy Chair(s): Christian HammerUniversity of Potsdam | |||
13:30 - 13:50 Research paper | Deep Static Modeling of invokedynamic Research Papers DOI Media Attached | ||
13:50 - 14:10 Research paper | Automated Large-scale Multi-language Dynamic Program Analysis in the Wild Research Papers Alex VillazónUniversidad Privada Boliviana, Bolivia, Haiyang SunUniversità della Svizzera italiana, Andrea RosàUniversity of Lugano, Switzerland, Eduardo RosalesUniversity of Lugano, Switzerland, Daniele BonettaOracle Labs, Isabella DefilippisUniversidad Privada Boliviana (UPB), Sergio OportoUniversidad Privada Boliviana (UPB), Walter BinderUniversity of Lugano, Switzerland DOI Media Attached | ||
14:10 - 14:30 Research paper | MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors Research Papers Linghui LuoPaderborn University, Julian DolbyIBM Research, Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM DOI Pre-print Media Attached | ||
14:30 - 14:50 Research paper | Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language Research Papers Alexi TurcotteNortheastern University, Ellen ArtecaNortheastern University, Gregor RichardsUniversity of Waterloo DOI Media Attached | ||
14:50 - 15:10 Research paper | Multiverse Debugging: Non-deterministic Debugging for Non-deterministic Programs Research Papers Carmen Torres LopezVrije Universiteit Brussel, Robbert Gurdeep SinghUniversiteit Gent, Belgium, Stefan MarrUniversity of Kent, Elisa Gonzalez BoixVrije Universiteit Brussel, Belgium, Christophe ScholliersUniversiteit Gent, Belgium DOI Media Attached |