3 papers
cs.LO2021
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…
cs.AI2020
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…
cs.PL2018
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…