diff --git a/data/NameMappings.txt b/data/NameMappings.txt index ec91540..e961493 100644 --- a/data/NameMappings.txt +++ b/data/NameMappings.txt @@ -350,3 +350,4 @@ Aleš Bizjak->Ales Bizjak Thomas Reps->Thomas W. Reps Oliver Bračevac->Oliver Bracevac Loris D'Antoni->Loris D'Antoni +V Krishna Nandivada->V. Krishna Nandivada diff --git a/data/PACMPL/2025/pacmpl9.html b/data/PACMPL/2025/pacmpl9.html index 098ab50..ebcf33f 100644 --- a/data/PACMPL/2025/pacmpl9.html +++ b/data/PACMPL/2025/pacmpl9.html @@ -1,6 +1,6 @@ -dblp: Proceedings of the ACM on Programming Languages, Volume 9 +dblp: Proceedings of the ACM on Programming Languages, Volume 9 @@ -14,21 +14,22 @@

Proceedings of the ACM on Programming Languages, Volume 9

- +

SPARQL queries 

Refine list

showing all ?? records
-

Volume 9, Number POPL, 2025

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.

+

Volume 9, Number POPL, 2025

Volume 9, Number OOPSLA1, 2025

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.

diff --git a/ui/js/data.js b/ui/js/data.js index 8c856be..460848d 100644 --- a/ui/js/data.js +++ b/ui/js/data.js @@ -1,8 +1,8 @@ -/* file data.js generated on 2025/08/05 16:46:04 +/* file data.js generated on 2025/08/07 17:19:45 456 Conferences analyzed: [ICSE 2013, ICSE 2014, ICSE 2022, ICSE 2015, ICSE 2012, ICSE 1995, ICSE 2008, ICSE 2001, ICSE 2006, ICSE 2007, ICSE 2000, ICSE 2009, ICSE 2017, ICSE 2010, ICSE 2019, ICSE 2021, ICSE 2020, ICSE 2018, ICSE 2011, ICSE 2016, ICSE 1997, ICSE 1999, ICSE 1998, ICSE 1996, ICSE 2005, ICSE 2002, ICSE 2003, ICSE 2004, OOPSLA 2013, OOPSLA 2014, OOPSLA 2022, OOPSLA 2025, OOPSLA 2024, OOPSLA 2023, OOPSLA 2015, OOPSLA 2012, OOPSLA 1995, OOPSLA 2008, OOPSLA 2001, OOPSLA 2006, OOPSLA 2007, OOPSLA 2000, OOPSLA 2009, OOPSLA 2017, OOPSLA 2010, OOPSLA 2026, OOPSLA 2019, OOPSLA 2021, OOPSLA 2020, OOPSLA 2018, OOPSLA 2011, OOPSLA 2016, OOPSLA 1997, OOPSLA 1999, OOPSLA 1998, OOPSLA 1996, OOPSLA 2005, OOPSLA 2002, OOPSLA 2003, OOPSLA 2004, PPoPP 2013, PPoPP 2014, PPoPP 2015, PPoPP 2012, PPoPP 1993, PPoPP 1995, PPoPP 2008, PPoPP 2001, PPoPP 2006, PPoPP 2007, PPoPP 2009, PPoPP 2010, PPoPP 2011, PPoPP 1997, PPoPP 1990, PPoPP 1999, PPoPP 1991, PPoPP 2005, PPoPP 2003, FSE-AE 2015, FSE-AE 2017, FSE-AE 2019, FSE-AE 2018, FSE-AE 2016, ISMM 2013, ISMM 2014, ISMM 2015, ISMM 2012, ISMM 2008, ISMM 2006, ISMM 2007, ISMM 2000, ISMM 2009, ISMM 2010, ISMM 2011, ISMM 2002, ISMM 2004, TFP 2013, TFP 2014, TFP 2022, TFP 2023, TFP 2015, TFP 2012, TFP 2008, TFP 2001, TFP 2006, TFP 2007, TFP 2000, TFP 2009, TFP 2017, TFP 2010, TFP 2019, TFP 2021, TFP 2020, TFP 2018, TFP 2011, TFP 2016, TFP 1999, TFP 2005, TFP 2003, TFP 2004, ECOOP 2013, ECOOP 2014, ECOOP 2015, ECOOP 2012, ECOOP 2008, ECOOP 2001, ECOOP 2006, ECOOP 2007, ECOOP 2000, ECOOP 2009, ECOOP 2017, ECOOP 2010, ECOOP 2019, ECOOP 2020, ECOOP 2018, ECOOP 2011, ECOOP 2016, ECOOP 1997, ECOOP 1999, ECOOP 1998, ECOOP 1996, ECOOP 2005, ECOOP 2002, ECOOP 2003, ECOOP 2004, ASE 2013, ASE 2014, ASE 2022, ASE 2015, ASE 2012, ASE 2008, ASE 2001, ASE 2006, ASE 2007, ASE 2009, ASE 2017, ASE 2010, ASE 2019, ASE 2021, ASE 2020, ASE 2018, ASE 2011, ASE 2016, ASE 2005, ASE 2002, ASE 2003, ASE 2004, OOPSLA-AE 2014, OOPSLA-AE 2015, OOPSLA-AE 2017, OOPSLA-AE 2019, OOPSLA-AE 2018, OOPSLA-AE 2016, SLE 2013, SLE 2014, SLE 2022, SLE 2015, SLE 2012, SLE 2008, SLE 2009, SLE 2017, SLE 2010, SLE 2019, SLE 2021, SLE 2020, SLE 2018, SLE 2011, SLE 2016, ICFP 2013, ICFP 2014, ICFP 2015, ICFP 2012, ICFP 2008, ICFP 2001, ICFP 2006, ICFP 2007, ICFP 2000, ICFP 2009, ICFP 2017, ICFP 2010, ICFP 2019, ICFP 2020, ICFP 2018, ICFP 2011, ICFP 2016, ICFP 1997, ICFP 1999, ICFP 1998, ICFP 1996, ICFP 2005, ICFP 2002, ICFP 2003, ICFP 2004, ESOP 2013, ESOP 2014, ESOP 2022, ESOP 2024, ESOP 2023, ESOP 2015, ESOP 2012, ESOP 1988, ESOP 1986, ESOP 1994, ESOP 1992, ESOP 2008, ESOP 2001, ESOP 2006, ESOP 2007, ESOP 2000, ESOP 2009, ESOP 2017, ESOP 2010, ESOP 2019, ESOP 2021, ESOP 2020, ESOP 2018, ESOP 2011, ESOP 2016, ESOP 1990, ESOP 1999, ESOP 1998, ESOP 1996, ESOP 2005, ESOP 2002, ESOP 2003, ESOP 2004, FSE 2013, FSE 2014, FSE 2022, FSE 2015, FSE 2012, FSE 2008, FSE 2001, FSE 2006, FSE 2007, FSE 2000, FSE 2009, FSE 2017, FSE 2010, FSE 2019, FSE 2021, FSE 2020, FSE 2018, FSE 2011, FSE 2016, FSE 1997, FSE 1999, FSE 1998, FSE 2005, FSE 2002, FSE 2003, FSE 2004, ICFP-AE 2017, ICFP-AE 2019, ICFP-AE 2018, Haskell 2013, Haskell 2014, Haskell 2015, Haskell 2012, Haskell 2008, Haskell 2006, Haskell 2007, Haskell 2009, Haskell 2017, Haskell 2010, Haskell 2019, Haskell 2021, Haskell 2020, Haskell 2018, Haskell 2011, Haskell 2016, Haskell 2005, Haskell 2003, Haskell 2004, POPL-AE 2017, POPL-AE 2019, POPL-AE 2018, POPL-AE 2016, CGO 2013, CGO 2014, CGO 2022, CGO 2015, CGO 2012, CGO 2008, CGO 2006, CGO 2007, CGO 2009, CGO 2017, CGO 2010, CGO 2019, CGO 2021, CGO 2020, CGO 2018, CGO 2011, CGO 2016, CGO 2005, CGO 2003, CGO 2004, ISSTA-AE 2017, ISSTA-AE 2019, ISSTA-AE 2018, ISSTA-AE 2016, POPL 2022, ICFP 2022, POPL 2025, POPL 2024, PLDI 2024, ICFP 2024, POPL 2023, PLDI 2023, ICFP 2023, POPL 2019, POPL 2021, ICFP 2021, POPL 2020, HOPL 2020, POPL 2018, POPL 2013, POPL 2014, POPL 2015, POPL 2012, POPL 1995, POPL 2008, POPL 2001, POPL 2006, POPL 2007, POPL 2000, POPL 2009, POPL 2017, POPL 2010, POPL 2026, POPL 2011, POPL 2016, POPL 1997, POPL 1999, POPL 1998, POPL 1996, POPL 2005, POPL 2002, POPL 2003, POPL 2004, PLDI-AE 2014, PLDI-AE 2015, PLDI-AE 2017, PLDI-AE 2019, PLDI-AE 2018, PLDI-AE 2016, ICSE-AE 2019, ICSE-AE 2020, CC 2013, CC 2014, CC 2022, CC 2015, CC 2012, CC 1988, CC 1994, CC 1992, CC 2008, CC 2001, CC 2006, CC 2007, CC 2000, CC 2009, CC 2017, CC 2010, CC 2019, CC 2021, CC 2020, CC 2018, CC 2011, CC 2016, CC 1990, CC 1999, CC 1998, CC 1996, CC 2005, CC 2002, CC 2003, CC 2004, PLDI 2013, PLDI 2014, PLDI 2022, PLDI 2025, PLDI 2015, PLDI 2012, PLDI 1995, PLDI 2008, PLDI 2001, PLDI 2006, PLDI 2007, PLDI 2000, PLDI 2009, PLDI 2017, PLDI 2010, PLDI 2019, PLDI 2021, PLDI 2020, PLDI 2018, PLDI 2011, PLDI 2016, PLDI 1997, PLDI 1999, PLDI 1998, PLDI 1996, PLDI 2005, PLDI 2002, PLDI 2003, PLDI 2004, ECOOP-AE 2015, ECOOP-AE 2017, ECOOP-AE 2019, ECOOP-AE 2018, ECOOP-AE 2016, ISSTA 2013, ISSTA 2014, ISSTA 2022, ISSTA 2015, ISSTA 2012, ISSTA 2008, ISSTA 2006, ISSTA 2007, ISSTA 2000, ISSTA 2009, ISSTA 2017, ISSTA 2010, ISSTA 2019, ISSTA 2021, ISSTA 2020, ISSTA 2018, ISSTA 2011, ISSTA 2016, ISSTA 1998, ISSTA 1996, ISSTA 2002, ISSTA 2004] - 21886 distinct authors - 3961 distinct PC Members - 18671 publications + 21974 distinct authors + 3960 distinct PC Members + 18738 publications */ /* INITIALIZE SUPPORTED CONFERENCES: */ @@ -782,6 +782,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2023}, "pages" : "337-362", "session" : "Refine list" + }, + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" } ], "committees" : [ @@ -7496,6 +7503,13 @@ list = [ { "author" : "Willow Ahrens", "publications" : [ + { + "title" : "Finch: Sparse and Structured Tensor Programming with Control Flow", + "authors" : [ "Willow Ahrens", "Teodoro Fields Collin", "Radha Patel", "Kyle Deeds", "Changwan Hong", "Saman P. Amarasinghe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1042-1072", + "session" : "" + }, { "title" : "Mechanised Hypersafety Proofs about Structured Data", "authors" : [ "Vladimir Gladshtein", "Qiyuan Zhao", "Willow Ahrens", "Saman P. Amarasinghe", "Ilya Sergey" ], @@ -9130,6 +9144,20 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-29", "session" : "" + }, + { + "title" : "Dependency-Aware Compilation for Surface Code Quantum Architectures", + "authors" : [ "Abtin Molavi", "Amanda Xu", "Swamit Tannu", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "57-84", + "session" : "" + }, + { + "title" : "Checking Observational Correctness of Database Systems", + "authors" : [ "Lauren Pick", "Amanda Xu", "Ankush Desai", "Sanjit A. Seshia", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1661-1688", + "session" : "" }, { "title" : "Synthesizing Quantum-Circuit Optimizers", @@ -13278,6 +13306,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1408-1437", "session" : "" + }, + { + "title" : "Finch: Sparse and Structured Tensor Programming with Control Flow", + "authors" : [ "Willow Ahrens", "Teodoro Fields Collin", "Radha Patel", "Kyle Deeds", "Changwan Hong", "Saman P. Amarasinghe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1042-1072", + "session" : "" }, { "title" : "NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks", @@ -14163,6 +14198,21 @@ list = [ ] }, +{ + "author" : "Pedro H. Azevedo de Amorim", + "publications" : [ + { + "title" : "Denotational Foundations for Expected Cost Analysis", + "authors" : [ "Pedro H. Azevedo de Amorim" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "280-306", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Pedro Henrique Avezedo de Amorim", "publications" : [ @@ -17982,6 +18032,21 @@ list = [ ] }, +{ + "author" : "David Aponte", + "publications" : [ + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jairo Aponte", "publications" : [ @@ -20969,6 +21034,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2023}, "pages" : "1-27", "session" : "Refine list" + }, + { + "title" : "Revealing Sources of (Memory) Errors via Backward Analysis", + "authors" : [ "Flavio Ascari", "Roberto Bruni", "Roberta Gori", "Francesco Logozzo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1321-1348", + "session" : "" } ], "committees" : [ @@ -26584,6 +26656,21 @@ list = [ ] }, +{ + "author" : "Thomas Bagrel", + "publications" : [ + { + "title" : "Destination Calculus: A Linear 𝜆-Calculus for Purely Functional Memory Writes", + "authors" : [ "Thomas Bagrel", "Arnaud Spiwack" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "253-279", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Rajive Bagrodia", "publications" : [ @@ -26723,6 +26810,21 @@ list = [ ] }, +{ + "author" : "Alexander Y. Bai", + "publications" : [ + { + "title" : "Metamorph: Synthesizing Large Objects from Dafny Specifications", + "authors" : [ "Aleksandr Fedchin", "Alexander Y. Bai", "Jeffrey S. Foster" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "759-785", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Chenggang Bai", "publications" : [ @@ -27875,6 +27977,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "CC", "year" : 2013} } ] }, +{ + "author" : "Hrishikesh Balakrishnan", + "publications" : [ + { + "title" : "FO-Complete Program Verification for Heap Logics", + "authors" : [ "Adithya Murali", "Hrishikesh Balakrishnan", "Aaron Councilman", "Parthasarathy Madhusudan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "730-758", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Rajesh Krishna Balan", "publications" : [ @@ -29190,6 +29307,21 @@ list = [ ] }, +{ + "author" : "H. M. N. Dilum Bandara", + "publications" : [ + { + "title" : "Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality", + "authors" : [ "Guanqin Zhang", "Zhenya Zhang", "H. M. N. Dilum Bandara", "Shiping Chen", "Jianjun Zhao", "Yulei Sui" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "85-112", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Nils Bandener", "publications" : [ @@ -34611,6 +34743,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice", + "authors" : [ "Jay Richards", "Daniel Wright", "Simon Cooksey", "Mark Batty" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1858-1882", + "session" : "" }, { "title" : "Library abstraction for C/C++ concurrency", @@ -34679,6 +34818,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back", + "authors" : [ "Kevin Batz", "Joost-Pieter Katoen", "Francesca Randone", "Tobias Winkler" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "421-448", + "session" : "" }, { "title" : "Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs", @@ -34982,6 +35128,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "POPL", "year" : 2016} } ] }, +{ + "author" : "Emilien Bauer", + "publications" : [ + { + "title" : "Compressed and Parallelized Structured Tensor Algebra", + "authors" : [ "Mahdi Ghorbani", "Emilien Bauer", "Tobias Grosser", "Amir Shaikhha" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1717-1745", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jörg Bauer", "publications" : [ @@ -36050,6 +36211,13 @@ list = [ { "author" : "Vincent Beardsley", "publications" : [ + { + "title" : "Carapace: Static-Dynamic Information Flow Control in Rust", + "authors" : [ "Vincent Beardsley", "Chris Xiong", "Ada Lamba", "Michael D. Bond" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "364-392", + "session" : "" + }, { "title" : "Cocoon: Static Information Flow Control in Rust", "authors" : [ "Ada Lamba", "Max Taylor", "Vincent Beardsley", "Jacob Bambeck", "Michael D. Bond", "Zhiqiang Lin" ], @@ -42533,6 +42701,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "ICSE-AE", "year" : 2020} } ] }, +{ + "author" : "Bishnu Bhusal", + "publications" : [ + { + "title" : "Checking δ-Satisfiability of Reals with Integrals", + "authors" : [ "Cody Rivera", "Bishnu Bhusal", "Rohit Chadha", "A. Prasad Sistla", "Mahesh Viswanathan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "704-729", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Laxmi Narayan Bhuyan", "publications" : [ @@ -47254,6 +47437,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2019}, "pages" : "499-524", "session" : "Security and Incremental Computation" + }, + { + "title" : "A Mechanized Semantics for Dataflow Circuits", + "authors" : [ "Tony Law", "Delphine Demange", "Sandrine Blazy" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "507-533", + "session" : "" }, { "title" : "Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler", @@ -48116,6 +48306,21 @@ list = [ ] }, +{ + "author" : "Sean Bocirnea", + "publications" : [ + { + "title" : "Type-Preserving Flat Closure Optimization", + "authors" : [ "Adam T. Geller", "Sean Bocirnea", "Chester J. F. Gould", "Paulette Koronkevich", "William J. Bowman" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "649-675", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Joshua A. Bockenek", "publications" : [ @@ -50207,6 +50412,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2004}, "pages" : "239-250", "session" : "Code Profiling" + }, + { + "title" : "Carapace: Static-Dynamic Information Flow Control in Rust", + "authors" : [ "Vincent Beardsley", "Chris Xiong", "Ada Lamba", "Michael D. Bond" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "364-392", + "session" : "" }, { "title" : "IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications", @@ -53512,6 +53724,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2016}, "pages" : "103-116", "session" : "Session 3" + }, + { + "title" : "Type-Preserving Flat Closure Optimization", + "authors" : [ "Adam T. Geller", "Sean Bocirnea", "Chester J. F. Gould", "Paulette Koronkevich", "William J. Bowman" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "649-675", + "session" : "" }, { "title" : "Indexed Types for a Statically Safe WebAssembly", @@ -54456,6 +54675,20 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation", + "authors" : [ "Philipp Schuster", "Marius Müller", "Klaus Ostermann", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1746-1773", + "session" : "" + }, + { + "title" : "The Simple Essence of Monomorphization", + "authors" : [ "Matthew Lutze", "Philipp Schuster", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1015-1041", + "session" : "" }, { "title" : "Qualifying System ", @@ -59508,6 +59741,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2023}, "pages" : "1-27", "session" : "Refine list" + }, + { + "title" : "Revealing Sources of (Memory) Errors via Backward Analysis", + "authors" : [ "Flavio Ascari", "Roberto Bruni", "Roberta Gori", "Francesco Logozzo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1321-1348", + "session" : "" }, { "title" : "Abstract extensionality: on the properties of incomplete abstract interpretations", @@ -70268,6 +70508,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-31", "session" : "" + }, + { + "title" : "Polymorphic Records for Dynamic Languages", + "authors" : [ "Giuseppe Castagna", "Loïc Peyrot" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1464-1491", + "session" : "" }, { "title" : "Polymorphic Type Inference for Dynamic Languages", @@ -72623,6 +72870,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2012}, "pages" : " 108-127", "session" : "Refine list" + }, + { + "title" : "Checking δ-Satisfiability of Reals with Integrals", + "authors" : [ "Cody Rivera", "Bishnu Bhusal", "Rohit Chadha", "A. Prasad Sistla", "Mahesh Viswanathan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "704-729", + "session" : "" }, { "title" : "Deciding accuracy of differential privacy schemes", @@ -75139,6 +75393,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2010}, "pages" : " 387-406", "session" : "Refine list" + }, + { + "title" : "Bolt-On Strong Consistency: Specification, Implementation, and Verification", + "authors" : [ "Nicholas V. Lewchenko", "Gowtham Kaki", "Bor-Yuh Evan Chang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1604-1631", + "session" : "" }, { "title" : "Historia: Refuting Callback Reachability with Message-History Logics", @@ -75498,6 +75759,21 @@ list = [ ] }, +{ + "author" : "Rui Chang", + "publications" : [ + { + "title" : "A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana", + "authors" : [ "Shenghao Yuan", "Zhuoruo Zhang", "Jiayi Lu", "David Sanán", "Rui Chang", "Yongwang Zhao" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1-27", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Stephen Chang", "publications" : [ @@ -79754,6 +80030,21 @@ list = [ ] }, +{ + "author" : "Jiasi Chen", + "publications" : [ + { + "title" : "Hambazi: Spatial Coordination Synthesis for Augmented Reality", + "authors" : [ "Yi-Zhen Tsai", "Jiasi Chen", "Mohsen Lesani" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "307-336", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jiawan Chen", "publications" : [ @@ -81881,6 +82172,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2021}, "pages" : "222-235", "session" : "Memory Optimization and Safeness" + }, + { + "title" : "Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality", + "authors" : [ "Guanqin Zhang", "Zhenya Zhang", "H. M. N. Dilum Bandara", "Shiping Chen", "Jianjun Zhao", "Yulei Sui" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "85-112", + "session" : "" } ], "committees" : [ @@ -88547,6 +88845,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "1326-1354", "session" : "" + }, + { + "title" : "Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness", + "authors" : [ "Dongjae Lee", "Janggun Lee", "Taeyoung Yoon", "Minki Cho", "Jeehoon Kang", "Chung-Kil Hur" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1267-1294", + "session" : "" }, { "title" : "Conditional Contextual Refinement", @@ -88609,6 +88914,21 @@ list = [ ] }, +{ + "author" : "Minsung Cho", + "publications" : [ + { + "title" : "Scaling Optimization over Uncertainty via Compilation", + "authors" : [ "Minsung Cho", "John Gouwar", "Steven Holtzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1546-1574", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Sungjun Cho", "publications" : [ @@ -91071,6 +91391,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2010}, "pages" : " 529-549", "session" : "Refine list" + }, + { + "title" : "Code Style Sheets: CSS for Code", + "authors" : [ "Sam Cohen", "Ravi Chugh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "196-224", + "session" : "" }, { "title" : "Live functional programming with typed holes", @@ -96018,6 +96345,21 @@ list = [ ] }, +{ + "author" : "Sam Cohen", + "publications" : [ + { + "title" : "Code Style Sheets: CSS for Code", + "authors" : [ "Sam Cohen", "Ravi Chugh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "196-224", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Sophie Cohen", "publications" : [ @@ -96919,6 +97261,21 @@ list = [ ] }, +{ + "author" : "Teodoro Fields Collin", + "publications" : [ + { + "title" : "Finch: Sparse and Structured Tensor Programming with Control Flow", + "authors" : [ "Willow Ahrens", "Teodoro Fields Collin", "Radha Patel", "Kyle Deeds", "Changwan Hong", "Saman P. Amarasinghe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1042-1072", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Peter Collingbourne", "publications" : [ @@ -98530,6 +98887,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice", + "authors" : [ "Jay Richards", "Daniel Wright", "Simon Cooksey", "Mark Batty" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1858-1882", + "session" : "" } ], "committees" : [ @@ -100810,6 +101174,21 @@ list = [ ] }, +{ + "author" : "Aaron Councilman", + "publications" : [ + { + "title" : "FO-Complete Program Verification for Heap Logics", + "authors" : [ "Adithya Murali", "Hrishikesh Balakrishnan", "Aaron Councilman", "Parthasarathy Madhusudan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "730-758", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Steve Counsell", "publications" : [ @@ -104763,6 +105142,20 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1291-1319", "session" : "" + }, + { + "title" : "Semantics of Sets of Programs", + "authors" : [ "Jinwoo Kim", "Shaan Nagy", "Thomas W. Reps", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "844-870", + "session" : "" + }, + { + "title" : "LOUD: Synthesizing Strongest and Weakest Specifications", + "authors" : [ "Kanghee Park", "Xuanyu Peng", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "956-983", + "session" : "" }, { "title" : "Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs", @@ -106129,6 +106522,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2020}, "pages" : "499-510", "session" : "Refine list" + }, + { + "title" : "Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis", + "authors" : [ "Yuchen Ji", "Ting Dai", "Zhichao Zhou", "Yutian Tang", "Jingzhu He" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1349-1377", + "session" : "" } ], "committees" : [ @@ -111135,6 +111535,21 @@ list = [ ] }, +{ + "author" : "Kyle Deeds", + "publications" : [ + { + "title" : "Finch: Sparse and Structured Tensor Programming with Control Flow", + "authors" : [ "Willow Ahrens", "Teodoro Fields Collin", "Radha Patel", "Kyle Deeds", "Changwan Hong", "Saman P. Amarasinghe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1042-1072", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Ewa Deelman", "publications" : [ @@ -111732,6 +112147,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-29", "session" : "" + }, + { + "title" : "KestRel: Relational Verification using E-Graphs for Program Alignment", + "authors" : [ "Robert Dickerson", "Prasita Mukherjee", "Benjamin Delaware" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1073-1100", + "session" : "" }, { "title" : "A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata", @@ -112126,6 +112548,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2009}, "pages" : " 207-221", "session" : "Security" + }, + { + "title" : "A Mechanized Semantics for Dataflow Circuits", + "authors" : [ "Tony Law", "Delphine Demange", "Sandrine Blazy" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "507-533", + "session" : "" }, { "title" : "Plan B: a buffered memory model for Java", @@ -113672,6 +114101,21 @@ list = [ ] }, +{ + "author" : "Anoop Deoras", + "publications" : [ + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jean-Christophe Deprez", "publications" : [ @@ -113899,6 +114343,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2015}, "pages" : "73-83", "session" : "Synthesis and Search-Based Approaches for Reactive Systems" + }, + { + "title" : "Checking Observational Correctness of Database Systems", + "authors" : [ "Lauren Pick", "Amanda Xu", "Ankush Desai", "Sanjit A. Seshia", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1661-1688", + "session" : "" }, { "title" : "Psym: Efficient Symbolic Exploration of Distributed Systems", @@ -116660,6 +117111,13 @@ list = [ { "author" : "Robert Dickerson", "publications" : [ + { + "title" : "KestRel: Relational Verification using E-Graphs for Program Alignment", + "authors" : [ "Robert Dickerson", "Prasita Mukherjee", "Benjamin Delaware" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1073-1100", + "session" : "" + }, { "title" : "Data-driven abductive inference of library specifications", "authors" : [ "Zhe Zhou", "Robert Dickerson", "Benjamin Delaware", "Suresh Jagannathan" ], @@ -119171,6 +119629,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1556-1582", "session" : "" + }, + { + "title" : "Fast Constraint Synthesis for C++ Function Templates", + "authors" : [ "Shuo Ding", "Qirun Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "225-252", + "session" : "" }, { "title" : "Automatically Reducing Privilege for Access Control Policies", @@ -121238,6 +121703,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "656-686", "session" : "" + }, + { + "title" : "Modal Effect Types", + "authors" : [ "Wenhao Tang", "Leo White", "Stephen Dolan", "Daniel Hillerström", "Sam Lindley", "Anton Lorenzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1130-1157", + "session" : "" }, { "title" : "Unboxed Data Constructors: Or, How cpp Decides a Halting Problem", @@ -122490,6 +122962,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "2057-2089", "session" : "" + }, + { + "title" : "Verification of Bit-Flip Attacks against Quantized Neural Networks", + "authors" : [ "Yedi Zhang", "Lei Huang", "Pengfei Gao", "Fu Song", "Jun Sun", "Jin Song Dong" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "984-1014", + "session" : "" }, { "title" : "Combining model checking and testing with an application to reliability prediction and distribution", @@ -124163,6 +124642,13 @@ list = [ { "author" : "Dana Drachsler-Cohen", "publications" : [ + { + "title" : "Guarding the Privacy of Label-Only Access to Neural Network Classifiers via iDP Verification", + "authors" : [ "Anan Kabaha", "Dana Drachsler-Cohen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1184-1212", + "session" : "" + }, { "title" : "Verification of Neural Networks' Global Robustness", "authors" : [ "Anan Kabaha", "Dana Drachsler-Cohen" ], @@ -140257,6 +140743,21 @@ list = [ ] }, +{ + "author" : "Le Fang", + "publications" : [ + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Lu Fang", "publications" : [ @@ -141638,6 +142139,21 @@ list = [ ] }, +{ + "author" : "Aleksandr Fedchin", + "publications" : [ + { + "title" : "Metamorph: Synthesizing Large Objects from Dafny Specifications", + "authors" : [ "Aleksandr Fedchin", "Alexander Y. Bai", "Jeffrey S. Foster" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "759-785", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Alessandro Di Federico", "publications" : [ @@ -143894,6 +144410,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "ASE", "year" : 2022} } ] }, +{ + "author" : "Yao Feng", + "publications" : [ + { + "title" : "Adaptive Shielding via Parametric Safety Proofs", + "authors" : [ "Yao Feng", "Jun Zhu", "André Platzer", "Jonathan Laurent" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "816-843", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yi Feng", "publications" : [ @@ -145471,6 +146002,13 @@ list = [ { "author" : "John K. Feser", "publications" : [ + { + "title" : "Peepco: Batch-Based Consistency Optimization", + "authors" : [ "Ivan Kuraj", "John K. Feser", "Nadia Polikarpova", "Armando Solar-Lezama" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1101-1129", + "session" : "" + }, { "title" : "Inductive Program Synthesis Guided by Observational Program Similarity", "authors" : [ "John K. Feser", "Işıl Dillig", "Armando Solar-Lezama" ], @@ -151583,6 +152121,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2016}, "pages" : "655-665", "session" : "Research Papers" + }, + { + "title" : "Metamorph: Synthesizing Large Objects from Dafny Specifications", + "authors" : [ "Aleksandr Fedchin", "Alexander Y. Bai", "Jeffrey S. Foster" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "759-785", + "session" : "" }, { "title" : "Absynthe: Abstract Interpretation-Guided Synthesis", @@ -160850,6 +161395,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2020}, "pages" : "1385-1387", "session" : "Refine list" + }, + { + "title" : "Verification of Bit-Flip Attacks against Quantized Neural Networks", + "authors" : [ "Yedi Zhang", "Lei Huang", "Pengfei Gao", "Fu Song", "Jun Sun", "Jin Song Dong" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "984-1014", + "session" : "" }, { "title" : "Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks", @@ -162837,6 +163389,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1757-1787", "session" : "" + }, + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" }, { "title" : "Horn-ICE learning for synthesizing invariants and contracts", @@ -164685,6 +165244,21 @@ list = [ ] }, +{ + "author" : "Yuhao Ge", + "publications" : [ + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Zhaoyi Ge", "publications" : [ @@ -164822,6 +165396,13 @@ list = [ { "author" : "Jacob Van Geffen", "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + }, { "title" : "Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs", "authors" : [ "Shankara Pailoor", "Yanju Chen", "Franklyn Wang", "Clara Rodríguez-Núñez", "Jacob Van Geffen", "Jason Morton", "Michael Chu", "Brian Gu", "Yu Feng", "Işıl Dillig" ], @@ -165279,6 +165860,13 @@ list = [ { "author" : "Adam T. Geller", "publications" : [ + { + "title" : "Type-Preserving Flat Closure Optimization", + "authors" : [ "Adam T. Geller", "Sean Bocirnea", "Chester J. F. Gould", "Paulette Koronkevich", "William J. Bowman" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "649-675", + "session" : "" + }, { "title" : "Indexed Types for a Statically Safe WebAssembly", "authors" : [ "Adam T. Geller", "Justin Frank", "William J. Bowman" ], @@ -167732,6 +168320,13 @@ list = [ { "author" : "Mahdi Ghorbani", "publications" : [ + { + "title" : "Compressed and Parallelized Structured Tensor Algebra", + "authors" : [ "Mahdi Ghorbani", "Emilien Bauer", "Tobias Grosser", "Amir Shaikhha" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1717-1745", + "session" : "" + }, { "title" : "Compiling Structured Tensor Algebra", "authors" : [ "Mahdi Ghorbani", "Mathieu Huot", "Shideh Hashemian", "Amir Shaikhha" ], @@ -173001,6 +173596,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "89-113", "session" : "" + }, + { + "title" : "QED in Context: An Observation Study of Proof Assistant Users", + "authors" : [ "Jessica Shi", "Cassia Torczon", "Harrison Goldstein", "Benjamin C. Pierce", "Andrew Head" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "337-363", + "session" : "" }, { "title" : "Daedalus: Safer Document Parsing", @@ -174241,6 +174843,21 @@ list = [ ] }, +{ + "author" : "Emmanuel Anaya Gonzalez", + "publications" : [ + { + "title" : "Laurel: Unblocking Automated Verification with Large Language Models", + "authors" : [ "Eric Mugnier", "Emmanuel Anaya Gonzalez", "Nadia Polikarpova", "Ranjit Jhala", "Yuanyuan Zhou" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1519-1545", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Teofilo F. Gonzalez", "publications" : [ @@ -175313,6 +175930,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2023}, "pages" : "1-27", "session" : "Refine list" + }, + { + "title" : "Revealing Sources of (Memory) Errors via Backward Analysis", + "authors" : [ "Flavio Ascari", "Roberto Bruni", "Roberta Gori", "Francesco Logozzo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1321-1348", + "session" : "" }, { "title" : "Abstract extensionality: on the properties of incomplete abstract interpretations", @@ -176442,6 +177066,21 @@ list = [ ] }, +{ + "author" : "Chester J. F. Gould", + "publications" : [ + { + "title" : "Type-Preserving Flat Closure Optimization", + "authors" : [ "Adam T. Geller", "Sean Bocirnea", "Chester J. F. Gould", "Paulette Koronkevich", "William J. Bowman" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "649-675", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Georgios I. Goumas", "publications" : [ @@ -176623,6 +177262,13 @@ list = [ { "author" : "John Gouwar", "publications" : [ + { + "title" : "Scaling Optimization over Uncertainty via Compilation", + "authors" : [ "Minsung Cho", "John Gouwar", "Steven Holtzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1546-1574", + "session" : "" + }, { "title" : "Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs", "authors" : [ "Federico Cassano", "John Gouwar", "Francesca Lucchetti", "Claire Schlesinger", "Anders Freeman", "Carolyn Jane Anderson", "Molly Q. Feldman", "Michael Greenberg", "Abhinav Jangda", "Arjun Guha" ], @@ -181489,6 +182135,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2018}, "pages" : "241-253", "session" : "Memory Usage Optimisation" + }, + { + "title" : "Compressed and Parallelized Structured Tensor Algebra", + "authors" : [ "Mahdi Ghorbani", "Emilien Bauer", "Tobias Grosser", "Amir Shaikhha" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1717-1745", + "session" : "" }, { "title" : "Guided Equality Saturation", @@ -183501,6 +184154,21 @@ list = [ ] }, +{ + "author" : "Dawu Gu", + "publications" : [ + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Dayong Gu", "publications" : [ @@ -184110,6 +184778,21 @@ list = [ ] }, +{ + "author" : "Yile Gu", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yu Gu", "publications" : [ @@ -184364,6 +185047,21 @@ list = [ ] }, +{ + "author" : "Hanqin Guan", + "publications" : [ + { + "title" : "Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles", + "authors" : [ "Zhineng Zhong", "Ziqi Zhang", "Hanqin Guan", "Ding Li" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "676-703", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Hui Guan", "publications" : [ @@ -188093,6 +188791,21 @@ list = [ ] }, +{ + "author" : "Ahan Gupta", + "publications" : [ + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Anoop Gupta", "publications" : [ @@ -192979,6 +193692,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1469-1496", "session" : "" + }, + { + "title" : "Counterexample-Guided Inference of Modular Specifications", + "authors" : [ "William T. Hallahan", "Ranjit Jhala", "Ruzica Piskac" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1689-1716", + "session" : "" }, { "title" : "Lazy counterfactual symbolic execution", @@ -200174,6 +200894,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2007}, "pages" : " 379-394", "session" : "Process Algebraic Techniques" + }, + { + "title" : "A Unifying Approach to Product Constructions for Quantitative Temporal Inference", + "authors" : [ "Kazuki Watanabe", "Sebastian Junges", "Jurriaan Rot", "Ichiro Hasuo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1575-1603", + "session" : "" }, { "title" : "Hyperstream processing systems: nonstandard modeling of continuous-time signals", @@ -201198,6 +201925,21 @@ list = [ ] }, +{ + "author" : "Musa Haydar", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Christopher M. Hayden", "publications" : [ @@ -202053,6 +202795,13 @@ list = [ "conference" : { "series" : "ICSE", "year" : 2022}, "pages" : "1669-1680", "session" : "Refine list" + }, + { + "title" : "Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis", + "authors" : [ "Yuchen Ji", "Ting Dai", "Zhichao Zhou", "Yutian Tang", "Jingzhu He" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1349-1377", + "session" : "" } ], "committees" : [ @@ -202488,6 +203237,21 @@ list = [ ] }, +{ + "author" : "Wenyu He", + "publications" : [ + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Xiao He", "publications" : [ @@ -202657,6 +203421,21 @@ list = [ ] }, +{ + "author" : "Yituo He", + "publications" : [ + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yuxiong He", "publications" : [ @@ -202740,6 +203519,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2016}, "pages" : "1133-1135", "session" : "Graduate Submissions" + }, + { + "title" : "QED in Context: An Observation Study of Proof Assistant Users", + "authors" : [ "Jessica Shi", "Cassia Torczon", "Harrison Goldstein", "Benjamin C. Pierce", "Andrew Head" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "337-363", + "session" : "" } ], "committees" : [ @@ -209199,6 +209985,13 @@ list = [ "conference" : { "series" : "TFP", "year" : 2017}, "pages" : "98-117", "session" : "Contributions" + }, + { + "title" : "Modal Effect Types", + "authors" : [ "Wenhao Tang", "Leo White", "Stephen Dolan", "Daniel Hillerström", "Sam Lindley", "Anton Lorenzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1130-1157", + "session" : "" }, { "title" : "Soundly Handling Linearity", @@ -213473,6 +214266,20 @@ list = [ { "author" : "Steven Holtzen", "publications" : [ + { + "title" : "Scaling Optimization over Uncertainty via Compilation", + "authors" : [ "Minsung Cho", "John Gouwar", "Steven Holtzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1546-1574", + "session" : "" + }, + { + "title" : "Multi-Language Probabilistic Programming", + "authors" : [ "Sam Stites", "John M. Li", "Steven Holtzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1239-1266", + "session" : "" + }, { "title" : "Bit Blasting Probabilistic Programs", "authors" : [ "Poorva Garg", "Steven Holtzen", "Guy Van den Broeck", "Todd D. Millstein" ], @@ -213863,6 +214670,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2021}, "pages" : "248-261", "session" : "Compiling Graph Algorithms, Compiling for GPUs" + }, + { + "title" : "Finch: Sparse and Structured Tensor Programming with Control Flow", + "authors" : [ "Willow Ahrens", "Teodoro Fields Collin", "Radha Patel", "Kyle Deeds", "Changwan Hong", "Saman P. Amarasinghe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1042-1072", + "session" : "" }, { "title" : "A sparse iteration space transformation framework for sparse tensor algebra", @@ -218211,6 +219025,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2021}, "pages" : "829-841", "session" : "Refine list" + }, + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" } ], "committees" : [ @@ -219775,6 +220596,13 @@ list = [ "conference" : { "series" : "PPoPP", "year" : 2009}, "pages" : " 289-290", "session" : "Posters" + }, + { + "title" : "Verification of Bit-Flip Attacks against Quantized Neural Networks", + "authors" : [ "Yedi Zhang", "Lei Huang", "Pengfei Gao", "Fu Song", "Jun Sun", "Jin Song Dong" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "984-1014", + "session" : "" }, { "title" : "PPOpenCL: a performance-portable OpenCL compiler with host and kernel thread code fusion", @@ -220271,6 +221099,21 @@ list = [ ] }, +{ + "author" : "Tianshu Huang", + "publications" : [ + { + "title" : "Unveiling Heisenbugs with Diversified Execution", + "authors" : [ "Arjun Ramesh", "Tianshu Huang", "Jaspreet Riar", "Ben L. Titzer", "Anthony Rowe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "393-420", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Tianze Huang", "publications" : [ @@ -222576,6 +223419,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "1812-1839", "session" : "" + }, + { + "title" : "Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness", + "authors" : [ "Dongjae Lee", "Janggun Lee", "Taeyoung Yoon", "Minki Cho", "Jeehoon Kang", "Chung-Kil Hur" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1267-1294", + "session" : "" }, { "title" : "Conditional Contextual Refinement", @@ -223323,6 +224173,21 @@ list = [ ] }, +{ + "author" : "Doha Hwang", + "publications" : [ + { + "title" : "PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns", + "authors" : [ "Donguk Kim", "Minseok Jeon", "Doha Hwang", "Hakjoo Oh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1378-1405", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Dongwon Hwang", "publications" : [ @@ -230656,6 +231521,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "832-863", "session" : "" + }, + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" } ], "committees" : [ @@ -233876,6 +234748,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-29", "session" : "" + }, + { + "title" : "PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns", + "authors" : [ "Donguk Kim", "Minseok Jeon", "Doha Hwang", "Hakjoo Oh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1378-1405", + "session" : "" }, { "title" : "PL4XGL: A Programming Language Approach to Explainable Graph Learning", @@ -234700,6 +235579,20 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "1446-1474", "session" : "" + }, + { + "title" : "Laurel: Unblocking Automated Verification with Large Language Models", + "authors" : [ "Eric Mugnier", "Emmanuel Anaya Gonzalez", "Nadia Polikarpova", "Ranjit Jhala", "Yuanyuan Zhou" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1519-1545", + "session" : "" + }, + { + "title" : "Counterexample-Guided Inference of Modular Specifications", + "authors" : [ "William T. Hallahan", "Ranjit Jhala", "Ruzica Piskac" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1689-1716", + "session" : "" }, { "title" : "Mechanizing Refinement Types", @@ -235275,6 +236168,21 @@ list = [ ] }, +{ + "author" : "Yuchen Ji", + "publications" : [ + { + "title" : "Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis", + "authors" : [ "Yuchen Ji", "Ting Dai", "Zhichao Zhou", "Yutian Tang", "Jingzhu He" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1349-1377", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "JulianAndres JiYang", "publications" : [ @@ -236792,6 +237700,13 @@ list = [ "conference" : { "series" : "ICSE", "year" : 2021}, "pages" : "1161-1173", "session" : "Refine list" + }, + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" } ], "committees" : [ @@ -237503,6 +238418,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "OOPSLA", "year" : 2026} } ] }, +{ + "author" : "Yuchen Jiang", + "publications" : [ + { + "title" : "Notions of Stack-Manipulating Computation and Relative Monads", + "authors" : [ "Yuchen Jiang", "Runze Xue", "Max S. New" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "563-589", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yunlian Jiang", "publications" : [ @@ -244799,6 +245729,21 @@ list = [ ] }, +{ + "author" : "Sebastian Junges", + "publications" : [ + { + "title" : "A Unifying Approach to Product Constructions for Quantitative Temporal Inference", + "authors" : [ "Kazuki Watanabe", "Sebastian Junges", "Jurriaan Rot", "Ichiro Hasuo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1575-1603", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Michael Jungmair", "publications" : [ @@ -246320,6 +247265,13 @@ list = [ { "author" : "Anan Kabaha", "publications" : [ + { + "title" : "Guarding the Privacy of Label-Only Access to Neural Network Classifiers via iDP Verification", + "authors" : [ "Anan Kabaha", "Dana Drachsler-Cohen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1184-1212", + "session" : "" + }, { "title" : "Verification of Neural Networks' Global Robustness", "authors" : [ "Anan Kabaha", "Dana Drachsler-Cohen" ], @@ -246451,6 +247403,21 @@ list = [ ] }, +{ + "author" : "Rohan Kadekodi", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Basim M. Kadhim", "publications" : [ @@ -247274,6 +248241,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2014}, "pages" : "311-324", "session" : "Dependent types" + }, + { + "title" : "Bolt-On Strong Consistency: Specification, Implementation, and Verification", + "authors" : [ "Nicholas V. Lewchenko", "Gowtham Kaki", "Bor-Yuh Evan Chang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1604-1631", + "session" : "" }, { "title" : "Verifying Indistinguishability of Privacy-Preserving Protocols", @@ -249439,6 +250413,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-31", "session" : "" + }, + { + "title" : "Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness", + "authors" : [ "Dongjae Lee", "Janggun Lee", "Taeyoung Yoon", "Minki Cho", "Jeehoon Kang", "Chung-Kil Hur" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1267-1294", + "session" : "" }, { "title" : "Modular Hardware Design of Pipelined Circuits with Hazards", @@ -251946,6 +252927,13 @@ list = [ { "author" : "Baris Kasikci", "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + }, { "title" : "Huron: hybrid false sharing detection and repair", "authors" : [ "Tanvir Ahmed Khan", "Yifan Zhao", "Gilles Pokam", "Barzan Mozafari", "Baris Kasikci" ], @@ -252516,6 +253504,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "145-174", "session" : "" + }, + { + "title" : "Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back", + "authors" : [ "Kevin Batz", "Joost-Pieter Katoen", "Francesca Randone", "Tobias Winkler" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "421-448", + "session" : "" }, { "title" : "Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs", @@ -253256,6 +254251,13 @@ list = [ { "author" : "G. A. Kavvos", "publications" : [ + { + "title" : "Adequacy for Algebraic Effects Revisited", + "authors" : [ "G. A. Kavvos" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "927-955", + "session" : "" + }, { "title" : "Modalities, cohesion, and information flow", "authors" : [ "G. A. Kavvos" ], @@ -259882,6 +260884,21 @@ list = [ ] }, +{ + "author" : "Donguk Kim", + "publications" : [ + { + "title" : "PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns", + "authors" : [ "Donguk Kim", "Minseok Jeon", "Doha Hwang", "Hakjoo Oh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1378-1405", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Dongwoo Kim", "publications" : [ @@ -260650,6 +261667,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "1326-1354", "session" : "" + }, + { + "title" : "Semantics of Sets of Programs", + "authors" : [ "Jinwoo Kim", "Shaan Nagy", "Thomas W. Reps", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "844-870", + "session" : "" }, { "title" : "Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs", @@ -269890,6 +270914,21 @@ list = [ ] }, +{ + "author" : "Paulette Koronkevich", + "publications" : [ + { + "title" : "Type-Preserving Flat Closure Optimization", + "authors" : [ "Adam T. Geller", "Sean Bocirnea", "Chester J. F. Gould", "Paulette Koronkevich", "William J. Bowman" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "649-675", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Konstantin Korovin", "publications" : [ @@ -276061,6 +277100,21 @@ list = [ ] }, +{ + "author" : "Sachit Kuhar", + "publications" : [ + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Martin Kuhlemann", "publications" : [ @@ -278029,6 +279083,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2015}, "pages" : "37-56", "session" : "Model Checking" + }, + { + "title" : "Peepco: Batch-Based Consistency Optimization", + "authors" : [ "Ivan Kuraj", "John K. Feser", "Nadia Polikarpova", "Armando Solar-Lezama" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1101-1129", + "session" : "" }, { "title" : "Complete completion using types and weights", @@ -279767,6 +280828,13 @@ list = [ { "author" : "Andreas Lööw", "publications" : [ + { + "title" : "The Simulation Semantics of Synthesisable Verilog", + "authors" : [ "Andreas Lööw" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1295-1320", + "session" : "" + }, { "title" : "Verified compilation on a verified processor", "authors" : [ "Andreas Lööw", "Ramana Kumar", "Yong Kiam Tan", "Magnus O. Myreen", "Michael Norrish", "Oskar Abrahamsson", "Anthony C. J. Fox" ], @@ -282754,6 +283822,13 @@ list = [ { "author" : "Ada Lamba", "publications" : [ + { + "title" : "Carapace: Static-Dynamic Information Flow Control in Rust", + "authors" : [ "Vincent Beardsley", "Chris Xiong", "Ada Lamba", "Michael D. Bond" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "364-392", + "session" : "" + }, { "title" : "Cocoon: Static Information Flow Control in Rust", "authors" : [ "Ada Lamba", "Max Taylor", "Vincent Beardsley", "Jacob Bambeck", "Michael D. Bond", "Zhiqiang Lin" ], @@ -285914,6 +286989,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "OOPSLA", "year" : 2026} } ] }, +{ + "author" : "Jonathan Laurent", + "publications" : [ + { + "title" : "Adaptive Shielding via Parametric Safety Proofs", + "authors" : [ "Yao Feng", "Jun Zhu", "André Platzer", "Jonathan Laurent" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "816-843", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Mickaël Laurent", "publications" : [ @@ -286415,6 +287505,21 @@ list = [ ] }, +{ + "author" : "Tony Law", + "publications" : [ + { + "title" : "A Mechanized Semantics for Dataflow Circuits", + "authors" : [ "Tony Law", "Delphine Demange", "Sandrine Blazy" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "507-533", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Julia L. Lawall", "publications" : [ @@ -287681,6 +288786,13 @@ list = [ "conference" : { "series" : "ECOOP", "year" : 2010}, "pages" : " 1", "session" : "Keynote 1" + }, + { + "title" : "Soundness of Predictive Concurrency Analyses", + "authors" : [ "Shuyang Liu", "Doug Lea", "Jens Palsberg" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "590-616", + "session" : "" } ], "committees" : [ @@ -288732,6 +289844,13 @@ list = [ { "author" : "Dongjae Lee", "publications" : [ + { + "title" : "Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness", + "authors" : [ "Dongjae Lee", "Janggun Lee", "Taeyoung Yoon", "Minki Cho", "Jeehoon Kang", "Chung-Kil Hur" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1267-1294", + "session" : "" + }, { "title" : "Refinement Composition Logic", "authors" : [ "Youngju Song", "Dongjae Lee" ], @@ -289449,6 +290568,13 @@ list = [ { "author" : "Janggun Lee", "publications" : [ + { + "title" : "Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness", + "authors" : [ "Dongjae Lee", "Janggun Lee", "Taeyoung Yoon", "Minki Cho", "Jeehoon Kang", "Chung-Kil Hur" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1267-1294", + "session" : "" + }, { "title" : "A Proof Recipe for Linearizability in Relaxed Memory Separation Logic", "authors" : [ "Sunho Park", "Jaewoo Kim", "Ike Mulder", "Jaehwang Jung", "Janggun Lee", "Robbert Krebbers", "Jeehoon Kang" ], @@ -290389,6 +291515,21 @@ list = [ ] }, +{ + "author" : "Shaun Christopher Lee", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Shinn-Der Lee", "publications" : [ @@ -294158,6 +295299,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "832-863", "session" : "" + }, + { + "title" : "Hambazi: Spatial Coordination Synthesis for Augmented Reality", + "authors" : [ "Yi-Zhen Tsai", "Jiasi Chen", "Mohsen Lesani" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "307-336", + "session" : "" }, { "title" : "Hamsaz: replication coordination analysis and synthesis", @@ -295550,6 +296698,13 @@ list = [ "conference" : { "series" : "ICSE", "year" : 2018}, "pages" : "1160-1170", "session" : "Inference and invariants" + }, + { + "title" : "Bolt-On Strong Consistency: Specification, Implementation, and Verification", + "authors" : [ "Nicholas V. Lewchenko", "Gowtham Kaki", "Bor-Yuh Evan Chang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1604-1631", + "session" : "" }, { "title" : "Sequential programming for replicated data stores", @@ -296877,6 +298032,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2015}, "pages" : "958-961", "session" : "Tool Demonstrations" + }, + { + "title" : "Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles", + "authors" : [ "Zhineng Zhong", "Ziqi Zhang", "Hanqin Guan", "Ding Li" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "676-703", + "session" : "" }, { "title" : "Calculating source line level energy information for Android applications", @@ -296945,6 +298107,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2024}, "pages" : "176-205", "session" : "Bidirectional Typing and Session Types" + }, + { + "title" : "Characterizing Implementability of Global Protocols with Infinite States and Data", + "authors" : [ "Elaine Li", "Felix Stutz", "Thomas Wies", "Damien Zufferey" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1434-1463", + "session" : "" } ], "committees" : [ @@ -297534,6 +298703,21 @@ list = [ ] }, +{ + "author" : "Haoran Li", + "publications" : [ + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Haoyu Li", "publications" : [ @@ -298157,6 +299341,13 @@ list = [ { "author" : "John M. Li", "publications" : [ + { + "title" : "Multi-Language Probabilistic Programming", + "authors" : [ "Sam Stites", "John M. Li", "Steven Holtzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1239-1266", + "session" : "" + }, { "title" : "Lilac: A Modal Separation Logic for Conditional Probability", "authors" : [ "John M. Li", "Amal J. Ahmed", "Steven Holtzen" ], @@ -300204,6 +301395,21 @@ list = [ ] }, +{ + "author" : "Tianchi Li", + "publications" : [ + { + "title" : "Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences", + "authors" : [ "Tianchi Li", "Xin Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1774-1801", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Tong Li", "publications" : [ @@ -300580,6 +301786,13 @@ list = [ { "author" : "Wu Angela Li", "publications" : [ + { + "title" : "Efficient Algorithms for the Uniform Tokenization Problem", + "authors" : [ "Wu Angela Li", "Konstantinos Mamouras" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1492-1518", + "session" : "" + }, { "title" : "Static Analysis for Checking the Disambiguation Robustness of Regular Expressions", "authors" : [ "Konstantinos Mamouras", "Alexis Le Glaunec", "Wu Angela Li", "Agnishom Chattopadhyay" ], @@ -302973,6 +304186,13 @@ list = [ "conference" : { "series" : "ICSE", "year" : 2022}, "pages" : "2253-2265", "session" : "Refine list" + }, + { + "title" : "API-Guided Dataset Synthesis to Finetune Large Code Models", + "authors" : [ "Zongjie Li", "Daoyuan Wu", "Shuai Wang", "Zhendong Su" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "786-815", + "session" : "" } ], "committees" : [ @@ -303054,6 +304274,21 @@ list = [ ] }, +{ + "author" : "Qihao Lian", + "publications" : [ + { + "title" : "Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials", + "authors" : [ "Qihao Lian", "Di Wang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1406-1433", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Ruiqi Lian", "publications" : [ @@ -307614,6 +308849,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1639-1667", "session" : "" + }, + { + "title" : "Modal Effect Types", + "authors" : [ "Wenhao Tang", "Leo White", "Stephen Dolan", "Daniel Hillerström", "Sam Lindley", "Anton Lorenzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1130-1157", + "session" : "" }, { "title" : "Soundly Handling Linearity", @@ -311596,6 +312838,13 @@ list = [ "conference" : { "series" : "ICSE", "year" : 2022}, "pages" : "2043-2055", "session" : "Refine list" + }, + { + "title" : "Soundness of Predictive Concurrency Analyses", + "authors" : [ "Shuyang Liu", "Doug Lea", "Jens Palsberg" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "590-616", + "session" : "" } ], "committees" : [ @@ -312286,6 +313535,21 @@ list = [ ] }, +{ + "author" : "Xinxin Liu", + "publications" : [ + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Xinyu Liu", "publications" : [ @@ -316276,6 +317540,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2010}, "pages" : " 708-725", "session" : "JIT compilation and tools" + }, + { + "title" : "Revealing Sources of (Memory) Errors via Backward Analysis", + "authors" : [ "Flavio Ascari", "Roberto Bruni", "Roberta Gori", "Francesco Logozzo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1321-1348", + "session" : "" }, { "title" : "Tracing compilation by abstract interpretation", @@ -317758,6 +319029,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2022}, "pages" : "357-380", "session" : "" + }, + { + "title" : "Modal Effect Types", + "authors" : [ "Wenhao Tang", "Leo White", "Stephen Dolan", "Daniel Hillerström", "Sam Lindley", "Anton Lorenzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1130-1157", + "session" : "" }, { "title" : "The Functional Essence of Imperative Binary Search Trees", @@ -318179,6 +319457,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2016}, "pages" : "883-894", "session" : "Research Papers" + }, + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" }, { "title" : "History-driven build failure fixing: how far are we", @@ -319064,6 +320349,21 @@ list = [ ] }, +{ + "author" : "Jiayi Lu", + "publications" : [ + { + "title" : "A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana", + "authors" : [ "Shenghao Yuan", "Zhuoruo Zhang", "Jiayi Lu", "David Sanán", "Rui Chang", "Yongwang Zhao" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1-27", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jie Lu", "publications" : [ @@ -320047,6 +321347,21 @@ list = [ ] }, +{ + "author" : "Yunping Lu", + "publications" : [ + { + "title" : "JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach", + "authors" : [ "Hanzhang Wang", "Wei Peng", "Wenwen Wang", "Yunping Lu", "Pen-Chung Yew", "Weihua Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "113-142", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yutong Lu", "publications" : [ @@ -322960,6 +324275,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-31", "session" : "" + }, + { + "title" : "The Simple Essence of Monomorphization", + "authors" : [ "Matthew Lutze", "Philipp Schuster", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1015-1041", + "session" : "" }, { "title" : "Associated Effects: Flexible Abstractions for Effectful Programming", @@ -324624,6 +325946,13 @@ list = [ { "author" : "Marius Müller", "publications" : [ + { + "title" : "Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation", + "authors" : [ "Philipp Schuster", "Marius Müller", "Klaus Ostermann", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1746-1773", + "session" : "" + }, { "title" : "Grokking the Sequent Calculus (Functional Pearl)", "authors" : [ "David Binder", "Marco Tzschentke", "Marius Müller", "Klaus Ostermann" ], @@ -325956,6 +327285,21 @@ list = [ ] }, +{ + "author" : "Xiaofei Ma", + "publications" : [ + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Xiaosong Ma", "publications" : [ @@ -327628,6 +328972,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1873-1902", "session" : "" + }, + { + "title" : "FO-Complete Program Verification for Heap Logics", + "authors" : [ "Adithya Murali", "Hrishikesh Balakrishnan", "Aaron Councilman", "Parthasarathy Madhusudan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "730-758", + "session" : "" }, { "title" : "Predictable Verification using Intrinsic Definitions", @@ -332180,6 +333531,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2016}, "pages" : "282-309", "session" : "Refine list" + }, + { + "title" : "Efficient Algorithms for the Uniform Tokenization Problem", + "authors" : [ "Wu Angela Li", "Konstantinos Mamouras" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1492-1518", + "session" : "" }, { "title" : "Efficient Matching of Regular Expressions with Lookaround Assertions", @@ -348380,6 +349738,20 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "832-863", "session" : "" + }, + { + "title" : "Automated Verification of Soundness of DNN Certifiers", + "authors" : [ "Avaljot Singh", "Yasmin Sarita", "Charith Mendis", "Gagandeep Singh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1802-1830", + "session" : "" + }, + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" }, { "title" : "goSLP: globally optimized superword level parallelism framework", @@ -358528,6 +359900,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2020}, "pages" : "1596-1600", "session" : "Tool Demonstrations" + }, + { + "title" : "Dependency-Aware Compilation for Surface Code Quantum Architectures", + "authors" : [ "Abtin Molavi", "Amanda Xu", "Swamit Tannu", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "57-84", + "session" : "" }, { "title" : "Synthesizing Quantum-Circuit Optimizers", @@ -359868,6 +361247,21 @@ list = [ ] }, +{ + "author" : "Arjan J. Mooij", + "publications" : [ + { + "title" : "Language-Parametric Reference Synthesis", + "authors" : [ "Daniël A. A. Pelsmaeker", "Aron Zwaan", "Casper Bach Poulsen", "Arjan J. Mooij" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1213-1238", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Benjamin Moon", "publications" : [ @@ -364833,6 +366227,21 @@ list = [ ] }, +{ + "author" : "Eric Mugnier", + "publications" : [ + { + "title" : "Laurel: Unblocking Automated Verification with Large Language Models", + "authors" : [ "Eric Mugnier", "Emmanuel Anaya Gonzalez", "Nadia Polikarpova", "Ranjit Jhala", "Yuanyuan Zhou" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1519-1545", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Rick Mugridge", "publications" : [ @@ -365018,6 +366427,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "PLDI", "year" : 2025} } ] }, +{ + "author" : "Prasita Mukherjee", + "publications" : [ + { + "title" : "KestRel: Relational Verification using E-Graphs for Program Alignment", + "authors" : [ "Robert Dickerson", "Prasita Mukherjee", "Benjamin Delaware" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1073-1100", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Shubhendu S. Mukherjee", "publications" : [ @@ -365649,6 +367073,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1873-1902", "session" : "" + }, + { + "title" : "FO-Complete Program Verification for Heap Logics", + "authors" : [ "Adithya Murali", "Hrishikesh Balakrishnan", "Aaron Councilman", "Parthasarathy Madhusudan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "730-758", + "session" : "" }, { "title" : "Predictable Verification using Intrinsic Definitions", @@ -369476,6 +370907,13 @@ list = [ { "author" : "Kartik Nagar", "publications" : [ + { + "title" : "Automatically Verifying Replication-Aware Linearizability", + "authors" : [ "Vimala Soundarapandian", "Kartik Nagar", "Aseem Rastogi", "K. C. Sivaramakrishnan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "871-897", + "session" : "" + }, { "title" : "Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models", "authors" : [ "Kartik Nagar", "Anmol Sahoo", "Romit Roy Chowdhury", "Suresh Jagannathan" ], @@ -370106,6 +371544,13 @@ list = [ { "author" : "Shaan Nagy", "publications" : [ + { + "title" : "Semantics of Sets of Programs", + "authors" : [ "Jinwoo Kim", "Shaan Nagy", "Thomas W. Reps", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "844-870", + "session" : "" + }, { "title" : "Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs", "authors" : [ "Shaan Nagy", "Jinwoo Kim", "Thomas W. Reps", "Loris D'Antoni" ], @@ -371665,16 +373110,6 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "PLDI", "year" : 2024} } ] }, -{ - "author" : "V Krishna Nandivada", - "publications" : [ - - ], - "committees" : [ - { "role" : "PC Member", "conference" : { "series" : "OOPSLA", "year" : 2025} }, - { "role" : "PC Member", "conference" : { "series" : "PLDI", "year" : 2024} } - ] -}, { "author" : "V. Krishna Nandivada", "publications" : [ @@ -371712,6 +373147,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2005}, "pages" : "37-48", "session" : "Virtual Machine Technologies" + }, + { + "title" : "IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis", + "authors" : [ "Aman Nougrahiya", "V. Krishna Nandivada" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "617-648", + "session" : "" }, { "title" : "Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes", @@ -371771,7 +373213,9 @@ list = [ } ], "committees" : [ - { "role" : "PC Member", "conference" : { "series" : "CC", "year" : 2019} } + { "role" : "PC Member", "conference" : { "series" : "OOPSLA", "year" : 2025} }, + { "role" : "PC Member", "conference" : { "series" : "CC", "year" : 2019} }, + { "role" : "PC Member", "conference" : { "series" : "PLDI", "year" : 2024} } ] }, { @@ -373752,6 +375196,21 @@ list = [ ] }, +{ + "author" : "Ian Neal", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Iulian Neamtiu", "publications" : [ @@ -375586,6 +377045,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "772-801", "session" : "" + }, + { + "title" : "Notions of Stack-Manipulating Computation and Relative Monads", + "authors" : [ "Yuchen Jiang", "Runze Xue", "Max S. New" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "563-589", + "session" : "" }, { "title" : "Gradual Typing for Effect Handlers", @@ -383611,6 +385077,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "FSE", "year" : 2003} } ] }, +{ + "author" : "Aman Nougrahiya", + "publications" : [ + { + "title" : "IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis", + "authors" : [ "Aman Nougrahiya", "V. Krishna Nandivada" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "617-648", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Adel Noureddine", "publications" : [ @@ -386813,6 +388294,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2022}, "pages" : "1-29", "session" : "" + }, + { + "title" : "PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns", + "authors" : [ "Donguk Kim", "Minseok Jeon", "Doha Hwang", "Hakjoo Oh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1378-1405", + "session" : "" }, { "title" : "PL4XGL: A Programming Language Approach to Explainable Graph Learning", @@ -391639,6 +393127,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2022}, "pages" : "438-465", "session" : "" + }, + { + "title" : "Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation", + "authors" : [ "Philipp Schuster", "Marius Müller", "Klaus Ostermann", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1746-1773", + "session" : "" }, { "title" : "Deriving Dependently-Typed OOP from First Principles", @@ -396329,6 +397824,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2003}, "pages" : " 198-207", "session" : "Validation and verification" + }, + { + "title" : "Soundness of Predictive Concurrency Analyses", + "authors" : [ "Shuyang Liu", "Doug Lea", "Jens Palsberg" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "590-616", + "session" : "" }, { "title" : "Compiling Conditional Quantum Gates without Using Helper Qubits", @@ -399625,6 +401127,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2020}, "pages" : "647-658", "session" : "Refine list" + }, + { + "title" : "Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation", + "authors" : [ "Jihee Park", "Insu Yun", "Sukyoung Ryu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "898-926", + "session" : "" } ], "committees" : [ @@ -399769,6 +401278,13 @@ list = [ { "author" : "Kanghee Park", "publications" : [ + { + "title" : "LOUD: Synthesizing Strongest and Weakest Specifications", + "authors" : [ "Kanghee Park", "Xuanyu Peng", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "956-983", + "session" : "" + }, { "title" : "Synthesizing Specifications", "authors" : [ "Kanghee Park", "Loris D'Antoni", "Thomas W. Reps" ], @@ -402172,6 +403688,21 @@ list = [ ] }, +{ + "author" : "Radha Patel", + "publications" : [ + { + "title" : "Finch: Sparse and Structured Tensor Programming with Control Flow", + "authors" : [ "Willow Ahrens", "Teodoro Fields Collin", "Radha Patel", "Kyle Deeds", "Changwan Hong", "Saman P. Amarasinghe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1042-1072", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Sanjay Patel", "publications" : [ @@ -404408,6 +405939,21 @@ list = [ ] }, +{ + "author" : "Anurudh Peduri", + "publications" : [ + { + "title" : "QbC: Quantum Correctness by Construction", + "authors" : [ "Anurudh Peduri", "Ina Schaefer", "Michael Walter" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "534-562", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Daniel Peebles", "publications" : [ @@ -405027,6 +406573,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Language-Parametric Reference Synthesis", + "authors" : [ "Daniël A. A. Pelsmaeker", "Aron Zwaan", "Casper Bach Poulsen", "Arjan J. Mooij" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1213-1238", + "session" : "" } ], "committees" : [ @@ -405345,6 +406898,21 @@ list = [ ] }, +{ + "author" : "Wei Peng", + "publications" : [ + { + "title" : "JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach", + "authors" : [ "Hanzhang Wang", "Wei Peng", "Wenwen Wang", "Yunping Lu", "Pen-Chung Yew", "Weihua Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "113-142", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Xiao Peng", "publications" : [ @@ -405650,6 +407218,13 @@ list = [ { "author" : "Xuanyu Peng", "publications" : [ + { + "title" : "LOUD: Synthesizing Strongest and Weakest Specifications", + "authors" : [ "Kanghee Park", "Xuanyu Peng", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "956-983", + "session" : "" + }, { "title" : "Synthesizing Efficient Memoization Algorithms", "authors" : [ "Yican Sun", "Xuanyu Peng", "Yingfei Xiong" ], @@ -409448,6 +411023,21 @@ list = [ ] }, +{ + "author" : "Loïc Peyrot", + "publications" : [ + { + "title" : "Polymorphic Records for Dynamic Languages", + "authors" : [ "Giuseppe Castagna", "Loïc Peyrot" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1464-1491", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "John Peyton", "publications" : [ @@ -411497,6 +413087,13 @@ list = [ { "author" : "Lauren Pick", "publications" : [ + { + "title" : "Checking Observational Correctness of Database Systems", + "authors" : [ "Lauren Pick", "Amanda Xu", "Ankush Desai", "Sanjit A. Seshia", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1661-1688", + "session" : "" + }, { "title" : "Psym: Efficient Symbolic Exploration of Distributed Systems", "authors" : [ "Lauren Pick", "Ankush Desai", "Aarti Gupta" ], @@ -412042,6 +413639,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "89-113", "session" : "" + }, + { + "title" : "QED in Context: An Observation Study of Proof Assistant Users", + "authors" : [ "Jessica Shi", "Cassia Torczon", "Harrison Goldstein", "Benjamin C. Pierce", "Andrew Head" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "337-363", + "session" : "" }, { "title" : "Stream Types", @@ -413902,6 +415506,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1469-1496", "session" : "" + }, + { + "title" : "Counterexample-Guided Inference of Modular Specifications", + "authors" : [ "William T. Hallahan", "Ranjit Jhala", "Ruzica Piskac" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1689-1716", + "session" : "" }, { "title" : "PyDex: Repairing Bugs in Introductory Python Assignments using LLMs", @@ -414899,6 +416510,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2020}, "pages" : "84-111", "session" : "Refine list" + }, + { + "title" : "Adaptive Shielding via Parametric Safety Proofs", + "authors" : [ "Yao Feng", "Jun Zhu", "André Platzer", "Jonathan Laurent" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "816-843", + "session" : "" }, { "title" : "VeriPhy: verified controller executables from verified cyber-physical system models", @@ -416389,6 +418007,20 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2022}, "pages" : "23-51", "session" : "" + }, + { + "title" : "Laurel: Unblocking Automated Verification with Large Language Models", + "authors" : [ "Eric Mugnier", "Emmanuel Anaya Gonzalez", "Nadia Polikarpova", "Ranjit Jhala", "Yuanyuan Zhou" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1519-1545", + "session" : "" + }, + { + "title" : "Peepco: Batch-Based Consistency Optimization", + "authors" : [ "Ivan Kuraj", "John K. Feser", "Nadia Polikarpova", "Armando Solar-Lezama" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1101-1129", + "session" : "" }, { "title" : "Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis", @@ -419786,6 +421418,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1903-1932", "session" : "" + }, + { + "title" : "Language-Parametric Reference Synthesis", + "authors" : [ "Daniël A. A. Pelsmaeker", "Aron Zwaan", "Casper Bach Poulsen", "Arjan J. Mooij" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1213-1238", + "session" : "" }, { "title" : "Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects", @@ -426140,6 +427779,13 @@ list = [ { "author" : "Andrew Quinn", "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + }, { "title" : "Execution reconstruction: harnessing failure reoccurrences for failure reproduction", "authors" : [ "Gefei Zuo", "Jiacheng Ma", "Andrew Quinn", "Pramod Bhatotia", "Pedro Fonseca", "Baris Kasikci" ], @@ -428532,6 +430178,21 @@ list = [ ] }, +{ + "author" : "Shanto Rahman", + "publications" : [ + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Kia Rahmani", "publications" : [ @@ -431349,6 +433010,21 @@ list = [ ] }, +{ + "author" : "Arjun Ramesh", + "publications" : [ + { + "title" : "Unveiling Heisenbugs with Diversified Execution", + "authors" : [ "Arjun Ramesh", "Tianshu Huang", "Jaspreet Riar", "Ben L. Titzer", "Anthony Rowe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "393-420", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Mathangi Ramesh", "publications" : [ @@ -432143,6 +433819,13 @@ list = [ { "author" : "Francesca Randone", "publications" : [ + { + "title" : "Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back", + "authors" : [ "Kevin Batz", "Joost-Pieter Katoen", "Francesca Randone", "Tobias Winkler" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "421-448", + "session" : "" + }, { "title" : "Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures", "authors" : [ "Francesca Randone", "Luca Bortolussi", "Emilio Incerto", "Mirco Tribastone" ], @@ -433306,6 +434989,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2019}, "pages" : "30-59", "session" : "Program Verification" + }, + { + "title" : "Automatically Verifying Replication-Aware Linearizability", + "authors" : [ "Vimala Soundarapandian", "Kartik Nagar", "Aseem Rastogi", "K. C. Sivaramakrishnan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "871-897", + "session" : "" }, { "title" : "Verified low-level programming embedded in F", @@ -434330,6 +436020,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2020}, "pages" : "737-749", "session" : "Fuzzing" + }, + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" }, { "title" : "CYCLE: Learning to Self-Refine the Code Generation", @@ -438407,6 +440104,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1291-1319", "session" : "" + }, + { + "title" : "Semantics of Sets of Programs", + "authors" : [ "Jinwoo Kim", "Shaan Nagy", "Thomas W. Reps", "Loris D'Antoni" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "844-870", + "session" : "" }, { "title" : "Newtonian Program Analysis of Probabilistic Programs", @@ -439502,6 +441206,21 @@ list = [ ] }, +{ + "author" : "Jaspreet Riar", + "publications" : [ + { + "title" : "Unveiling Heisenbugs with Diversified Execution", + "authors" : [ "Arjun Ramesh", "Tianshu Huang", "Jaspreet Riar", "Ben L. Titzer", "Anthony Rowe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "393-420", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Colin Riba", "publications" : [ @@ -440098,6 +441817,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "PLDI-AE", "year" : 2014} } ] }, +{ + "author" : "Jay Richards", + "publications" : [ + { + "title" : "Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice", + "authors" : [ "Jay Richards", "Daniel Wright", "Simon Cooksey", "Mark Batty" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1858-1882", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "John T. Richards", "publications" : [ @@ -442782,6 +444516,13 @@ list = [ { "author" : "Cody Rivera", "publications" : [ + { + "title" : "Checking δ-Satisfiability of Reals with Integrals", + "authors" : [ "Cody Rivera", "Bishnu Bhusal", "Rohit Chadha", "A. Prasad Sistla", "Mahesh Viswanathan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "704-729", + "session" : "" + }, { "title" : "Predictable Verification using Intrinsic Definitions", "authors" : [ "Adithya Murali", "Cody Rivera", "Parthasarathy Madhusudan" ], @@ -448432,6 +450173,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2022}, "pages" : "575-602", "session" : "Refine list" + }, + { + "title" : "A Unifying Approach to Product Constructions for Quantitative Temporal Inference", + "authors" : [ "Kazuki Watanabe", "Sebastian Junges", "Jurriaan Rot", "Ichiro Hasuo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1575-1603", + "session" : "" } ], "committees" : [ @@ -449773,6 +451521,21 @@ list = [ ] }, +{ + "author" : "Anthony Rowe", + "publications" : [ + { + "title" : "Unveiling Heisenbugs with Diversified Execution", + "authors" : [ "Arjun Ramesh", "Tianshu Huang", "Jaspreet Riar", "Ben L. Titzer", "Anthony Rowe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "393-420", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Reuben Rowe", "publications" : [ @@ -454069,6 +455832,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2021}, "pages" : "1129-1140", "session" : "Programming Languages" + }, + { + "title" : "Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation", + "authors" : [ "Jihee Park", "Insu Yun", "Sukyoung Ryu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "898-926", + "session" : "" }, { "title" : "Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation", @@ -457656,6 +459426,21 @@ list = [ ] }, +{ + "author" : "Ayman Said", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Mahmoud Said", "publications" : [ @@ -459980,6 +461765,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "2057-2089", "session" : "" + }, + { + "title" : "A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana", + "authors" : [ "Shenghao Yuan", "Zhuoruo Zhang", "Jiayi Lu", "David Sanán", "Rui Chang", "Yongwang Zhao" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1-27", + "session" : "" } ], "committees" : [ @@ -462256,6 +464048,13 @@ list = [ { "author" : "Yasmin Sarita", "publications" : [ + { + "title" : "Automated Verification of Soundness of DNN Certifiers", + "authors" : [ "Avaljot Singh", "Yasmin Sarita", "Charith Mendis", "Gagandeep Singh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1802-1830", + "session" : "" + }, { "title" : "ApproxHPVM: a portable compiler IR for accuracy-aware optimizations", "authors" : [ "Hashim Sharif", "Prakalp Srivastava", "Muhammad Huzaifa", "Maria Kotsifakou", "Keyur Joshi", "Yasmin Sarita", "Nathan Zhao", "Vikram S. Adve", "Sasa Misailovic", "Sarita V. Adve" ], @@ -465626,6 +467425,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2017}, "pages" : "291-302", "session" : "Research Papers" + }, + { + "title" : "QbC: Quantum Correctness by Construction", + "authors" : [ "Anurudh Peduri", "Ina Schaefer", "Michael Walter" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "534-562", + "session" : "" } ], "committees" : [ @@ -469992,6 +471798,20 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation", + "authors" : [ "Philipp Schuster", "Marius Müller", "Klaus Ostermann", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1746-1773", + "session" : "" + }, + { + "title" : "The Simple Essence of Monomorphization", + "authors" : [ "Matthew Lutze", "Philipp Schuster", "Jonathan Immanuel Brachthäuser" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1015-1041", + "session" : "" }, { "title" : "Back to Direct Style: Typed and Tight", @@ -474244,6 +476064,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2022}, "pages" : "886-901", "session" : "" + }, + { + "title" : "Inductive Synthesis of Inductive Heap Predicates", + "authors" : [ "Ziyi Yang", "Ilya Sergey" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "169-195", + "session" : "" }, { "title" : "Mechanised Hypersafety Proofs about Structured Data", @@ -474923,6 +476750,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2017}, "pages" : "649-660", "session" : "Research Papers" + }, + { + "title" : "Checking Observational Correctness of Database Systems", + "authors" : [ "Lauren Pick", "Amanda Xu", "Ankush Desai", "Sanjit A. Seshia", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1661-1688", + "session" : "" }, { "title" : "Message Chains for Distributed System Verification", @@ -476540,6 +478374,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1-33", "session" : "" + }, + { + "title" : "Compressed and Parallelized Structured Tensor Algebra", + "authors" : [ "Mahdi Ghorbani", "Emilien Bauer", "Tobias Grosser", "Amir Shaikhha" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1717-1745", + "session" : "" }, { "title" : "Compiling Structured Tensor Algebra", @@ -481480,6 +483321,13 @@ list = [ { "author" : "Jessica Shi", "publications" : [ + { + "title" : "QED in Context: An Observation Study of Proof Assistant Users", + "authors" : [ "Jessica Shi", "Cassia Torczon", "Harrison Goldstein", "Benjamin C. Pierce", "Andrew Head" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "337-363", + "session" : "" + }, { "title" : "Internalizing Indistinguishability with Dependent Types", "authors" : [ "Yiyun Liu", "Jonathan Chan", "Jessica Shi", "Stephanie Weirich" ], @@ -487788,6 +489636,21 @@ list = [ ] }, +{ + "author" : "Avaljot Singh", + "publications" : [ + { + "title" : "Automated Verification of Soundness of DNN Certifiers", + "authors" : [ "Avaljot Singh", "Yasmin Sarita", "Charith Mendis", "Gagandeep Singh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1802-1830", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Gagandeep Singh", "publications" : [ @@ -487825,6 +489688,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1036-1065", "session" : "" + }, + { + "title" : "Automated Verification of Soundness of DNN Certifiers", + "authors" : [ "Avaljot Singh", "Yasmin Sarita", "Charith Mendis", "Gagandeep Singh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1802-1830", + "session" : "" }, { "title" : "Input-Relational Verification of Deep Neural Networks", @@ -489087,6 +490957,13 @@ list = [ { "author" : "A. Prasad Sistla", "publications" : [ + { + "title" : "Checking δ-Satisfiability of Reals with Integrals", + "authors" : [ "Cody Rivera", "Bishnu Bhusal", "Rohit Chadha", "A. Prasad Sistla", "Mahesh Viswanathan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "704-729", + "session" : "" + }, { "title" : "Deciding accuracy of differential privacy schemes", "authors" : [ "Gilles Barthe", "Rohit Chadha", "Paul Krogmeier", "A. Prasad Sistla", "Mahesh Viswanathan" ], @@ -489232,6 +491109,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2009}, "pages" : " 161-172", "session" : "Session 7" + }, + { + "title" : "Automatically Verifying Replication-Aware Linearizability", + "authors" : [ "Vimala Soundarapandian", "Kartik Nagar", "Aseem Rastogi", "K. C. Sivaramakrishnan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "871-897", + "session" : "" }, { "title" : "Continuing WebAssembly with Effect Handlers", @@ -493451,6 +495335,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2022}, "pages" : "742-771", "session" : "" + }, + { + "title" : "Peepco: Batch-Based Consistency Optimization", + "authors" : [ "Ivan Kuraj", "John K. Feser", "Nadia Polikarpova", "Armando Solar-Lezama" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1101-1129", + "session" : "" }, { "title" : "Top-Down Synthesis for Library Learning", @@ -494307,6 +496198,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2022}, "pages" : "872-884", "session" : "Security" + }, + { + "title" : "Verification of Bit-Flip Attacks against Quantized Neural Networks", + "authors" : [ "Yedi Zhang", "Lei Huang", "Pengfei Gao", "Fu Song", "Jun Sun", "Jin Song Dong" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "984-1014", + "session" : "" }, { "title" : "EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis", @@ -495714,6 +497612,13 @@ list = [ { "author" : "Matthew Sotoudeh", "publications" : [ + { + "title" : "Pathological Cases for a Class of Reachability-Based Garbage Collectors", + "authors" : [ "Matthew Sotoudeh" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "449-476", + "session" : "" + }, { "title" : "Provable repair of deep neural networks", "authors" : [ "Matthew Sotoudeh", "Aditya V. Thakur" ], @@ -495785,6 +497690,13 @@ list = [ { "author" : "Vimala Soundarapandian", "publications" : [ + { + "title" : "Automatically Verifying Replication-Aware Linearizability", + "authors" : [ "Vimala Soundarapandian", "Kartik Nagar", "Aseem Rastogi", "K. C. Sivaramakrishnan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "871-897", + "session" : "" + }, { "title" : "Certified mergeable replicated data types", "authors" : [ "Vimala Soundarapandian", "Adharsh Kamath", "Kartik Nagar", "K. C. Sivaramakrishnan" ], @@ -497288,6 +499200,13 @@ list = [ "conference" : { "series" : "ICFP", "year" : 2022}, "pages" : "137-164", "session" : "" + }, + { + "title" : "Destination Calculus: A Linear 𝜆-Calculus for Purely Functional Memory Writes", + "authors" : [ "Thomas Bagrel", "Arnaud Spiwack" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "253-279", + "session" : "" }, { "title" : "Linear Haskell: practical linearity in a higher-order polymorphic language", @@ -502654,6 +504573,21 @@ list = [ ] }, +{ + "author" : "Sam Stites", + "publications" : [ + { + "title" : "Multi-Language Probabilistic Programming", + "authors" : [ "Sam Stites", "John M. Li", "Steven Holtzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1239-1266", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Greg Stitt", "publications" : [ @@ -505551,6 +507485,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2024}, "pages" : "176-205", "session" : "Bidirectional Typing and Session Types" + }, + { + "title" : "Characterizing Implementability of Global Protocols with Infinite States and Data", + "authors" : [ "Elaine Li", "Felix Stutz", "Thomas Wies", "Damien Zufferey" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1434-1463", + "session" : "" } ], "committees" : [ @@ -506678,6 +508619,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "957-985", "session" : "" + }, + { + "title" : "API-Guided Dataset Synthesis to Finetune Large Code Models", + "authors" : [ "Zongjie Li", "Daoyuan Wu", "Shuai Wang", "Zhendong Su" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "786-815", + "session" : "" }, { "title" : "API-Driven Program Synthesis for Testing Static Typing Implementations", @@ -507858,6 +509806,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1556-1582", "session" : "" + }, + { + "title" : "Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality", + "authors" : [ "Guanqin Zhang", "Zhenya Zhang", "H. M. N. Dilum Bandara", "Shiping Chen", "Jianjun Zhao", "Yulei Sui" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "85-112", + "session" : "" }, { "title" : "Context-Free Language Reachability via Skewed Tabulation", @@ -510205,6 +512160,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "2057-2089", "session" : "" + }, + { + "title" : "Verification of Bit-Flip Attacks against Quantized Neural Networks", + "authors" : [ "Yedi Zhang", "Lei Huang", "Pengfei Gao", "Fu Song", "Jun Sun", "Jin Song Dong" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "984-1014", + "session" : "" }, { "title" : "Combining model checking and testing with an application to reliability prediction and distribution", @@ -515833,7 +517795,13 @@ list = [ { "author" : "Jean-Pierre Talpin", "publications" : [ - + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" + } ], "committees" : [ { "role" : "PC Member", "conference" : { "series" : "ESOP", "year" : 2009} } @@ -516712,6 +518680,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2016}, "pages" : "169-180", "session" : "Research Papers" + }, + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" }, { "title" : "DocTer: documentation-guided fuzzing for testing deep learning API functions", @@ -517841,6 +519816,13 @@ list = [ { "author" : "Wenhao Tang", "publications" : [ + { + "title" : "Modal Effect Types", + "authors" : [ "Wenhao Tang", "Leo White", "Stephen Dolan", "Daniel Hillerström", "Sam Lindley", "Anton Lorenzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1130-1157", + "session" : "" + }, { "title" : "Soundly Handling Linearity", "authors" : [ "Wenhao Tang", "Daniel Hillerström", "Sam Lindley", "J. Garrett Morris" ], @@ -518140,6 +520122,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2020}, "pages" : "914-926", "session" : "Mobile" + }, + { + "title" : "Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis", + "authors" : [ "Yuchen Ji", "Ting Dai", "Zhichao Zhou", "Yutian Tang", "Jingzhu He" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1349-1377", + "session" : "" } ], "committees" : [ @@ -518342,6 +520331,13 @@ list = [ { "author" : "Swamit Tannu", "publications" : [ + { + "title" : "Dependency-Aware Compilation for Surface Code Quantum Architectures", + "authors" : [ "Abtin Molavi", "Amanda Xu", "Swamit Tannu", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "57-84", + "session" : "" + }, { "title" : "Synthesizing Quantum-Circuit Optimizers", "authors" : [ "Amanda Xu", "Abtin Molavi", "Lauren Pick", "Swamit Tannu", "Aws Albarghouthi" ], @@ -526505,6 +528501,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "646-672", "session" : "" + }, + { + "title" : "Unveiling Heisenbugs with Diversified Execution", + "authors" : [ "Arjun Ramesh", "Tianshu Huang", "Jaspreet Riar", "Ben L. Titzer", "Anthony Rowe" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "393-420", + "session" : "" }, { "title" : "Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks", @@ -528638,6 +530641,13 @@ list = [ { "author" : "Cassia Torczon", "publications" : [ + { + "title" : "QED in Context: An Observation Study of Proof Assistant Users", + "authors" : [ "Jessica Shi", "Cassia Torczon", "Harrison Goldstein", "Benjamin C. Pierce", "Andrew Head" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "337-363", + "session" : "" + }, { "title" : "Effects and Coeffects in Call-by-Push-Value", "authors" : [ "Cassia Torczon", "Emmanuel Suárez Acevedo", "Shubh Agrawal", "Joey Velez-Ginorio", "Stephanie Weirich" ], @@ -532321,6 +534331,21 @@ list = [ ] }, +{ + "author" : "Yi-Zhen Tsai", + "publications" : [ + { + "title" : "Hambazi: Spatial Coordination Synthesis for Augmented Reality", + "authors" : [ "Yi-Zhen Tsai", "Jiasi Chen", "Mohsen Lesani" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "307-336", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yun Chen Tsai", "publications" : [ @@ -545330,6 +547355,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "986-1012", "session" : "" + }, + { + "title" : "Checking δ-Satisfiability of Reals with Integrals", + "authors" : [ "Cody Rivera", "Bishnu Bhusal", "Rohit Chadha", "A. Prasad Sistla", "Mahesh Viswanathan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "704-729", + "session" : "" }, { "title" : "Dynamic Race Detection with O(1) Samples", @@ -550513,6 +552545,21 @@ list = [ ] }, +{ + "author" : "Michael Walter", + "publications" : [ + { + "title" : "QbC: Quantum Correctness by Construction", + "authors" : [ "Anurudh Peduri", "Ina Schaefer", "Michael Walter" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "534-562", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Braden M. Walters", "publications" : [ @@ -551994,6 +554041,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2017}, "pages" : "880-908", "session" : "Refine list" + }, + { + "title" : "Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials", + "authors" : [ "Qihao Lian", "Di Wang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1406-1433", + "session" : "" }, { "title" : "Newtonian Program Analysis of Probabilistic Programs", @@ -552637,6 +554691,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2020}, "pages" : "1387-1397", "session" : "Industry Papers" + }, + { + "title" : "JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach", + "authors" : [ "Hanzhang Wang", "Wei Peng", "Wenwen Wang", "Yunping Lu", "Pen-Chung Yew", "Weihua Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "113-142", + "session" : "" } ], "committees" : [ @@ -555559,6 +557620,21 @@ list = [ ] }, +{ + "author" : "Ruixin Wang", + "publications" : [ + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Runzhe Wang", "publications" : [ @@ -555909,6 +557985,21 @@ list = [ ] }, +{ + "author" : "Shiqi Wang", + "publications" : [ + { + "title" : "UTFix: Change Aware Unit Test Repairing using LLM", + "authors" : [ "Shanto Rahman", "Sachit Kuhar", "Berk Çirisci", "Pranav Garg", "Shiqi Wang", "Xiaofei Ma", "Anoop Deoras", "Baishakhi Ray" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "143-168", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Shiyang Wang", "publications" : [ @@ -556019,6 +558110,20 @@ list = [ "conference" : { "series" : "ASE", "year" : 2020}, "pages" : "1053-1065", "session" : "Refine list" + }, + { + "title" : "API-Guided Dataset Synthesis to Finetune Large Code Models", + "authors" : [ "Zongjie Li", "Daoyuan Wu", "Shuai Wang", "Zhendong Su" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "786-815", + "session" : "" + }, + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" }, { "title" : "PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis", @@ -556056,6 +558161,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "ICSE-AE", "year" : 2020} } ] }, +{ + "author" : "Shuling Wang", + "publications" : [ + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Shuo Wang", "publications" : [ @@ -556762,6 +558882,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2020}, "pages" : "107-120", "session" : "Abstract" + }, + { + "title" : "JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach", + "authors" : [ "Hanzhang Wang", "Wei Peng", "Wenwen Wang", "Yunping Lu", "Pen-Chung Yew", "Weihua Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "113-142", + "session" : "" }, { "title" : "Helper function inlining in dynamic binary translation", @@ -560447,6 +562574,21 @@ list = [ ] }, +{ + "author" : "Kazuki Watanabe", + "publications" : [ + { + "title" : "A Unifying Approach to Product Constructions for Quantitative Temporal Inference", + "authors" : [ "Kazuki Watanabe", "Sebastian Junges", "Jurriaan Rot", "Ichiro Hasuo" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1575-1603", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Keiichi Watanabe", "publications" : [ @@ -566416,6 +568558,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "656-686", "session" : "" + }, + { + "title" : "Modal Effect Types", + "authors" : [ "Wenhao Tang", "Leo White", "Stephen Dolan", "Daniel Hillerström", "Sam Lindley", "Anton Lorenzen" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1130-1157", + "session" : "" }, { "title" : "Oxidizing OCaml with Modal Memory Management", @@ -567593,6 +569742,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1378-1407", "session" : "" + }, + { + "title" : "Characterizing Implementability of Global Protocols with Infinite States and Data", + "authors" : [ "Elaine Li", "Felix Stutz", "Thomas Wies", "Damien Zufferey" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1434-1463", + "session" : "" }, { "title" : "Embedding Hindsight Reasoning in Separation Logic", @@ -569415,6 +571571,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1-30", "session" : "" + }, + { + "title" : "Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back", + "authors" : [ "Kevin Batz", "Joost-Pieter Katoen", "Francesca Randone", "Tobias Winkler" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "421-448", + "session" : "" }, { "title" : "Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs", @@ -572392,6 +574555,13 @@ list = [ "conference" : { "series" : "ESOP", "year" : 2020}, "pages" : "599-625", "session" : "Refine list" + }, + { + "title" : "Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice", + "authors" : [ "Jay Richards", "Daniel Wright", "Simon Cooksey", "Mark Batty" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1858-1882", + "session" : "" } ], "committees" : [ @@ -572902,6 +575072,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2022}, "pages" : "709-721", "session" : "Mining Software Repositories" + }, + { + "title" : "API-Guided Dataset Synthesis to Finetune Large Code Models", + "authors" : [ "Zongjie Li", "Daoyuan Wu", "Shuai Wang", "Zhendong Su" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "786-815", + "session" : "" } ], "committees" : [ @@ -573272,6 +575449,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2020}, "pages" : "871-882", "session" : "Refine list" + }, + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" } ], "committees" : [ @@ -579933,6 +582117,21 @@ list = [ ] }, +{ + "author" : "Chris Xiong", + "publications" : [ + { + "title" : "Carapace: Static-Dynamic Information Flow Control in Rust", + "authors" : [ "Vincent Beardsley", "Chris Xiong", "Ada Lamba", "Michael D. Bond" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "364-392", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jianxin Xiong", "publications" : [ @@ -580367,6 +582566,20 @@ list = [ { "author" : "Amanda Xu", "publications" : [ + { + "title" : "Dependency-Aware Compilation for Surface Code Quantum Architectures", + "authors" : [ "Abtin Molavi", "Amanda Xu", "Swamit Tannu", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "57-84", + "session" : "" + }, + { + "title" : "Checking Observational Correctness of Database Systems", + "authors" : [ "Lauren Pick", "Amanda Xu", "Ankush Desai", "Sanjit A. Seshia", "Aws Albarghouthi" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1661-1688", + "session" : "" + }, { "title" : "Synthesizing Quantum-Circuit Optimizers", "authors" : [ "Amanda Xu", "Abtin Molavi", "Lauren Pick", "Swamit Tannu", "Aws Albarghouthi" ], @@ -581764,6 +583977,21 @@ list = [ ] }, +{ + "author" : "Jiexiao Xu", + "publications" : [ + { + "title" : "Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing", + "authors" : [ "Yile Gu", "Ian Neal", "Jiexiao Xu", "Shaun Christopher Lee", "Ayman Said", "Musa Haydar", "Jacob Van Geffen", "Rohan Kadekodi", "Andrew Quinn", "Baris Kasikci" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "477-506", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jingwei Xu", "publications" : [ @@ -582698,6 +584926,21 @@ list = [ ] }, +{ + "author" : "Xiong Xu", + "publications" : [ + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Xiwei Xu", "publications" : [ @@ -584293,6 +586536,21 @@ list = [ ] }, +{ + "author" : "Runze Xue", + "publications" : [ + { + "title" : "Notions of Stack-Manipulating Computation and Relative Monads", + "authors" : [ "Yuchen Jiang", "Runze Xue", "Max S. New" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "563-589", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Wei Xue", "publications" : [ @@ -589768,6 +592026,21 @@ list = [ ] }, +{ + "author" : "Ziyi Yang", + "publications" : [ + { + "title" : "Inductive Synthesis of Inductive Heap Predicates", + "authors" : [ "Ziyi Yang", "Ilya Sergey" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "169-195", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Ziyue Yang", "publications" : [ @@ -591950,6 +594223,13 @@ list = [ "conference" : { "series" : "CGO", "year" : 2003}, "pages" : "125-134", "session" : "EPIC Compilation" + }, + { + "title" : "JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach", + "authors" : [ "Hanzhang Wang", "Wei Peng", "Wenwen Wang", "Yunping Lu", "Pen-Chung Yew", "Weihua Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "113-142", + "session" : "" }, { "title" : "Data Dependence Profiling for Speculative Optimizations", @@ -593707,6 +595987,13 @@ list = [ "conference" : { "series" : "POPL", "year" : 2025}, "pages" : "1326-1354", "session" : "" + }, + { + "title" : "Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness", + "authors" : [ "Dongjae Lee", "Janggun Lee", "Taeyoung Yoon", "Minki Cho", "Jeehoon Kang", "Chung-Kil Hur" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1267-1294", + "session" : "" } ], "committees" : [ @@ -596902,6 +599189,21 @@ list = [ ] }, +{ + "author" : "Shenghao Yuan", + "publications" : [ + { + "title" : "A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana", + "authors" : [ "Shenghao Yuan", "Zhuoruo Zhang", "Jiayi Lu", "David Sanán", "Rui Chang", "Yongwang Zhao" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1-27", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Ting Yuan", "publications" : [ @@ -597107,6 +599409,21 @@ list = [ ] }, +{ + "author" : "Yueming Yuan", + "publications" : [ + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yujie Yuan", "publications" : [ @@ -597399,6 +599716,21 @@ list = [ ] }, +{ + "author" : "Insu Yun", + "publications" : [ + { + "title" : "Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation", + "authors" : [ "Jihee Park", "Insu Yun", "Sukyoung Ryu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "898-926", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Jeonghyun Yun", "publications" : [ @@ -601265,6 +603597,13 @@ list = [ { "author" : "Bohua Zhan", "publications" : [ + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" + }, { "title" : "Mechanizing the CMP Abstraction for Parameterized Verification", "authors" : [ "Yongjian Li", "Bohua Zhan", "Jun Pang" ], @@ -601295,6 +603634,13 @@ list = [ { "author" : "Naijun Zhan", "publications" : [ + { + "title" : "HpC: A Calculus for Hybrid and Mobile Systems", + "authors" : [ "Xiong Xu", "Jean-Pierre Talpin", "Shuling Wang", "Hao Wu", "Bohua Zhan", "Xinxin Liu", "Naijun Zhan" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1158-1183", + "session" : "" + }, { "title" : "Lower Bounds for Possibly Divergent Probabilistic Programs", "authors" : [ "Shenghua Feng", "Mingshuai Chen", "Han Su", "Benjamin Lucien Kaminski", "Joost-Pieter Katoen", "Naijun Zhan" ], @@ -602949,6 +605295,13 @@ list = [ { "author" : "Guanqin Zhang", "publications" : [ + { + "title" : "Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality", + "authors" : [ "Guanqin Zhang", "Zhenya Zhang", "H. M. N. Dilum Bandara", "Shiping Chen", "Jianjun Zhao", "Yulei Sui" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "85-112", + "session" : "" + }, { "title" : "Flow2Vec: value-flow-based precise code embedding", "authors" : [ "Yulei Sui", "Xiao Cheng", "Guanqin Zhang", "Haoyu Wang" ], @@ -606551,6 +608904,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "1556-1582", "session" : "" + }, + { + "title" : "Fast Constraint Synthesis for C++ Function Templates", + "authors" : [ "Shuo Ding", "Qirun Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "225-252", + "session" : "" }, { "title" : "SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories", @@ -607339,6 +609699,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2018}, "pages" : "880-883", "session" : "Bugs" + }, + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" } ], "committees" : [ @@ -607493,6 +609860,13 @@ list = [ "conference" : { "series" : "PPoPP", "year" : 2011}, "pages" : " 213-222", "session" : "Parallel applications and scheduling" + }, + { + "title" : "JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach", + "authors" : [ "Hanzhang Wang", "Wei Peng", "Wenwen Wang", "Yunping Lu", "Pen-Chung Yew", "Weihua Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "113-142", + "session" : "" } ], "committees" : [ @@ -608664,6 +611038,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2015}, "pages" : "745-757", "session" : "Java and Object-Oriented Programming" + }, + { + "title" : "Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences", + "authors" : [ "Tianchi Li", "Xin Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1774-1801", + "session" : "" }, { "title" : "Learning Abstraction Selection for Bayesian Program Analysis", @@ -609195,6 +611576,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2022}, "pages" : "82:1-82:13", "session" : "Research Papers" + }, + { + "title" : "Verification of Bit-Flip Attacks against Quantized Neural Networks", + "authors" : [ "Yedi Zhang", "Lei Huang", "Pengfei Gao", "Fu Song", "Jun Sun", "Jin Song Dong" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "984-1014", + "session" : "" }, { "title" : "Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks", @@ -610520,6 +612908,21 @@ list = [ ] }, +{ + "author" : "Zhenya Zhang", + "publications" : [ + { + "title" : "Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality", + "authors" : [ "Guanqin Zhang", "Zhenya Zhang", "H. M. N. Dilum Bandara", "Shiping Chen", "Jianjun Zhao", "Yulei Sui" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "85-112", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Zhenyu Zhang", "publications" : [ @@ -610658,6 +613061,21 @@ list = [ ] }, +{ + "author" : "Zhuoruo Zhang", + "publications" : [ + { + "title" : "A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana", + "authors" : [ "Shenghao Yuan", "Zhuoruo Zhang", "Jiayi Lu", "David Sanán", "Rui Chang", "Yongwang Zhao" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1-27", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Ziqi Zhang", "publications" : [ @@ -610674,6 +613092,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2020}, "pages" : "838-850", "session" : "Machine Learning" + }, + { + "title" : "Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles", + "authors" : [ "Zhineng Zhong", "Ziqi Zhang", "Hanqin Guan", "Ding Li" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "676-703", + "session" : "" }, { "title" : "ModelDiff: testing-based DNN similarity comparison for model reuse detection", @@ -611196,6 +613621,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2019}, "pages" : "477-487", "session" : "Main Research" + }, + { + "title" : "Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality", + "authors" : [ "Guanqin Zhang", "Zhenya Zhang", "H. M. N. Dilum Bandara", "Shiping Chen", "Jianjun Zhao", "Yulei Sui" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "85-112", + "session" : "" }, { "title" : "Probabilistic Points-to Analysis for Java", @@ -612448,6 +614880,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "ICSE", "year" : 2022} } ] }, +{ + "author" : "Yongwang Zhao", + "publications" : [ + { + "title" : "A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana", + "authors" : [ "Shenghao Yuan", "Zhuoruo Zhang", "Jiayi Lu", "David Sanán", "Rui Chang", "Yongwang Zhao" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1-27", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yu Zhao", "publications" : [ @@ -612485,6 +614932,21 @@ list = [ ] }, +{ + "author" : "Yubo Zhao", + "publications" : [ + { + "title" : "Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation", + "authors" : [ "Yikun Hu", "Yituo He", "Wenyu He", "Haoran Li", "Yubo Zhao", "Shuai Wang", "Dawu Gu" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "28-56", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yue Zhao", "publications" : [ @@ -612683,6 +615145,21 @@ list = [ { "role" : "PC Member", "conference" : { "series" : "CC", "year" : 2021} } ] }, +{ + "author" : "Zhongkai Zhao", + "publications" : [ + { + "title" : "Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison", + "authors" : [ "Ruixin Wang", "Zhongkai Zhao", "Le Fang", "Nan Jiang", "Yiling Lou", "Lin Tan", "Tianyi Zhang" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1831-1857", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Zhongyuan Zhao", "publications" : [ @@ -614309,6 +616786,21 @@ list = [ ] }, +{ + "author" : "Zhineng Zhong", + "publications" : [ + { + "title" : "Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles", + "authors" : [ "Zhineng Zhong", "Ziqi Zhang", "Hanqin Guan", "Ding Li" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "676-703", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Zhiqing Zhong", "publications" : [ @@ -615974,6 +618466,21 @@ list = [ ] }, +{ + "author" : "Yanqi Zhou", + "publications" : [ + { + "title" : "SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention", + "authors" : [ "Ahan Gupta", "Yueming Yuan", "Devansh Jain", "Yuhao Ge", "David Aponte", "Yanqi Zhou", "Charith Mendis" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1632-1660", + "session" : "" + } + ], + "committees" : [ + + ] +}, { "author" : "Yaoda Zhou", "publications" : [ @@ -616194,6 +618701,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2005}, "pages" : " 306-315", "session" : "Bug localization" + }, + { + "title" : "Laurel: Unblocking Automated Verification with Large Language Models", + "authors" : [ "Eric Mugnier", "Emmanuel Anaya Gonzalez", "Nadia Polikarpova", "Ranjit Jhala", "Yuanyuan Zhou" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1519-1545", + "session" : "" } ], "committees" : [ @@ -616390,6 +618904,13 @@ list = [ "conference" : { "series" : "ASE", "year" : 2022}, "pages" : "91:1-91:12", "session" : "Research Papers" + }, + { + "title" : "Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis", + "authors" : [ "Yuchen Ji", "Ting Dai", "Zhichao Zhou", "Yutian Tang", "Jingzhu He" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1349-1377", + "session" : "" } ], "committees" : [ @@ -616972,6 +619493,13 @@ list = [ "conference" : { "series" : "FSE", "year" : 2007}, "pages" : " 517-520", "session" : "ESEC/FSE'07 posters" + }, + { + "title" : "Adaptive Shielding via Parametric Safety Proofs", + "authors" : [ "Yao Feng", "Jun Zhu", "André Platzer", "Jonathan Laurent" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "816-843", + "session" : "" } ], "committees" : [ @@ -620550,6 +623078,13 @@ list = [ "conference" : { "series" : "ECOOP", "year" : 2019}, "pages" : "28:1-28:27", "session" : "Experiences" + }, + { + "title" : "Characterizing Implementability of Global Protocols with Infinite States and Data", + "authors" : [ "Elaine Li", "Felix Stutz", "Thomas Wies", "Damien Zufferey" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1434-1463", + "session" : "" }, { "title" : "Multiparty motion coordination: from choreographies to robotics programs", @@ -620894,6 +623429,13 @@ list = [ "conference" : { "series" : "OOPSLA", "year" : 2022}, "pages" : "424-448", "session" : "" + }, + { + "title" : "Language-Parametric Reference Synthesis", + "authors" : [ "Daniël A. A. Pelsmaeker", "Aron Zwaan", "Casper Bach Poulsen", "Arjan J. Mooij" ], + "conference" : { "series" : "OOPSLA", "year" : 2025}, + "pages" : "1213-1238", + "session" : "" } ], "committees" : [