Pith. sign in

REVIEW 3 major objections 5 minor 59 references

Conflict Extraction in Probabilistic Datalog Analyses

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that conflicting alarms in probabilistic Datalog analyses can be identified exactly as minimal unsatisfiable subsets of a Boolean encoding of the derivation graph, and that PPProbe enumerates these subsets soundly and…

desk verdict The problem is real and the derivation-aware sampling idea is worth building on, but Algorithm 6's replacement rule is unsound under negative dependencies, so the central soundness claim needs repair before the results can be trusted. read the letter →

arxiv 2608.10755 v1 pith:XWOYLWWJ submitted 2026-08-11 cs.SE cs.PL

Siyu Chen , Chungha Sung , Xuyang Li , Jingbo Wang This is my paper · ORCID
classification cs.SEcs.PL
keywords probabilisticDatalogminimalunsatisfiablesubsetsconflictextractionderivationgraphMUSenumerationstaticanalysisfalsealarmreduction
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Probabilistic Datalog analyses return alarms with marginal probabilities, and a developer can easily be presented with two alarms that are each plausible in some possible world but that no single world contains together. This paper argues that those mutually exclusive output combinations are exactly the minimal unsatisfiable subsets (MUSes) of the Boolean encoding of the program's derivation graph, and that a specialized MUS enumerator called PPProbe can find them soundly and efficiently. PPProbe prioritizes candidate sets by exploiting negative structural and statistical dependencies in the derivation graph, then prunes the search by deriving new conflicts from old ones through logical replacement. If the claim is right, developers can automatically filter out alarm combinations that can never co-occur, and the paper reports an average 47.7% reduction in mutually inconsistent alarms across 70 benchmarks.

What carries the argument

The load-bearing object is the Boolean interpretation of the grounded derivation graph (Definition 4): each rule instance becomes an independent Bernoulli event variable $S[r]$, each fact becomes a Boolean variable $\Gamma[v]$, and each derived fact is defined by $D_v = \bigvee_{r \in \mathrm{Derv}(v)} (S[r] \wedge \bigwedge_{b^+ \in B^+} \Gamma[b^+] \wedge \bigwedge_{b^- \in B^-} \neg \Gamma[b^-])$. This reduces the question 'can these output facts co-occur?' to a SAT problem over $\Phi$, and a minimal unsatisfiable subset of output facts under $\Phi$ is exactly a minimal conflict. The supporting mechanisms are the derivation graph itself: negative edges $h \to b$ for each negated body literal $b$ drive derivative sampling, and recursive dependency sets $\mathrm{Dep}^+$ and $\mathrm{Dep}^-$ (input facts that support or oppose a relation) steer the sampler toward statistically negatively dependent pairs; logical replacement over the graph then generates new MUSes bottom-up.

What would settle it

Run PPProbe on the program containing only the rule `0.5::p :- p.` (a positive recursive cycle with no base fact). The intended least-model semantics says p is false in every possible world, so the set `{p}` should be reported as unsatisfiable; if PPProbe reports `{p}` as satisfiable, the Boolean encoding has admitted a self-supported model and the claimed soundness of the abstraction is violated.

Watch

Extended reading notes

Core claim

The central claim is that conflicts among output facts of a probabilistic Datalog program are exactly the minimal unsatisfiable subsets (MUSes) under the Boolean encoding $\Phi$ of the grounded derivation graph, and that PPProbe enumerates these MUSes soundly. Soundness is defined as every produced MUS corresponding to a genuine conflict: the facts in the MUS cannot hold together in any valid interpretation, independent of the numeric probabilities. The two mechanisms that make enumeration efficient are derivative sampling, which targets combinations whose derivation trees share input facts with opposite polarity, and bottom-up MUS inference, which replaces facts in a known MUS by their derivation ancestors (or blocks alternate derivations) to synthesize new conflicts without extra solver calls. On 70 benchmarks from side-channel analysis, data race detection, semantic diffing, and Bayesian networks, PPProbe reports higher throughput than MARCO, ReMUS, and TOME, and the conflicts it finds yield a conservative false-positive reduction, averaging 47.7%.

Load-bearing premise

The Boolean encoding of Definition 4 assumes that every satisfiable assignment to rule-event and fact variables corresponds to a genuine possible world, without enforcing Datalog's least-fixpoint semantics, so positive recursive derivations might create self-supported 'worlds' that the intended semantics rejects.

Editorial extensions

If this is right

  • If PPProbe is sound, any alarm set that is a superset of a detected MUS can be discarded without inspecting it, because no possible world realizes it.
  • The reduction percentages (69% for side-channel queries, 61% for data-race queries) are conservative lower bounds on the fraction of alarm combinations a developer can prune.
  • Because the encoding and enumeration ignore the concrete probability values, the same pipeline applies to any probabilistic Datalog program whose rule probabilities are learned or estimated differently.
  • The technique changes the workflow of probabilistic program analysis: instead of triaging every alarm, a developer first runs conflict extraction and only inspects alarms that survive the MUS-based filter.
  • Generic MUS enumerators that ignore derivation-graph structure time out on the same benchmarks, indicating that the structural guidance, not the SAT encoding alone, is responsible for the scalability.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The pipeline is insensitive to probability values, so the same conflict extractor would work for any probabilistic Datalog program regardless of how its rule probabilities were learned; the four-domain evaluation already suggests this portability, but the paper does not claim it as a general theorem.
  • The dependency polarity sets could double as an explanation mechanism: when PPProbe reports a conflict, the shared input fact appearing in Dep+ of one fact and Dep- of the other identifies the root cause, a feature the paper does not implement.
  • The reported reductions understate the benefit for individual alarms: they are computed on combinations, so a developer who simply drops alarms participating in any detected MUS would likely remove more than 47.7% of the alarm volume; this per-alarm metric is not reported.
  • If the least-fixpoint faithfulness gap in Definition 4 is real, then on programs with positive recursive cycles PPProbe could miss genuine conflicts (because the encoding over-approximates the possible worlds); testing this on synthetic recursion-only programs would separate the abstraction question from the tool's practical value.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces PPProbe, a tool for extracting minimal unsatisfiable subsets (MUSes) from probabilistic Datalog analyses. The authors formalize mutual inconsistency among output facts as MUSes over a Boolean encoding Φ of the derivation graph, and propose two optimizations: derivative sampling, which uses negative structural and statistical dependencies to prioritize candidate combinations, and bottom-up MUS inference, which derives new conflicts via logical replacement over the derivation graph. The tool is evaluated on 70 benchmarks from side-channel analysis, data race analysis, semantic diffing, and Bayesian networks, reporting higher MUS throughput than MARCO, ReMUS, and TOME, as well as substantial reductions in false alarms when MUSes are used as constraints in a MaxSAT filtering step.

Significance. If the reported results and the soundness claims hold, PPProbe would be a useful domain-specific MUS enumeration method for an emerging class of probabilistic program analyses. The paper has several strengths: it identifies a genuinely new problem (mutual inconsistency of probabilistic Datalog outputs), the implementation is artifact-backed, the evaluation covers multiple real-world domains, the ablations isolate the contribution of each optimization, and the stability analysis speaks to the randomness of the sampler. The claimed throughput gains over generic MUS enumerators are plausible in spirit, since the tool exploits derivation-graph structure that generic tools ignore. However, the paper's central soundness claim is currently not established: the bottom-up inference step contains a concrete unsoundness under negative dependencies, and the Boolean encoding's relation to least-fixpoint possible-world semantics is asserted rather than proven. These issues are local and fixable in principle, but they must be addressed before the contributions can be accepted.

major comments (3)
  1. [Section 6, Algorithm 6 (lines 3–5) and Algorithm 7] The 'exclusive dependency' replacement is not sound when the dependency is negative. The paper does not restrict 'depends solely on v' to positive dependencies. Under the Boolean encoding of Definition 4, if n's only derivation is n :- ¬v, then Γ[n] = S_n ∧ ¬Γ[v], so Γ[n]=true forces Γ[v]=false. Replacing v by n can therefore turn an UNSAT set into a SAT set. Concretely, take input b and rules v :- b, a :- ¬v, n :- ¬v. Then M={v,a} is an MUS: v requires b, and a requires ¬v. But C=(M\{v})∪{n}={a,n} is SAT by setting S_a=S_n=true, Γ[v]=false, and Γ[b]=true. Algorithm 7 then calls Shrink(C) without a prior CheckSat, since Algorithm 1 only calls Shrink after the UNSAT check in line 8. Running a deletion-based shrink on a SAT formula can return a set that is not an MUS of Φ, directly invalidating the soundness claim in Section 4 unless 'depends solely' is defined to exclude negative dependencies and the algorithm is modified accordingly.
  2. [Section 3.2, Definition 4 and Section 3.3, Definition 5] The encoding Φ is asserted to characterize possible worlds but does not enforce least-fixpoint semantics. Section 3.1 defines the solution as the least fixpoint over the Herbrand universe, and only negation is required to be stratified; positive recursion is allowed. For a rule p :- p, the equation Γ[p] ↔ (S[p] ∧ Γ[p]) admits the spurious model Γ[p]=true with S[p]=true even when p has no derivation from input facts. Thus Φ-models can be a strict superset of possible worlds. This does not affect the UNSAT direction used for conflict detection—if Φ is unsatisfiable, no possible world exists—but it means the claim in Section 3.3 that joint satisfiability under Φ captures co-occurrence in a possible world is unproven, and the minimality guarantee of Definition 6 may not hold for actual conflicts: a proper subset can be Φ-SAT via a spurious model while being unsatisfiable in every possible world. The authors should either prove that every model of Φ extends to a least-fixpoint model (which is false for the p :- p example) or explicitly separate the soundness claim from the completeness/minimality claim.
  3. [Section 6, 'Logical Replacement' paragraph] The paper asserts that replacing v by n in a known MUS yields a set 'guaranteed to be UNSAT' (Algorithm 6, line 4), and that blocking an alternative derivation d2 with a positive literal v' by adding the other members of an existing MUS M_alt is sound (lines 15–17). The second assertion relies on the fact that any model of Φ with M_alt\{v'} true must have v' false, which is true only because M_alt is an MUS under Φ; this dependence should be stated explicitly. More importantly, the first assertion has no proof and, as shown in the previous comment, is false without a polarity condition. The section should include a formal invariant stating exactly which syntactic conditions make logical replacement preserve unsatisfiability, together with a proof, or the algorithmic claim should be weakened.
minor comments (5)
  1. [Table 2] The runtime entries are typeset without separators (e.g., '0.40.5 0.4 2.40.00.0 0.0 0.01.93.0 2.4 17.9'), which makes the values unreadable; please reformat the table so that each column is distinct.
  2. [Section 7.2 and Figure 6] The caption of Figure 6 says 'Normalized MUS count', while the text describes normalized throughput relative to the best baseline. These terms should be reconciled, and the normalization base (per-domain best baseline) should be stated in the caption.
  3. [Section 5.2, Algorithm 4] Algorithm 4 returns Root' as a set (S+∪S− minus Visited), but Algorithm 2 uses it as a single root; if the set is empty or contains multiple elements, the behavior is underspecified. Please clarify the intended selection rule or return type.
  4. [Section 7.1] The phrase 'Eightside-channel analysis benchmarks' is missing a space, and the table of benchmark statistics would benefit from a Total row so that the reader can verify the claimed count of 70 benchmarks directly.
  5. [Section 5.2, Theorem 1] The proof of Theorem 1 is informal: it does not rigorously justify that satisfying assignments for v1 and v2 can always be combined when the dependencies on shared input facts have the same polarity, especially in the presence of intermediate derived facts and multiple derivations. Either a complete proof should be supplied, or the statement should be marked as a heuristic that guides sampling rather than as a theorem.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the MUS criterion is stated over an independently defined Boolean encoding, and author self-citations are only benchmark provenance.

full rationale

No circularity is present in the derivation chain. PPProbe's MUSes are defined directly over the Boolean encoding Φ (Definition 4) and the joint-satisfiability check Ψ (Definition 5); the enumeration loop (Algorithm 1) uses an external SAT solver for the UNSAT check and Shrink, so discovered MUSes are not produced by construction from the sampling heuristic. The claim that Φ is 'sufficient for conflict extraction' is an abstraction-correctness assertion, not a circular definition: Definition 6 is stated in terms of Ψ, and the paper does not define Φ using the target MUSes or benchmark outcomes. The paper's self-citations ([45], [54], [55], [56]) appear as benchmark provenance and motivation, not as load-bearing evidence for soundness, so they do not constitute circular support. The main caveats—the unproved least-fixpoint fidelity of Φ and Algorithm 6's unguarded exclusive-dependency replacement for negative literals—are correctness risks, but they are not cases where a result is equivalent to its input by construction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim does not fit any constants to data. The assumptions are semantic commitments about how probabilistic Datalog possible worlds map to Boolean equations, plus one evaluation assumption about what the MaxSAT reduction measures.

assumptions (4)
  • domain assumption Probabilistic Datalog programs used in this paper have stratified negation, so negation never appears in recursive cycles.
    Stated in Section 3.1; needed for the least-fixpoint semantics that underlies possible-world reasoning.
  • domain assumption Each grounded rule instance is an independent Bernoulli event, and possible worlds are captured by the Boolean equations of Definition 4.
    Section 3.2, Definition 4. The paper asserts this abstraction is sufficient for conflict extraction without proving that every model of the equations corresponds to a possible world.
  • ad hoc to paper The definitional equations Gamma[v] = D_v characterize all possible worlds, including under positive recursion.
    Definition 4 allows non-least fixpoints (e.g., self-supported cyclic derivations), so the encoding may admit assignments that the language's least-model semantics would reject.
  • ad hoc to paper MaxSAT with MUS constraints gives a lower bound on false-positive reduction.
    Section 7.4 methodology; it actually provides an upper bound on the number of alarms that can be pruned while keeping a consistent subset, not a proven reduction in false positives.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Conflict Extraction in Probabilistic Datalog Analyses." pith.science (2026). https://pith.science/paper/XWOYLWWJ

@misc{pith2026260810755,
  author       = {Pith},
  title        = {Pith review of: Conflict Extraction in Probabilistic Datalog Analyses},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XWOYLWWJ}},
  note         = {Machine review of arXiv:2608.10755}
}
read the original abstract

Probabilistic extensions of Datalog enable static analyses such as pointer analysis, data race detection, and side-channel analysis to rank alarms by likelihood, but this added expressiveness also introduces a new challenge absent from deterministic analyses: the final output may contain alarms that are individually plausible yet mutually inconsistent, because marginal probabilities do not guarantee joint satisfiability. As a result, developers may spend effort investigating combinations of alarms that can never co-occur in any possible world. We address this problem by formalizing such inconsistencies as minimal unsatisfiable subsets (MUSes) and introducing PPProbe, a conflict extractor specialized for probabilistic Datalog analyses. Rather than improving MUS enumeration in general, PPProbe exploits the structure of Datalog derivation graphs to guide the search toward likely conflicts and prune the search space through bottom-up UNSAT inference. We evaluate PPProbe on 70 benchmarks from power side-channel analysis, data race detection, semantic diffing, and Bayesian-network inference. The results show that PPProbe achieves 2.5 to 24 times higher throughput than state-of-the-art MUS enumerators, and that the conflicts it identifies yield a conservative estimate of false-positive reduction, filtering out an average of 47.7% of mutually inconsistent alarms.

Figures

Figures reproduced from arXiv: 2608.10755 by the authors.

Figure 1
Figure 1. PPProbe– Overview of generating MUSes from the probabilistic Datalog program 𝑃. visibility hinders tasks like program analysis, where developers must decide which alarms to investigate and trace to root cause. To systematically capture and explain these conflicts, we represent them as minimal unsatisfiable subsets (MUSes)—minimal sets of output facts whose conjunction is unsatisfiable (UNSAT) while every proper subs… view at source ↗
Figure 2
Figure 2. Side-channel analysis in probabilistic Datalog. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Left: an example program adapted from [58]. Right: its derivation graph, where white nodes are input facts and gray nodes are derived facts. The red highlights show a conflict: one branch requires ¬leak(c2), while the other requires leak(c2), so sid(c3) and leak(c5) cannot hold together. Rule numbers refer to [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Sampling example showing the application of [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]
Figure 5
Figure 5. Figure 5: Evolution of the sampling quota (𝑦-axis) across successive iterations (𝑥-axis). Solid markers denote UNSAT combinations verified by the SAT solver, whereas hollow markers represent SAT combinations. the solver continues to find UNSAT combinations. By maintaining small …
Figure 6
Figure 6. Figure 6: Normalized MUS count of PPProbe and its ablated variants relative to the strongest baseline. graph for the input probabilistic Datalog program. For satisfiability checking, PPProbe integrates with the CVC5 SMT solver [3]. Our experimental evaluation was conducted on a …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 33 canonical work pages

  1. [1]

    Falck, U

    Steen Andreassen, {Finn V.} Jensen, {Stig Kjær} Andersen, B. Falck, U. Kjærulff, M. Woldbye, A.R. Sørensen, A. Rosenfalck, and F. Jensen. 1989.MUNIN: an expert EMG assistant. Pergamon Press, 255–277

    work page 1989

  2. [2]

    James Bailey and Peter J Stuckey. 2005. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In International Workshop on Practical Aspects of Declarative Languages. Springer, 174–186. doi:10.1007/978-3-540-30557-6_14

    work page doi:10.1007/978-3-540-30557-6_14 2005

  3. [3]

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. 2022. cvc5: A versatile and industrial-strength SMT solver. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 415–442. doi:10.1007/978-3-0...

    doi:10.1007/978-3-030-99524-9_24 2022

  4. [4]

    Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub. 2015. Verified Proofs of Higher-Order Masking. InAdvances in Cryptology – EUROCRYPT 2015, Elisabeth Oswald and Marc Fischlin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 457–485. doi:10.1007/978-3-662-46800-5_18

    doi:10.1007/978-3-662-46800-5_18 2015

  5. [5]

    Jaroslav Bendík. 2017. Consistency checking in requirements analysis. InProceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis(Santa Barbara, CA, USA)(ISSTA 2017). Association for Computing Machinery, New York, NY, USA, 408–411. doi:10.1145/3092703.3098239

    work page arXiv 2017

  6. [6]

    Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat. 2016. Tunable Online MUS/MSS Enumeration. In36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 65), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.). Schloss...

    work page doi:10.4230/lipics.fsttcs.2016.50 2016

  7. [7]

    Jaroslav Bendík and Ivana Cerná. 2020. Replication-Guided Enumeration of Minimal Unsatisfiable Subsets. InCP (Lecture Notes in Computer Science, Vol. 12333). Springer, 37–54. doi:10.1007/978-3-030-58475-7_3

    work page doi:10.1007/978-3-030-58475-7_3 2020

  8. [8]

    Jaroslav Bendík and Ivana Černá. 2020. MUST: Minimal Unsatisfiable Subsets Enumeration Tool. InTools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Armin Biere and David Parker (Eds.). Lecture Notes in Computer Science, Vol. 12078. Springer, 135–152. doi:10.1007/978-3-030-45190-5_8

    work page doi:10.1007/978-3-030-45190-5_8 2020

Show all 59 references
  1. [9]

    Jaroslav Bendík, Ivana Černá, and Nikola Beneš. 2018. Recursive Online Enumeration of All Minimal Unsatisfiable Subsets. In Automated Technology for Verification and Analysis (ATV A 2018) (Lecture Notes in Computer Science, Vol. 11138). Springer, Cham, 143–159. doi:10.1007/978...

    2018 doi

  2. [10]

    Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly declarative specification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications. 243–262. doi:10.1145/1639949.1640108

    2009

  3. [11]

    Stefano Ceri, Georg Gottlob, and Letizia Tanca. 1990. Logic Programming and Databases: An Overview.Logic Programming and Databases(1990), 1–15. doi:10.1007/978-3-642-83952-8_1

    1990 doi

  4. [12]

    John W Chinneck and Erik W Dravnieks. 1991. Locating minimal infeasible constraint sets in linear programs.ORSA Journal on Computing3, 2 (1991), 157–168. doi:10.1287/ijoc.3.2.157

    1991 doi

  5. [13]

    Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. 2007. ProbLog: A probabilistic Prolog and its application in link discovery. InIJCAI 2007, Proceedings of the 20th international joint conference on artificial intelligence. IJCAI-INT JOINT CONF ARTIF INTELL, 2462–2467

    2007

  6. [14]

    Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. 2006. A scalable algorithm for minimal unsatisfiable core extraction. InInternational conference on theory and applications of satisfiability testing. Springer, 36–41. doi:10.1007/11814948_5

    2006 doi

  7. [15]

    Norbert Fuhr. 1995. Probabilistic datalog—a logic for powerful retrieval methods. InProceedings of the 18th annual international ACM SIGIR conference on Research and development in information retrieval. 282–290. doi:10.1145/215206.215372

    1995

  8. [16]

    R. M. Gasca, C. Del Valle, M. T. Gómez-López, and R. Ceballos. 2007. NMUS: Structural Analysis for Improving the Derivation of All MUSes in Overconstrained Numeric CSPs. InCurrent Topics in Artificial Intelligence: 12th Conference of the Spanish Association for Artificial Inte...

    2007 doi

  9. [17]

    John Gleeson and Jennifer Ryan. 1990. Identifying minimally infeasible subsystems of inequalities.ORSA Journal on Computing 2, 1 (1990), 61–63. doi:10.1287/ijoc.2.1.61

    1990 doi

  10. [18]

    Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Peter Lindner. 2022. Generative datalog with continuous distributions.J. ACM69, 6 (2022), 1–52. doi:10.1145/3559102

    2022 doi

  11. [19]

    Vedad Hadžić, Gaëtan Cassiers, Robert Primas, Stefan Mangard, and Roderick Bloem. 2024. Quantile: Quantifying Information Leakage.IACR Transactions on Cryptographic Hardware and Embedded Systems2024, 1 (2024), 433–456. doi:10.46586/tches.v2024. i1.433-456

    2024 doi

  12. [20]

    Kihong Heo, Mukund Raghothaman, Xujie Si, and Mayur Naik. 2019. Continuously reasoning about programs using differential bayesian inference. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 561–575. doi:10.1145/3314221.3314616

    2019

  13. [21]

    Herbert Jordan, Bernhard Scholz, and Pavle Subotić. 2016. Soufflé: On synthesis of program analyzers. InInternational Conference on Computer Aided Verification. Springer, 422–430. doi:10.1007/978-3-319-41540-6_23

    2016 doi

  14. [22]

    Markus Kusano and Chao Wang. 2016. Flow-sensitive composition of thread-modular abstract interpretation. InProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. 799–809. doi:10.1145/2950290.2950291

    2016

  15. [23]

    Markus Kusano and Chao Wang. 2017. Thread-modular static analysis for relaxed memory models. InProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. 337–348. doi:10.1145/3106237.3106243

    2017

  16. [24]

    Tianchi Li and Xin Zhang. 2025. Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences. Proceedings of the ACM on Programming Languages9, OOPSLA1 (2025), 1774–1801. doi:10.1145/3720508

    2025 doi

  17. [25]

    Ziyang Li, Jiani Huang, and Mayur Naik. 2023. Scallop: A language for neurosymbolic programming.Proceedings of the ACM on Programming Languages7, PLDI (2023), 1463–1487. doi:10.1145/3591280

    2023 doi

  18. [26]

    Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva

    Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. 2016. Fast, flexible MUS enumeration.Constraints 21, 2 (2016), 223–250. doi:10.1007/s10601-015-9183-0

    2016 doi

  19. [27]

    Liffiton and Karem A

    Mark H. Liffiton and Karem A. Sakallah. 2005. On Finding All Minimally Unsatisfiable Subformulas. InTheory and Applications of Satisfiability Testing, F. Bacchus and T. Walsh (Eds.). Lecture Notes in Computer Science, Vol. 3569. Springer-Verlag Berlin Heidelberg, 173–186. doi:...

    2005 doi

  20. [28]

    Liffiton and Karem A

    Mark H. Liffiton and Karem A. Sakallah. 2008. Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints.Journal of Automated Reasoning40, 1 (2008), 1–33. doi:10.1007/s10817-007-9084-z

    2008 doi

  21. [29]

    Inês Lynce and João Silva. 2004. On Computing Minimum Unsatisfiable Cores, In The Seventh International Conference on Theory and Applications of Satisfiability Testing.LNCS

    2004

  22. [30]

    Magnus Madsen, Ming-Ho Yee, and Ondřej Lhoták. 2016. From datalog to flix: A declarative language for fixed points on lattices. ACM SIGPLAN Notices51, 6 (2016), 194–208. doi:10.1145/2980983.2908096

    2016

  23. [31]

    Brian Milch, Bhaskara Marthi, Stuart Russell, David Sontag, Daniel L Ong, and Andrey Kolobov. 2007. Blog: Probabilistic models with unknown objects.Statistical relational learning(2007), 373. doi:10.7551/mitpress/7432.003.0015

    2007 doi

  24. [32]

    Maher Mneimneh, Inês Lynce, Zaher Andraus, João Marques-Silva, and Karem Sakallah. 2005. A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. InInternational Conference on Theory and Applications of Satisfiability Testing. Springer, 467–474. doi...

    2005 doi

  25. [33]

    Chris Mungall. 2009. Experiences using logic programming in bioinformatics. InInternational Conference on Logic Programming. Springer, 1–21. doi:10.1007/978-3-642-02846-5_1

    2009 doi

  26. [34]

    Mayur Naik, Alex Aiken, and John Whaley. 2006. Effective static race detection for Java. InProceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation. 308–319. doi:10.1145/1133981.1134018

    2006

  27. [35]

    Yoonna Oh, Maher N Mneimneh, Zaher S Andraus, Karem A Sakallah, and Igor L Markov. 2004. AMUSE: a minimally-unsatisfiable subformula extractor. InProceedings of the 41st annual design automation conference. 518–523. doi:10.1145/996566.996710

    2004

  28. [36]

    Mukund Raghothaman, Sulekha Kulkarni, Kihong Heo, and Mayur Naik. 2018. User-Guided Program Reasoning Using Bayesian Inference. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation(Philadelphia, 26 Chen et al. PA, USA)(PLDI 2018). ...

    2018

  29. [37]

    Seemanta Saha, Surendra Ghentiyala, Shihua Lu, Lucas Bang, and Tevfik Bultan. 2023. Obtaining information leakage bounds via approximate model counting.Proceedings of the ACM on Programming Languages7, PLDI (2023), 1488–1509. doi:10.1145/3591281

    2023 doi

  30. [38]

    Marco Scutari. 2010. Learning Bayesian networks with the bnlearn R package.Journal of statistical software35 (2010), 1–22. doi:10.18637/jss.v035.i03

    2010 doi

  31. [39]

    Jiwon Seo. 2018. Datalog extensions for bioinformatic data analysis. In2018 40th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC). IEEE, 1303–1306. doi:10.1109/EMBC.2018.8512571

    2018

  32. [40]

    Jiwon Seo, Stephen Guo, and Monica S Lam. 2015. SociaLite: An efficient graph query language based on datalog.IEEE Transactions on Knowledge and Data Engineering27, 7 (2015), 1824–1837. doi:10.1109/TKDE.2015.2405562

    2015

  33. [41]

    Jiwon Seo, Jongsoo Park, Jaeho Shin, and Monica S Lam. 2013. Distributed socialite: A datalog-based language for large-scale graph analysis.Proceedings of the VLDB Endowment6, 14 (2013), 1906–1917. doi:10.14778/2556549.2556572

    2013

  34. [42]

    Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, and Mana Taghdiri. 2003. Debugging overconstrained declarative models using unsatisfiable cores. In18th IEEE International Conference on Automated Software Engineering, 2003. Proceedings. IEEE, 94–105. doi:10.1109...

    2003 arXiv

  35. [44]

    Roni Stern, Meir Kalech, Alexander Feldman, and Gregory Provan. 2012. Exploring the duality in conflict-directed model-based diagnosis. InProceedings of the AAAI Conference on Artificial Intelligence, Vol. 26. 828–834. doi:10.1609/aaai.v26i1.8231

    2012 doi

  36. [45]

    Lahiri, Constantin Enea, and Chao Wang

    Chungha Sung, Shuvendu K. Lahiri, Constantin Enea, and Chao Wang. 2018. Datalog-Based Scalable Semantic Diffing of Concur- rent Programs. InProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering(Montpellier, France)(ASE 2018). ACM, New York...

    2018

  37. [46]

    SATO Taisuke. 1995. A statistical learning method for logic programs with distribution semantics. InProceedings of ICLP. 715–729. doi:10.7551/mitpress/4298.003.0069

    1995 doi

  38. [47]

    K Tuncay Tekle, Michael Gorbovitski, and Yanhong A Liu. 2010. Graph queries through datalog optimizations. InProceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming. 25–34. doi:10.1145/ 1836089.1836093

    2010

  39. [48]

    Saeid Tizpaz-Niari, Pavol Čern`y, and Ashutosh Trivedi. 2019. Quantitative mitigation of timing side channels. InInternational conference on computer aided verification. Springer, 140–160. doi:10.1007/978-3-030-25540-4_8

    2019 doi

  40. [49]

    Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. 2008. Finding minimal unsatisfiable cores of declarative specifications. InInternational symposium on formal methods. Springer, 326–341. doi:10.1007/978-3-540-68237-0_23

    2008 doi

  41. [50]

    Jeffrey D. Ullman. 1988.Principles of Database and Knowledge-Base Systems, Volume I. Principles of Computer Science Series, Vol. 14. Computer Science Press. https://dblp.org/rec/books/cs/Ullman88

    1988

  42. [51]

    JNM Van Loon. 1981. Irreducibly inconsistent systems of linear inequalities.European Journal of Operational Research8, 3 (1981), 283–288. doi:10.1016/0377-2217(81)90177-6

    1981 doi

  43. [52]

    Joost Vennekens, Marc Denecker, and Maurice Bruynooghe. 2009. CP-logic: A language of causal probabilistic events and its relation to logic programming.Theory and practice of logic programming9, 3 (2009), 245–308. doi:10.1017/S1471068409003767

    2009 doi

  44. [53]

    Joost Vennekens, Sofie Verbaeten, and Maurice Bruynooghe. 2004. Logic programs with annotated disjunctions. InInternational Conference on Logic Programming. Springer, 431–445. doi:10.1007/978-3-540-27775-0_30

    2004 doi

  45. [54]

    Jingbo Wang, Shashin Halalingaiah, Weiyi Chen, Chao Wang, and Işil Dillig. 2025. Probabilistic Inference for Datalog with Correlated Inputs.Proceedings of the ACM on Programming LanguagesOOPSLA2 (2025). doi:10.1145/3763058

    2025 doi

  46. [55]

    Jingbo Wang, Chungha Sung, Mukund Raghothaman, and Chao Wang. 2021. Data-driven synthesis of provably sound side channel analyses. In2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 810–822. doi:10.1109/ ICSE43902.2021.00079 Conflict Extraction...

    2021

  47. [56]

    Jingbo Wang, Chungha Sung, and Chao Wang. 2019. Mitigating power side channels during compilation. InProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 590–601. doi:10.1145/333890...

    2019

  48. [57]

    John Whaley, Dzintars Avots, Michael Carbin, and Monica S Lam. 2005. Using Datalog with binary decision diagrams for program analysis. InAsian Symposium on Programming Languages and Systems. Springer, 97–118. doi:10.1007/11575467_8

    2005 doi

  49. [58]

    Jun Zhang, Pengfei Gao, Fu Song, and Chao Wang. 2018. SCInfer: Refinement-based verification of software countermeasures against side-channel attacks. InInternational Conference on Computer Aided Verification. Springer, 157–177. doi:10.1007/978-3- 319-96142-2_12

    2018 doi

  50. [59]

    Xin Zhang, Radu Grigore, Xujie Si, and Mayur Naik. 2017. Effective interactive resolution of static analysis alarms.Proceedings of the ACM on Programming Languages1, OOPSLA (2017), 1–30. doi:10.1145/3133881

    2017 doi

  51. [60]

    Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program analyses in Datalog. InProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 239–248. doi:10.1145/2594291.2594327

    2014

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.