APPL is a sound, relatively complete abstract program logic that subsumes Hoare, incorrectness, and hyperproperty logics via lattice semantics and a non-idempotent monoidal operator for nondeterminism.
org/abs/2504.20415v1
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
Relational Kleene algebra with graph loop has a PSPACE-complete equational theory over relational models.
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
Soteria is a functional library for building direct symbolic execution engines, demonstrated by the first Rust engine supporting Tree Borrows and a compositional C engine that matches or exceeds prior tools.
A type system with types over normal forms and a decidable complement operator via subtyping is sound and complete, deriving refutation principles to certify incorrectness in functional programs.
AnyPoC introduces a multi-agent system for generating and validating PoC tests from LLM bug reports, producing 1.3x more valid PoCs, rejecting 9.8x more false positives, and discovering 122 new bugs across 12 major projects.
citing papers explorer
-
A Program Logic for Abstract (Hyper)Properties
APPL is a sound, relatively complete abstract program logic that subsumes Hoare, incorrectness, and hyperproperty logics via lattice semantics and a non-idempotent monoidal operator for nondeterminism.
-
The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
Relational Kleene algebra with graph loop has a PSPACE-complete equational theory over relational models.
-
Trace-Guided Synthesis of Effectful Test Generators
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
-
Soteria: Efficient Symbolic Execution as a Functional Library
Soteria is a functional library for building direct symbolic execution engines, demonstrated by the first Rust engine supporting Tree Borrows and a compositional C engine that matches or exceeds prior tools.
-
A Complementary Approach to Incorrectness Typing
A type system with types over normal forms and a decidable complement operator via subtyping is sound and complete, deriving refutation principles to certify incorrectness in functional programs.
-
AnyPoC: Universal Proof-of-Concept Test Generation for Scalable LLM-Based Bug Detection
AnyPoC introduces a multi-agent system for generating and validating PoC tests from LLM bug reports, producing 1.3x more valid PoCs, rejecting 9.8x more false positives, and discovering 122 new bugs across 12 major projects.