ComputingComputer ScienceProgramming LanguagesSoftware EngineeringSystems ProgrammingAbstract Syntax TreesControl-flow AnalysisData-flow AnalysisStatic AnalysisStatic Code AnalysisSymbolic ExecutionCall Graph ConstructionInterprocedural AnalysisPreconditionsSummary-based Symbolic ExecutionSymbolic AnalysisSymbolic State RepresentationTest GenerationWeakest Preconditions
Symbolic analysis shows promise as a foundation for bug-finding, specification inference, verification, and test generation. This paper addresses demand-driven symbolic analysis for object-oriented programs and frameworks. Many such codes comprise large, partial programs with highly dynamic behaviors--polymorphism, reflection, and so on--posing significant scalability challenges for any static analysis.
27
Symbolic execution and program testing
James C. King · Communications of the ACM · 1976 · 3K citations · Full text
Separation logic: a logic for shared mutable data structures
John Reynolds · 2003 · 2.2K citations
Patrice Godefroid, Nils Klarlund, Koushik Sen · ACM SIGPLAN Notices · 2005 · 2.1K citations
Koushik Sen, Darko Marinov, Gul Agha · 2005 · 1.7K citations