A bisimulation-invariant synthesis framework for optimal predicate pushdown in fold-based UDFs produces correct transformations that speed up 150 real pipelines by 2.4x on average.
In: Proceedings of the 37th ACM SIG- PLAN Conference on Programming Language Design and Implementa- tion, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
roles
background 3polarities
background 3representative citing papers
Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
APIDiffer automatically detects 72 API inconsistencies across 11 Ethereum clients using specification-guided test generation and LLM-based false-positive filtering, with 90% of bugs confirmed by developers.
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
OpDiffer applies LLMs and static analysis to opcode-level differential testing of EVMs, reporting 26 previously unknown bugs across nine implementations along with coverage gains and an estimate that 7.21% of real contracts could trigger the bugs.
Proposes constraint-based type inference for type-directed synthesis of polymorphic code and GADTs, implemented in the Scythe live programming tool for Haskell.
citing papers explorer
-
Optimal Predicate Pushdown Synthesis
A bisimulation-invariant synthesis framework for optimal predicate pushdown in fold-based UDFs produces correct transformations that speed up 150 real pipelines by 2.4x on average.
-
Hyper Separation Logic (extended version)
Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
-
When Specifications Meet Reality: Uncovering API Inconsistencies in Ethereum Infrastructure
APIDiffer automatically detects 72 API inconsistencies across 11 Ethereum clients using specification-guided test generation and LLM-based false-positive filtering, with 90% of bugs confirmed by developers.
-
ClassInvGen: Class Invariant Synthesis using Large Language Models
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
-
OpDiffer: LLM-Assisted Opcode-Level Differential Testing of Ethereum Virtual Machine
OpDiffer applies LLMs and static analysis to opcode-level differential testing of EVMs, reporting 26 previously unknown bugs across nine implementations along with coverage gains and an estimate that 7.21% of real contracts could trigger the bugs.
-
Constraint-Based Type-Directed Program Synthesis
Proposes constraint-based type inference for type-directed synthesis of polymorphic code and GADTs, implemented in the Scythe live programming tool for Haskell.