PropGen automates property generation for Android app testing via LLM synthesis from guided exploration and feedback refinement, yielding 912 valid properties and 25 previously unknown bugs across 12 apps.
arXiv preprint arXiv:2405.02580 (2024)
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
years
2026 5verdicts
UNVERDICTED 5representative citing papers
VLP adds an NL documentation layer with trace-linked mismatch detection and derived formal checks to make human validation of LLM code feasible, lifting pass@1 from 28.7-73.2% to 65.4-93.5%.
SpecSyn generates formal specifications with over 90% precision and 75% recall, successfully verifying 1071 out of 1365 target properties on open-source programs.
V2E automates PoC generation, triggerability and profitability validation, and iterative refinement using LLMs to confirm exploitable smart contract vulnerabilities, outperforming baselines on 264 labeled contracts.
Improved IsabeLLM adds RAG, error tracing, and Isabelle compatibility updates and is tested on verifying Bitcoin Proof of Work consensus.
citing papers explorer
-
From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing
PropGen automates property generation for Android app testing via LLM synthesis from guided exploration and feedback refinement, yielding 912 valid properties and 25 previously unknown bugs across 12 apps.
-
Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming
VLP adds an NL documentation layer with trace-linked mismatch detection and derived formal checks to make human validation of LLM code feasible, lifting pass@1 from 28.7-73.2% to 65.4-93.5%.
-
SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
SpecSyn generates formal specifications with over 90% precision and 75% recall, successfully verifying 1071 out of 1365 target properties on open-source programs.
-
V2E: Validating Smart Contract Vulnerabilities through Profit-driven Exploit Generation and Execution
V2E automates PoC generation, triggerability and profitability validation, and iterative refinement using LLMs to confirm exploitable smart contract vulnerabilities, outperforming baselines on 264 labeled contracts.
-
IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
Improved IsabeLLM adds RAG, error tracing, and Isabelle compatibility updates and is tested on verifying Bitcoin Proof of Work consensus.