28 citations · 46 across the 8 of their papers we have counts for
9 papers
Beyond Output Faithfulness: Learning Attributions that Preserve Computational Pathways
Siyu Zhang, Kenneth Mcmillan
Faithfulness metrics such as insertion and deletion evaluate how feature removal affects model outputs but overlook whether explanations preserve the computational pathway the netw…
A Case Study in Analytic Protocol Analysis in ACL2
Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan +2
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of math…
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
Wenxi Wang, Yang Hu, Mohit Tiwari +3
Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are base…
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan +3
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imp…
Bayesian Interpolants as Explanations for Neural Inferences
Kenneth L. McMillan
The notion of Craig interpolant, used as a form of explanation in automated reasoning, is adapted from logical inference to statistical inference and used to explain inferences mad…
Learning Abstractions for Program Synthesis
Xinyu Wang, Greg Anderson, Isil Dillig +1
Many example-guided program synthesis techniques use abstractions to prune the search space. While abstraction-based synthesis has proven to be very powerful, a domain expert needs…
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel +1
We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely…
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
Nikolaj Bjorner, Ken McMillan, Andrey Rybalchenko
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs di…
Interpolant-Based Transition Relation Approximation
Ranjit Jhala, Kenneth L. McMillan
In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software mode…