Semantic program alignment for equivalence checking

Z3: An Efficient SMT Solver

de Moura, L., & Bjørner, N. (2008) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-78800-3_24 · Cited by 6,595 · see citing works

An axiomatic basis for computer programming

Hoare, C. A. R. (1969) · Communications of the ACM · doi:10.1145/363235.363259 · Cited by 4,006 · see citing works

CVC4

Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., & Tinelli, C. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-22110-1_14 · Cited by 655 · see citing works

Translation validation for an optimizing compiler

Necula, G. C. (2000) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/349299.349314 · Cited by 490 · see citing works

Houdini, an Annotation Assistant for ESC/Java

Flanagan, C., & Leino, K. R. M. (2001) · Lecture notes in computer science · doi:10.1007/3-540-45251-6_29 · Cited by 406 · see citing works

Simple relational correctness proofs for static analyses and program transformations

Benton, N. (2004) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/964001.964003 · Cited by 358 · see citing works

Stochastic superoptimization

Schkufza, E., Sharma, R., & Aiken, A. (2013) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/2451116.2451150 · Cited by 279 · see citing works

An Evaluation of Vectorizing Compilers

Maleki, S., Gao, Y., Garzarán, M. J., Wong, T., & Padua, D. (2011) · International Conference on Parallel Architectures and Compilation Techniques (PACT) · doi:10.1109/pact.2011.68 · Cited by 222 · see citing works

Relational Verification Using Product Programs

Barthe, G., Crespo, J. M., & Kunz, C. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-21437-0_17 · Cited by 205 · see citing works

Equality saturation

Tate, R., Stepp, M., Tatlock, Z., & Lerner, S. (2009) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/1480881.1480915 · Cited by 198 · see citing works

Translation validation for a verified OS kernel

Sewell, T. A. L., Myreen, M. O., & Klein, G. (2013) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/2491956.2462183 · Cited by 142 · see citing works

Provably correct peephole optimizations with alive

Lopes, N. P., Menendez, D., Nagarakatte, S., & Regehr, J. D. (2015) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/2737924.2737965 · Cited by 131 · see citing works

Practical, Low-Effort Equivalence Verification of Real Code

Ramos, D. A., & Engler, D. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-22110-1_55 · Cited by 124 · see citing works

Automating regression verification

Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., & Ulbrich, M. (2014) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/2642937.2642987 · Cited by 122 · see citing works

Proving optimizations correct using parameterized program equivalence

Kundu, S., Tatlock, Z., & Lerner, S. (2009) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/1542476.1542513 · Cited by 113 · see citing works

CoVaC: Compiler Validation by Program Analysis of the Cross-Product

Zaks, A., & Pnueli, A. (2008) · Springer eBooks · doi:10.1007/978-3-540-68237-0_5 · Cited by 109 · see citing works

Data-driven equivalence checking

Sharma, R., Schkufza, E., Churchill, B., & Aiken, A. (2013) · Conference on Object-Oriented Programming Systems, Languages, and Applications · doi:10.1145/2509136.2509509 · Cited by 83 · see citing works

Simple relational correctness proofs for static analyses and program transformations

Benton, N. (2004) · ACM SIGPLAN Notices · doi:10.1145/982962.964003 · Cited by 73 · see citing works

Evaluating value-graph translation validation for LLVM

Tristan, J.-B., Govereau, P., & Morrisett, G. (2011) · ACM SIGPLAN Notices · doi:10.1145/1993316.1993533 · Cited by 71 · see citing works

Evaluating value-graph translation validation for LLVM

Tristan, J.-B., Govereau, P., & Morrisett, G. (2011) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/1993498.1993533 · Cited by 71 · see citing works

From relational verification to SIMD loop synthesis

Barthe, G., Crespo, J. M., Gulwani, S., Kunz, C., & Marron, M. (2013) · ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming · doi:10.1145/2442516.2442529 · Cited by 65 · see citing works

Equality-Based Translation Validator for LLVM

Stepp, M., Tate, R., & Lerner, S. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-22110-1_59 · Cited by 63 · see citing works

Stratified synthesis: automatically learning the x86-64 instruction set

Heule, S., Schkufza, E., Sharma, R., & Aiken, A. (2016) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/2908080.2908121 · Cited by 59 · see citing works

Equivalence checking of static affine programs using widening to handle recurrences

Verdoolaege, S., Janssens, G., & Bruynooghe, M. (2012) · ACM Transactions on Programming Languages and Systems · doi:10.1145/2362389.2362390 · Cited by 57 · see citing works

Stochastic superoptimization

Schkufza, E., Sharma, R., & Aiken, A. (2013) · ACM SIGARCH Computer Architecture News · doi:10.1145/2490301.2451150 · Cited by 57 · see citing works

Abstract Semantic Differencing for Numerical Programs

Partush, N., & Yahav, E. (2013) · Lecture notes in computer science · doi:10.1007/978-3-642-38856-9_14 · Cited by 50 · see citing works

Will you still compile me tomorrow? static cross-version compiler validation

Hawblitzel, C., Lahiri, S. K., Pawar, K., Hashmi, H., Gokbulut, S., Fernando, L., Detlefs, D., & Wadsworth, S. (2013) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/2491411.2491442 · Cited by 42 · see citing works

Relational Verification Through Horn Clause Transformation

Angelis, E. D., Fioravanti, F., Pettorossi, A., & Proietti, M. (2016) · Lecture notes in computer science · doi:10.1007/978-3-662-53413-7_8 · Cited by 33 · see citing works

Black-Box Equivalence Checking Across Compiler Optimizations

Dahiya, M., & Bansal, S. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-71237-6_7 · Cited by 33 · see citing works

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

Lopes, N. P., & Monteiro, J. C. (2015) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-015-0366-1 · Cited by 30 · see citing works

Translation validation for a verified OS kernel

Sewell, T. A. L., Myreen, M. O., & Klein, G. (2013) · ACM SIGPLAN Notices · doi:10.1145/2499370.2462183 · Cited by 28 · see citing works

Conditionally correct superoptimization

Sharma, R., Schkufza, E., Churchill, B., & Aiken, A. (2015) · Conference on Object-Oriented Programming Systems, Languages, and Applications · doi:10.1145/2814270.2814278 · Cited by 23 · see citing works

Automated Discovery of Simulation Between Programs

Fedyukovich, G., Gurfinkel, A., & Sharygina, N. (2015) · Lecture notes in computer science · doi:10.1007/978-3-662-48899-7_42 · Cited by 23 · see citing works

Partitioned Memory Models for Program Analysis

Wang, W., Barrett, C., & Wies, T. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-52234-0_29 · Cited by 22 · see citing works

Synchronizing Constrained Horn Clauses

Mordvinov, D., & Fedyukovich, G. (2018) · EPiC series in computing · doi:10.29007/gr5c · Cited by 22 · see citing works

Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations

Schordan, M., Lin, P., Quinlan, D., & Pouchet, L.-N. (2014) · Lecture notes in computer science · doi:10.1007/978-3-662-45231-8_41 · Cited by 22 · see citing works

Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition

Gupta, S., Saxena, A., Mahajan, A., & Bansal, S. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-94144-8_22 · Cited by 19 · see citing works

Sound Loop Superoptimization for Google Native Client

Churchill, B., Sharma, R., Bastien, J., & Aiken, A. (2017) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/3037697.3037754 · Cited by 19 · see citing works

PolyCheck: dynamic verification of iteration space transformations on affine programs

Bao, W., Krishnamoorthy, S., Pouchet, L.-N., Rastello, F., & Sadayappan, P. (2016) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/2837614.2837656 · Cited by 17 · see citing works

Data-driven equivalence checking

Sharma, R., Schkufza, E., Churchill, B., & Aiken, A. (2013) · ACM SIGPLAN Notices · doi:10.1145/2544173.2509509 · Cited by 16 · see citing works

Modeling Undefined Behaviour Semantics for Checking Equivalence Across Compiler Optimizations

Dahiya, M., & Bansal, S. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-70389-3_2 · Cited by 12 · see citing works

Conditionally correct superoptimization

Sharma, R., Schkufza, E., Churchill, B., & Aiken, A. (2015) · ACM SIGPLAN Notices · doi:10.1145/2858965.2814278 · Cited by 10 · see citing works

Relational Program Reasoning Using Compiler IR

Kiefer, M., Klebanov, V., & Ulbrich, M. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-48869-1_12 · Cited by 8 · see citing works

Validation of Loop Parallelization and Loop Vectorization Transformations

Dutta, S., Sarkar, D., Rawat, A., & Singh, K. (2016) · International Conference on Evaluation of Novel Approaches to Software Engineering · doi:10.5220/0005869501950202 · Cited by 7 · see citing works

Predicate Pairing with Abstraction for Relational Verification

Angelis, E. D., Fioravanti, F., Pettorossi, A., & Proietti, M. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-94460-9_17 · Cited by 2 · see citing works

Enhancing Predicate Pairing with Abstraction for Relational VerificationPreprint

Angelis, E. D., Fioravanti, F., Pettorossi, A., & Proietti, M. (2017) · arXiv (Cornell University) · doi:10.48550/arxiv.1709.04809 · Cited by 1 · see citing works

TASO

Jia, Z., Padon, O., Thomas, J. J., Warszawski, T., Zaharia, M., & Aiken, A. (2019) · ACM SIGOPS Symposium on Operating Systems Principles (SOSP) · doi:10.1145/3341301.3359630 · Cited by 261 · see citing works

Alive2: bounded translation validation for LLVM

Lopes, N. P., Lee, J., Hur, C.-K., Liu, Z., & Regehr, J. D. (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3453483.3454030 · Cited by 118 · see citing works

Constraint-Based Relational Verification

Unno, H., Terauchi, T., & Koskinen, E. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81685-8_35 · Cited by 48 · see citing works

ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code

Badihi, S., Akinotcho, F., Li, Y., & Rubin, J. (2020) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3368089.3409757 · Cited by 45 · see citing works

Software Verification of Hyperproperties Beyond k-Safety

Beutner, R., & Finkbeiner, B. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-13185-1_17 · Cited by 44 · see citing works

Clover: Closed-Loop Verifiable Code Generation

Sun, C., Sheng, Y., Padon, O., & Barrett, C. (2024) · Lecture Notes in Computer Science · doi:10.1007/978-3-031-65112-0_7 · Cited by 43 · see citing works

Verifix: Verified Repair of Programming Assignments

Ahmed, U. Z., Fan, Z., Yi, J., Al-Bataineh, O. I., & Roychoudhury, A. (2022) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3510418 · Cited by 33 · see citing works

Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History

Naumann, D. A. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-61470-6_7 · Cited by 21 · see citing works

Diffy: Inductive Reasoning of Array Programs Using Difference Invariants

Chakraborty, S., Gupta, A., & Unadkat, D. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81688-9_42 · Cited by 20 · see citing works

An Algebra of Alignment for Relational Verification

Antonopoulos, T., Koskinen, E., Le, T. C., Nagasamudram, R., Naumann, D. A., & Ngo, M. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3571213 · Cited by 19 · see citing works

PEQCHECK: Localized and Context-aware Checking of Functional Equivalence

Jakobs, M.-C. (2021) · IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE) · doi:10.1109/formalise52586.2021.00019 · Cited by 18 · see citing works

Knowledge Equivalence in Digital Twins of Intelligent Systems

Zhang, N., Rami Bahsoon, A., Tziritas, N., & Theodoropoulos, G. K. (2023) · ACM Transactions on Modeling and Computer Simulation · doi:10.1145/3635306 · Cited by 18 · see citing works

Hyperproperty Verification as CHC Satisfiability

Itzhaky, S., Shoham, S., & Vizel, Y. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-57267-8_9 · Cited by 16 · see citing works

Counterexample-guided correlation algorithm for translation validation

Gupta, S., Rose, A., & Bansal, S. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428289 · Cited by 14 · see citing works

Formally Verifying Optimizations with Block Simulations

Gourdin, L., Bonneau, B., Boulmé, S., Monniaux, D. P., & Bérard, A. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3622799 · Cited by 15 · see citing works

Understanding the Robustness of Transformer-Based Code Intelligence via Code Transformation: Challenges and Opportunities

Li, Y., Qi, S., Gao, C., Peng, Y., Lo, D., Lyu, M. R.-T., & Xu, Z. (2025) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2024.3524461 · Cited by 13 · see citing works

SMT-Based Translation Validation for Machine Learning Compiler

Bang, S., SeungHyeon, N., Chun, I., Jhoo, H. Y., & Lee, J. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-13188-2_19 · Cited by 12 · see citing works

Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects

Malík, V., & Vojnar, T. (2021) · IEEE International Conference on Software Testing, Verification and Validation (ICST) · doi:10.1109/icst49551.2021.00045 · Cited by 12 · see citing works

Leapfrog: certified equivalence for protocol parsers

Doenges, R., Kappé, T., Sarracino, J., Foster, N., & Morrisett, G. (2022) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3519939.3523715 · Cited by 11 · see citing works

Learning to Synthesize Relational Invariants

Wang, J., & Wang, C. (2022) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3551349.3556942 · Cited by 13 · see citing works

Alignment Completeness for Relational Hoare Logics

Nagasamudram, R., & Naumann, D. A. (2021) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics52264.2021.9470690 · Cited by 10 · see citing works

Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules

Kommrusch, S., Monperrus, M., & Pouchet, L.-N. (2023) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2023.3271065 · Cited by 9 · see citing works

Proving and Disproving Equivalence of Functional Programming Assignments

Milovančević, D., & Kunčak, V. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3591258 · Cited by 10 · see citing works

ReACC: A Retrieval-Augmented Code Completion Framework

Lu, S., Duan, N., Han, H., Guo, D., Hwang, S.-W., & Svyatkovskiy, A. (2022) · arXiv · doi:10.48550/arxiv.2203.07722 · Cited by 96 · see citing works

Input-Relational Verification of Deep Neural Networks

Banerjee, D., Xu, C., & Singh, G. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3656377 · Cited by 9 · see citing works

Formal Verification of Code Conversion: A Comprehensive Survey

Mahmoud, A. T., Mohammed, A. A., Ayman, M., Medhat, W., Selim, S., Zayed, H. H., Yousef, A. H., & Elaraby, N. (2024) · Technologies · doi:10.3390/technologies12120244 · Cited by 10 · see citing works

ParDiff: Practical Static Differential Analysis of Network Protocol Parsers

Zheng, M., Shi, Q., Liu, X., Xu, X., Yu, L., Liu, C., Wei, G., & Zhang, X. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3649854 · Cited by 9 · see citing works

A Relational Program Logic with Data Abstraction and Dynamic Framing

Banerjee, A., Nagasamudram, R., Naumann, D. A., & Nikouei, M. (2022) · ACM Transactions on Programming Languages and Systems · doi:10.1145/3551497 · Cited by 9 · see citing works

A Self-certifying Compilation Framework for WebAssembly

Namjoshi, K. S., & Xue, A. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-67067-2_7 · Cited by 9 · see citing works

Verified code generation for the polyhedral model

Courant, N., & Leroy, X. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3434321 · Cited by 9 · see citing works

Verifying Data Constraint Equivalence in FinTech Systems

Wang, C., Fan, G., Yao, P., Pan, F., & Zhang, C. (2023) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse48619.2023.00117 · Cited by 7 · see citing works

Code-Level Functional Equivalence Checking of Annotative Software Product Lines

Wang, A., Feng, N., & Chećhik, M. (2023) · International Software Product Line Conference (SPLC) · doi:10.1145/3579027.3608978 · Cited by 7 · see citing works

PEQtest: Testing Functional Equivalence

Jakobs, M.-C., & Wiesner, M. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-99429-7_11 · Cited by 7 · see citing works

NeurIPS 2020 NLC2CMD Competition: Translating Natural Language to Bash CommandsPreprint

Agarwal, M., Chakraborti, T., Fu, Q., Gros, D., Lin, X., Maene, J., Talamadupula, K., Teng, Z., & White, J. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2103.02523 · Cited by 6 · see citing works

Automated regression unit test generation for program merges

Ji, T., Chen, L., Mao, X., Yi, X., & Jiang, J. (2022) · Science China Information Sciences · doi:10.1007/s11432-019-3020-4 · Cited by 5 · see citing works

Leveraging AI for Productive and Trustworthy HPC Software: Challenges and Research Directions

Teranishi, K., Menon, H., Godoy, W. F., Balaprakash, P., Bau, D., Ben‐Nun, T., Bhatele, A. S., Franchetti, F., Franusich, M., Gamblin, T., et al. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-07612-0_47 · Cited by 4 · see citing works

Guided linking: dynamic linking without the costs

Bartell, S., Dietz, W., & Adve, V. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428213 · Cited by 4 · see citing works

Graph Neural Networks for Mapping Variables Between Programs

Orvalho, P., Piepenbrock, J., Janota, M., & Manquinho, V. M. (2023) · Frontiers in artificial intelligence and applications · doi:10.3233/faia230468 · Cited by 4 · see citing works

Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks

Chen, Q., Yu, C., Liu, R., Zhang, C., Wang, Y., Wang, K., Su, T., & Wang, L. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3649829 · Cited by 4 · see citing works

Approximate Relational Reasoning for Quantum Programs

Yan, P., Jiang, H., & Yu, N. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-65633-0_22 · Cited by 4 · see citing works

ElasticMiter: Formally Verified Dataflow Circuit Rewrites

Elakhras, A., Xu, J., Erhart, M., Ienne, P., & Josipović, L. (2025) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/3676641.3715993 · Cited by 3 · see citing works

Verifying Semantic Equivalence of Large Models with Equality Saturation

Zulkifli, K. S., Qian, W., Zhu, S., Zhou, Y., Zhang, Z., & Lou, C. (2025) · Workshop on Machine Learning and Systems (EuroMLSys) · doi:10.1145/3721146.3721943 · Cited by 3 · see citing works

KestRel: Relational Verification using E-Graphs for Program Alignment

Dickerson, R., Mukherjee, P., & Delaware, B. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720474 · Cited by 3 · see citing works

Automatic Generation of Debug Headers through BlackBox Equivalence Checking

Kurhe, V. K., Karia, P., Gupta, S., Rose, A., & Bansal, S. (2022) · Proceedings of the CGO/Proceedings of the ... CGO · doi:10.1109/cgo53902.2022.9741273 · Cited by 3 · see citing works

Fundamental Approaches to Software Engineering

Johnsen, E. B., & Wimmer, M. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-99429-7 · Cited by 3 · see citing works

Automated Verification of Consistency in Zero-Knowledge Proof Circuits

Stephens, J., Pailoor, S., & Dillig, I. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-98668-0_16 · Cited by 2 · see citing works

Automated Property Directed Self Composition

Shenoy, A., Prabhu, S., Madhukar, K., Shemer, R., & Srivas, M. K. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-45332-8_7 · Cited by 2 · see citing works

Equivalence by Canonicalization for Synthesis-Backed Refactoring

Lubin, J. P., Ferguson, J., Ye, K., Yim, J., & Chasins, S. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3656453 · Cited by 2 · see citing works

Extending Dynamic Logics with First-Class Relational Reasoning

Xiang, J., & Chong, S. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-93706-4_23 · Cited by 2 · see citing works

InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments

Orvalho, P., Janota, M., & Manquinho, V. M. (2025) · Journal of Systems and Software · doi:10.1016/j.jss.2025.112481 · Cited by 2 · see citing works

Verification of Functional Correctness of Code Diversification Techniques

Jang, J.-W., Verbeek, F., & Ravindran, B. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-76384-8_11 · Cited by 2 · see citing works

Scaling Arbitrary Android App Analyses

Pauck, F. (2022) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3551349.3561339 · Cited by 2 · see citing works

Lockstep Composition for Unbalanced Loops

Hamza, A., & Fedyukovich, G. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-30820-8_18 · Cited by 2 · see citing works

Synthesizing Efficient Memoization Algorithms

Sun, Y., Peng, X., & Xiong, Y. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3622800 · Cited by 3 · see citing works

Scalable comparison of JavaScript V8 bytecode traces

Cabrera-Arteaga, J., Monperrus, M., & Baudry, B. (2019) · Virtual Machines and Intermediate Languages for Emerging Modularization Mechanisms · doi:10.1145/3358504.3361228 · Cited by 2 · see citing works

Deductive Binary Code Verification Against Source-Code-Level Specifications

Kamkin, A., Khoroshilov, A. V., Kotsynyak, A., & Putro, P. A. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-50995-8_3 · Cited by 2 · see citing works

Using hypersafety verification for proving correctness of programming assignments

Anil, J. K., Sumanth Prabhu, S., Madhukar, K., & Venkatesh, R. (2020) · IEEE/ACM International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) · doi:10.1145/3377816.3381747 · Cited by 2 · see citing works

Scaling client-specific equivalence checking via impact boundary search

Feng, N., Mora, F., Hui, V., & Chećhik, M. (2020) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3324884.3416634 · Cited by 2 · see citing works

Learning to Superoptimize Real-world ProgramsPreprint

Shypula, A., Yin, P., Lacomis, J., Goues, C. L., Schwartz, E. J., & Neubig, G. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2109.13498 · Cited by 2 · see citing works

Invaastcluster: On Applying Invariant-Based Program Clustering to Introductory Programming AssignmentsPreprint

Orvalho, P., Janota, M., & Manquinho, V. M. (2023) · SSRN Electronic Journal · doi:10.2139/ssrn.4595235 · Cited by 2 · see citing works

Verifying relational properties using trace logic

Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovács, L., & Maffei, M. (2019) · Chalmers Research (Chalmers University of Technology) · doi:10.23919/fmcad.2019.8894277 · Cited by 21 · see citing works

Detection of Optimizations Missed by the Compiler

Zhang, Y. (2023) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3611643.3617846 · Cited by 1 · see citing works

Predicate abstraction for hyperliveness verification

Beutner, R., & Finkbeiner, B. (2025) · Formal Methods in System Design · doi:10.1007/s10703-025-00482-5 · Cited by 1 · see citing works

Contextual Equality Saturation

Drewery, A., Jensen, T. W., & Pichardie, D. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-07106-4_3 · Cited by 1 · see citing works

Are Large Language Models Smart Enough for SQL Tutoring and Assessment?

Naha, K., Rubaiat, S. Y., & Jamil, H. M. (2025) · IEEE International Conference on Advanced Learning Technologies (ICALT) · doi:10.1109/icalt64023.2025.00109 · Cited by 1 · see citing works

LOOPRAG: Enhancing Loop Transformation Optimization with Retrieval-Augmented Large Language Models

Zhi, Y., Cao, Y., Dai, J., Han, X., Pu, J., Wu, Q., Cheng, S., & Cai, M. (2026) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/3779212.3790183 · Cited by 1 · see citing works

The WhyRel Prototype for Modular Relational Verification of Pointer Programs

Nagasamudram, R., Banerjee, A., & Naumann, D. A. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-30820-8_11 · Cited by 1 · see citing works

Modeling Dynamic (De)Allocations of Local Memory for Translation Validation

Rose, A., & Bansal, S. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3649863 · Cited by 1 · see citing works

Programming Languages and Systems

Weirich, S. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-57267-8 · Cited by 1 · see citing works

Architecture of a Machine Code Deductive Verification System

GLADYSHEV, I. V., Kamkin, A., Kotsynyak, A., Putro, P. A., & Khoroshilov, A. V. (2020) · Proceedings of the Institute for System Programming of RAS · doi:10.15514/ispras-2020-32(3)-1 · Cited by 1 · see citing works

PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)Preprint

Jakobs, M.-C. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2101.09042 · Cited by 1 · see citing works

Direct Construction of Program Alignment Automata for Equivalence CheckingPreprint

Goyal, M., Azeem, M., Madhukar, K., & Venkatesh, R. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2109.01864 · Cited by 1 · see citing works

Self-Supervised Learning to Prove Equivalence Between Programs via Semantics-Preserving Rewrite RulesPreprint

Kommrusch, S., Monperrus, M., & Pouchet, L.-N. (2021) · arXiv (Cornell University) · Cited by 1 · see citing works

Reductions for Safety Proofs (Extended Version)Preprint

Farzan, A., & Vandikas, A. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1910.14619

Data Abstraction and Relational Program Logic.Preprint

Nikouei, M., Banerjee, A., & Naumann, D. A. (2019) · arXiv (Cornell University)

Evolutionary Conflict CheckingPreprint

Ji, T., Chen, L., Mao, X., Yi, X., & Jiang, J. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2009.10340

VP_TT: A value propagation based equivalence checker for testability transformations

Chouksey, R., Maddheshiya, S. K., & Karfa, C. (2021) · IET Software · doi:10.1049/sfw2.12008

Program Equivalence Checking for the Facilitation of Quantum Offloading

Speer, J., & Nurminen, J. K. (2021) · IEEE Annual Computing and Communication Workshop and Conference (CCWC) · doi:10.1109/ccwc51732.2021.9375948

Analysis and Transformation of Constrained Horn Clauses for Program Verification

Angelis, E. D., Fioravanti, F., Gallagher, J. P., Hermenegildo, M. V., Pettorossi, A., & Proietti, M. (2021) · Theory and Practice of Logic Programming · doi:10.1017/s1471068421000211

Last Diff Analyzer: Multi-language Automated Approver for Behavior-Preserving Code Revisions

Wang, Y., Welc, A., Clapp, L., & Chen, L. (2023) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3611643.3613870

Relational Denotational and Algebraic Semantics Based on UTP

Hou, Z., & Zhu, H. (2025) · Lecture notes in computer science · doi:10.1007/978-981-96-1621-3_15

WhyRel: an auto-active relational verifier

Nagasamudram, R., Banerjee, A., & Naumann, D. A. (2025) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-025-00786-1

Exact Loop Bound Analysis

Riley, D., & Fedyukovich, G. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3729323

Incremental Verification of Concurrent Programs through Refinement Constraint Adaptation

Yin, L., Li, Y., Chen, K. W., Dong, W., & Wang, J. (2025) · Proceedings of the ACM on software engineering. · doi:10.1145/3728976

Products of Recursive Programs for Hypersafety Verification

Cheng, R., & Farzan, A. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763160

Towards Compiler-Guided Static Analysis

Mikek, B. (2025) · ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) · doi:10.1145/3758316.3762823

Fast, Fine-Grained Equivalence Checking for Neural Decompilers

Dramko, L., Goues, C. L., & Schwartz, E. J. (2025) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3772368

Antarbhukti: Verifying Correctness of PLC Software During System Evolution

Bandyopadhyay, S., & Sarkar, S. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-08707-2_21

Promise: Property Mining for Sequential Synthesis

Xu, J., Cortadella, J., & Josipović, L. (2025) · doi:10.1109/iccad66269.2025.11240727

Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects

Malík, V., Vojnar, T., & Nečas, F. (2026) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3801958

Static analysis of program portability by abstract interpretation

Delmas, D. (2022) · doi:10.70675/6c6519d6zbe2az4c21zb810ze8cac31743e7

Operational and Algebraic Approaches to the Two-Run Relational System

Hou, Z., Zhu, H., & Bowen, J. P. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-16855-9_7

SemAder : Evading LLM-Based Binary Code Analysis via Structure-Semantics Joint Induction

Wang, Y., Kang, F., Shu, H., Xiong, X., & Yang, J. (2026) · ACM Transactions on Privacy and Security · doi:10.1145/3818619

Modular Reasoning About Object Relations

Greutmann, M., Eilers, M., & Müller, P. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-32526-6_6

Spatial and Temporal Decomposition for Faster Translation Validation

Mikek, B., Bommineni, C., Zhang, Q., & Reps, T. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3839512

Incremental Program Synthesis from Event Logs

Kim, J., Nicolet, V., Dodds, J., & D’Antoni, L. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3839460

PEG for Information Flow: Analysis and Incremental Reasoning

Drewery, A., Jensen, T. W., & Pichardie, D. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-40374-2_10

Direct Construction of Program Alignment Automata for Equivalence CheckingPreprint

Goyal, M., Azeem, M., Madhukar, K., & Venkatesh, R. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2109.01864 · Cited by 1 · see citing works

Two Approaches of Showing Program Equivalence CSC2108 Automated Verification Final Report

Bradel, B. J. (2008)

On the Semantic Equivalence of a Program and Any of its Intermediate Representations

Lusi, D. P. (2015) · Arizona State University Library Digital Repository (Arizona State University)

An algorithm deciding functional equivalence in a new class of program schemes

Sabelfeld, V. K. (1990) · Theoretical Computer Science · doi:10.1016/0304-3975(90)90201-r · Cited by 13 · see citing works

KestRel: Relational Verification using E-Graphs for Program Alignment

Dickerson, R., Mukherjee, P., & Delaware, B. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720474 · Cited by 3 · see citing works