SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Mon 16 Nov 2020 10:20 - 11:00 at SPLASH-VII - Posters Session 2
Mon 16 Nov 2020 22:20 - 23:00 at SPLASH-VII - Posters Session 2 Mirror

We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files.

CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert’s programs that allows arbitrary shuffling of global definitions by linking and the other for ELF object files that treats blocks of encoded definitions as unanalyzable and indivisible units.

We propose a lightweight approach that solves the above problem without any modification to CompCert’s framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files.

Conference Day
Mon 16 Nov

Displayed time zone: Central Time (US & Canada) change

10:20 - 11:00
Posters Session 2Posters at SPLASH-VII +12h
10:20
40m
Poster
Resolution as Intersection Subtyping via Modus PonensOOPSLA
Posters
Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag
10:20
40m
Poster
Macros For Domain-Specific LanguagesOOPSLA
Posters
Michael BallantyneNortheastern University, Alexis KingNorthwestern University, Matthias FelleisenNortheastern University
10:20
40m
Poster
Precise Inference of Expressive Units of Measurement TypesOOPSLA
Posters
Tongtong XiangUniversity of Waterloo, Jeff Y. LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo
10:20
40m
Poster
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by ExampleOOPSLA
Posters
Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University
10:20
40m
Poster
A Sparse Iteration Space Transformation Framework for Sparse Tensor AlgebraOOPSLA
Posters
Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University
DOI Pre-print Media Attached File Attached
10:20
40m
Poster
Learning Semantic Program Embeddings with Graph Interval Neural NetworkOOPSLA
Posters
Yu WangNanjing University, China, Ke WangVisa Research, Fengjuan GaoNanjing University, Linzhang WangNanjing University
10:20
40m
Poster
Statically Verified Refinements for Multiparty ProtocolsOOPSLA
Posters
Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Raymond HuUniversity of Hertfordshire, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London
10:20
40m
Poster
Towards a Formal Foundation of Intermittent ComputingOOPSLA
Posters
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
10:20
40m
Poster
Incremental Predicate Analysis for Regression VerificationOOPSLA
Posters
Qianshan YuTsinghua University, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
10:20
40m
Poster
StreamQL: A Query Language for Processing Streaming Time SeriesOOPSLA
Posters
Lingkun KongRice University, Konstantinos MamourasRice University
10:20
40m
Poster
SATUNE: Synthesizing Efficient SAT EncodersOOPSLA
Posters
Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine
10:20
40m
Poster
Scaling Exact Inference for Discrete Probabilistic ProgramsOOPSLA
Posters
Steven HoltzenUniversity of California at Los Angeles, Guy Van den BroeckUniversity of California at Los Angeles, Todd MillsteinUniversity of California, Los Angeles
10:20
40m
Poster
Certified and Efficient Instruction SchedulingOOPSLA
Posters
Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG, Cyril SixKalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David MonniauxGrenoble Alps University / CNRS / Grenoble INP / VERIMAG
10:20
40m
Poster
Revisiting Iso-Recursive SubtypingOOPSLA
Posters
Yaoda ZhouUniversity of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Jinxu ZhaoUniversity of Hong Kong
10:20
40m
Poster
Guided Linking: Dynamic Linking Without the CostsOOPSLA
Posters
Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign
10:20
40m
Poster
Unifying Execution of Imperative Generators and Declarative SpecificationsOOPSLA
Posters
Pengyu NieUniversity of Texas at Austin, Marinela ParovicUniversity of Texas at Austin, Zhiqiang ZangUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin, Aleksandar MilicevicMicrosoft, Milos GligoricUniversity of Texas at Austin
10:20
40m
Poster
CompCertELF: Verified Separate Compilation of C Programs into ELF Object FilesOOPSLA
Posters
Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WilkeCentraleSupélec, Zhong ShaoYale University
22:20 - 23:00
Posters Session 2 MirrorPosters at SPLASH-VII
22:20
40m
Poster
Learning Semantic Program Embeddings with Graph Interval Neural NetworkOOPSLA
Posters
Yu WangNanjing University, China, Ke WangVisa Research, Fengjuan GaoNanjing University, Linzhang WangNanjing University
22:20
40m
Poster
Towards a Formal Foundation of Intermittent ComputingOOPSLA
Posters
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
22:20
40m
Poster
StreamQL: A Query Language for Processing Streaming Time SeriesOOPSLA
Posters
Lingkun KongRice University, Konstantinos MamourasRice University
22:20
40m
Poster
Incremental Predicate Analysis for Regression VerificationOOPSLA
Posters
Qianshan YuTsinghua University, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
22:20
40m
Poster
SATUNE: Synthesizing Efficient SAT EncodersOOPSLA
Posters
Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine
22:20
40m
Poster
A Sparse Iteration Space Transformation Framework for Sparse Tensor AlgebraOOPSLA
Posters
Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University
DOI Pre-print Media Attached File Attached
22:20
40m
Poster
Unifying Execution of Imperative Generators and Declarative SpecificationsOOPSLA
Posters
Pengyu NieUniversity of Texas at Austin, Marinela ParovicUniversity of Texas at Austin, Zhiqiang ZangUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin, Aleksandar MilicevicMicrosoft, Milos GligoricUniversity of Texas at Austin
22:20
40m
Poster
Statically Verified Refinements for Multiparty ProtocolsOOPSLA
Posters
Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Raymond HuUniversity of Hertfordshire, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London
22:20
40m
Poster
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by ExampleOOPSLA
Posters
Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University
22:20
40m
Poster
Revisiting Iso-Recursive SubtypingOOPSLA
Posters
Yaoda ZhouUniversity of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Jinxu ZhaoUniversity of Hong Kong
22:20
40m
Poster
Macros For Domain-Specific LanguagesOOPSLA
Posters
Michael BallantyneNortheastern University, Alexis KingNorthwestern University, Matthias FelleisenNortheastern University
22:20
40m
Poster
CompCertELF: Verified Separate Compilation of C Programs into ELF Object FilesOOPSLA
Posters
Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WilkeCentraleSupélec, Zhong ShaoYale University
22:20
40m
Poster
Certified and Efficient Instruction SchedulingOOPSLA
Posters
Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG, Cyril SixKalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David MonniauxGrenoble Alps University / CNRS / Grenoble INP / VERIMAG
22:20
40m
Poster
Resolution as Intersection Subtyping via Modus PonensOOPSLA
Posters
Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag
22:20
40m
Poster
Precise Inference of Expressive Units of Measurement TypesOOPSLA
Posters
Tongtong XiangUniversity of Waterloo, Jeff Y. LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo
22:20
40m
Poster
Guided Linking: Dynamic Linking Without the CostsOOPSLA
Posters
Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign
22:20
40m
Poster
Scaling Exact Inference for Discrete Probabilistic ProgramsOOPSLA
Posters
Steven HoltzenUniversity of California at Los Angeles, Guy Van den BroeckUniversity of California at Los Angeles, Todd MillsteinUniversity of California, Los Angeles