Desyan: A Platform for Seamless Value-Flow and Symbolic Analysis
Panagiotis Diamantakis, Thanassis Avgerinos, Yannis Smaragdakis

TL;DR
Desyan is a unified platform that seamlessly integrates value-flow and symbolic analysis, enabling efficient and flexible program reasoning by combining Datalog evaluation with SMT solving.
Contribution
It introduces a novel platform that unifies value-flow and symbolic analysis within a single engine, enhancing performance and flexibility in program analysis tasks.
Findings
Datalog evaluation is over 20x faster for value-flow analysis.
Using Datalog-native symbolic reasoning can double speed compared to SMT solving.
The platform supports diverse analysis techniques with high efficiency.
Abstract
Over the past two decades, two different types of static analyses have emerged as dominant paradigms both in academia and industry: value-flow analysis (e.g., data-flow analysis or points-to analysis) and symbolic analysis (e.g., symbolic execution). Despite their individual successes in numerous application fields, the two approaches have remained largely separate; an artifact of the simple reality that there is no broadly adopted unifying platform for effortless and efficient integration of symbolic techniques with high-performance data-flow reasoning. To bridge this gap, we introduce Desyan: a platform for writing program analyses with seamless integration of value-flow and symbolic reasoning. Desyan expands a production-ready Datalog fixpoint engine (Souffl\'e) with full-fledged SMT solving invoking industry-leading SMT engines. Desyan provides constructs for automatically (and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Embedded Systems Design Techniques
