Fetching the paper…
Reading the bibliography…
We target the problem of automatically synthesizing proofs of semantic equivalence between two programs made of sequences of statements.
“Graph Representations for Higher-Order Logic and Theorem Proving”
Aditya Paliwal et al · 1905
Earlier work this paper cites.
“Regular expressions and the equivalence of programs”
Donald Kaplan · 1969
Earlier work this paper cites.
“Global common subexpression elimination”
John Cocke · 1970
Earlier work this paper cites.
“Dynamic Construction of Finite Automata from examples using Hill-climbing”
M. Tomita · 1982
Earlier work this paper cites.
“Probabilistic Algorithms for Deciding Equivalence of Straight-Line Programs”
Oscar Ibarra and Shlomo Moran · 1983
Earlier work this paper cites.
“Computing with rewrite systems”
Nachum Dershowitz · 1985
Earlier work this paper cites.
“Rewriting techniques for program synthesis”
Uday Reddy · 1989
Earlier work this paper cites.
“Data flow analysis as model checking”
Bernhard Steffen · 1991
Earlier work this paper cites.
“Advanced Compiler Design Implementation.”
Steven Muchnick · 1997
Earlier work this paper cites.
“Early stopping-but when?”
Lutz Prechelt · 1998
Earlier work this paper cites.
“Code transformations to improve memory parallelism”
Vijay Pai and Sarita Adve · 1999
Earlier work this paper cites.
“Translation validation for an optimizing compiler”
George Necula · 2000
Earlier work this paper cites.
“Translation Validation for an Optimizing Compiler”
George. Necula · 2000
Earlier work this paper cites.
“Ensemble Methods in Machine Learning”
Thomas. Dietterich · 2000
Earlier work this paper cites.
“Syntactic program transformations for automatic abstraction”
Kedar Namjoshi and Robert Kurshan · 2000
Earlier work this paper cites.
“Taylor expansion diagrams: A compact, canonical representation with applications to symbolic verification”
Maciej Ciesielski, Priyank Kalla, Zhihong Zheng and Bruno Rouzeyre · 2002
Earlier work this paper cites.
“On the equivalence of two systems of affine recurrence equations”
Denis Barthou, Paul Feautrier and Xavier Redon · 2002
Earlier work this paper cites.
“Behavioral consistency of C and Verilog programs using bounded model checking”
Edmund Clarke, Daniel Kroening and Karen Yorav · 2003
Earlier work this paper cites.
“Model checking programs”
Willem Visser et al · 2003
Earlier work this paper cites.
“On the recognition of algorithm templates”
Christophe Alias and Denis Barthou · 2004
Earlier work this paper cites.
“Program transformation with Stratego/XT”
Eelco Visser · 2004
Earlier work this paper cites.
“Approximate probabilistic model checking”
Thomas Hérault, Richard Lassaigne, Frédéric Magniette and Sylvain Peyronnet · 2004
Earlier work this paper cites.
“On probabilistic program equivalence and refinement”
Andrzej Murawski and Joël Ouaknine · 2005
Earlier work this paper cites.
“Ablego: A Function Outlining and Partial Inlining Framework: Research Articles”
Peng Zhao and José Amaral · 2007
Earlier work this paper cites.
“Inference rules for proving the equivalence of recursive procedures”
Benny Godlin and Ofer Strichman · 2008
Earlier work this paper cites.
“Program analysis for compiler validation”
Anna Zaks and Amir Pnueli · 2008
Earlier work this paper cites.
“Equivalence checking of static affine programs using widening to handle recurrences”
Sven Verdoolaege, Gerda Janssens and Maurice Bruynooghe · 2009
Earlier work this paper cites.
“Program transformations using temporal logic side conditions”
Sara Kalvala, Richard Warburton and David Lacey · 2009
Earlier work this paper cites.
“Generative Language Modeling for Automated Theorem Proving”
Stanislas Polu and Ilya Sutskever · 2009
Earlier work this paper cites.
Nghi.. Bui · 2009
Earlier work this paper cites.
“A framework for formal verification of compiler optimizations”
William Mansky and Elsa Gunter · 2010
Earlier work this paper cites.
“Well-structured program equivalence is highly undecidable”
Robert Goldblatt and Marcel Jackson · 2012
Earlier work this paper cites.
“On the naturalness of software”
Abram Hindle et al · 2012
Earlier work this paper cites.
“Equivalence checking of static affine programs using widening to handle recurrences”
Sven Verdoolaege, Gerda Janssens and Maurice Bruynooghe · 2012
Cited alongside, same era.
“Probabilistic theorem proving”
Vibhav Gogate and Pedro Domingos · 2012
Cited alongside, same era.
“Verification of Loop and Arithmetic Transformations of Array-Intensive Behaviors”
Chandan Karfa, Kunal Banerjee, Dipankar Sarkar and Chittaranjan Mandal · 2013
Cited alongside, same era.
“When polyhedral transformations meet SIMD code generation”
Martin Kong et al · 2013
Cited alongside, same era.
“An empirical investigation of catastrophic forgetting in gradient-based neural networks”
Ian Goodfellow et al · 2013
Cited alongside, same era.
“Semantic program alignment for equivalence checking”
Berkeley Churchill, Oded Padon, Rahul Sharma and Alex Aiken · 2019
Later among the works it cites.
“Code2Vec: Learning Distributed Representations of Code”
Uri Alon, Meital Zilberstein, Omer Levy and Eran Yahav · 2019
Later among the works it cites.
“An Empirical Study on Learning Bug-Fixing Patches in the Wild via Neural Machine Translation”
Michele Tufano et al · 2019
Later among the works it cites.
“DIRE: A Neural Approach to Decompiled Identifier Naming”
Jeremy Lacomis et al · 2019
Later among the works it cites.
“Automatically harnessing sparse acceleration”
Philip Ginsbach, Bruce Collie and Michael O’Boyle · 2020
Later among the works it cites.
“Program Equivalence for Assisted Grading of Functional Programs”
Joshua Clune, Vijay Ramamurthy, Ruben Martins and Umut. Acar · 2020
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
“Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions”
Yves Bertot and Pierre Castéran · 2013
Cited alongside, same era.
“Extending the scope of translation validation by augmenting path based equivalence checkers with SMT solvers”
Kunal Banerjee, Chittaranjan Mandal and Dipankar Sarkar · 2014
Cited alongside, same era.
“Sequence to sequence learning with neural networks”
I Sutskever, O Vinyals and QV Le · 2014
Cited alongside, same era.
“On program equivalence with reductions”
Guillaume Iooss, Christophe Alias and Sanjay Rajopadhye · 2014
Cited alongside, same era.
“Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations”
Markus Schordan, Pei-Hung Lin, Dan Quinlan and Louis-Noël Pouchet · 2014
Cited alongside, same era.
“Adam: A Method for Stochastic Optimization”
Diederik. Kingma and Jimmy Ba · 2015
Cited alongside, same era.
“Program equivalence by circular reasoning”
Dorel Lucanu and Vlad Rusu · 2015
Cited alongside, same era.
Later among the works it cites.
“Equivalence of dataflow graphs via rewrite rules using a graph-to-sequence neural model”
Steve Kommrusch, Théo Barollet and Louis-Noël Pouchet · 2020
Later among the works it cites.
“Properties of matrix multiplication”
Sal Khan · 2020
Later among the works it cites.
“Scaling Laws for Neural Language Models”
J. Kaplan et al · 2020
Later among the works it cites.
“ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code”
Sahar Badihi, Faridah Akinotcho, Yi Li and Julia Rubin · 2020
Later among the works it cites.
“An Appraisal of Incremental Learning Methods”
Yong Luo, Liancheng Yin, Wenchao Bai and Keming Mao · 2020
Later among the works it cites.
“Incremental Unsupervised Domain-Adversarial Training of Neural Networks”
Antonio-Javier Gallego, Jorge Calvo-Zaragoza and Robert. Fisher · 2020
Later among the works it cites.
“Deep Learning For Symbolic Mathematics”
Guillaume Lample and François Charton · 2020
Later among the works it cites.
“The 2020 State of the Octoverse”, 2021
GitHub · 2021
Closest in time.
“Language-parametric compiler validation with application to LLVM”
Theodoros Kasampalis et al · 2021
Closest in time.
“S4Eq Software”, https://github.com/SteveKommrusch/PrgEq , 2021
Steve Kommrusch · 2021
Closest in time.
“MACHINE LEARNING FOR COMPUTER AIDED PROGRAMMING: FROM STOCHASTIC PROGRAM REPAIR TO VERIFIABLE PROGRAM EQUIVALENCE”, 2021
Steve Kommrusch · 2021
Closest in time.
“Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models”
Steve Kommrusch, Théo Barollet and Louis-Noël Pouchet · 2021
Closest in time.
“Egg: Fast and Extensible Equality Saturation”
Max Willsey et al · 2021
Closest in time.
“EqBench: A Dataset of Equivalent and Non-equivalent Program Pairs”
Sahar Badihi, Yi Li and Julia Rubin · 2021
Closest in time.
“Neural Program Repair with Execution-based Backpropagation”
He Ye, Matias Martinez and Martin Monperrus · 2021
Closest in time.
“Exploring the Possibilities of Applying Transfer Learning Methods for Natural Language Processing in Software Development”, 2021
Wei Ding · 2021
Closest in time.
“Application of Seq2Seq Models on Code Correction”
Shan Huang, Xiao Zhou and Sang Chin · 2021
Closest in time.
“Decision Transformer: Reinforcement Learning via Sequence Modeling”
Lili Chen et al · 2021
Closest in time.
“Recognizing and Verifying Mathematical Equations using Multiplicative Differential Neural Units”
Ankur Mali, Alexander. II, Daniel Kifer and C. Giles · 2021
Closest in time.
“A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving”
Maxwell Crouse et al · 2021
Closest in time.
“Generating Bug-Fixes Using Pretrained Transformers”
Dawn Drain, Chen Wu, Alexey Svyatkovskiy and Neel Sundaresan · 2021
Closest in time.
“On the generalizability of Neural Program Models with respect to semantic-preserving program transformations”
Md Rabin et al · 2021
Closest in time.
“Self-Supervised Contrastive Learning for Code Retrieval and Summarization via Semantic-Preserving Transformations”
Nghi.. Bui, Yijun Yu and Lingxiao Jiang · 2021
Closest in time.
“Self-Supervised Bug Detection and Repair”
Miltiadis Allamanis, Henry Jackson-Flux and Marc Brockschmidt · 2021
Closest in time.
“HyperTree Proof Search for Neural Theorem Proving”
Guillaume Lample et al · 2022
Closest in time.
“Neural Transfer Learning for Repairing Security Vulnerabilities in C Code”
Zimin Chen, Steve Kommrusch and Martin Monperrus · 2022
Closest in time.