Zobrazeno 1 - 10
of 25
pro vyhledávání: '"Oded Padon"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 18, Issue 3 (2022)
We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mech
Externí odkaz:
https://doaj.org/article/af77f4ffff944dc5b9b4fa94be3184e8
Publikováno v:
Logical Methods in Computer Science, Vol Volume 15, Issue 3 (2019)
We consider the problem of checking whether a proposed invariant $\varphi$ expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. While the problem is undecidable, modern SMT solvers can sometimes
Externí odkaz:
https://doaj.org/article/e50a2da54e4048988bd09ac5c12248a2
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:1-29
Many invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We present a new formal duality between states and predicates, and use
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030720155
TACAS (1)
Tools and Algorithms for the Construction and Analysis of Systems
TACAS (1)
Tools and Algorithms for the Construction and Analysis of Systems
We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mech
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6c012e58eb99cf40a4c6d880e7d47570
https://doi.org/10.46298/lmcs-18(3:26)2022
https://doi.org/10.46298/lmcs-18(3:26)2022
Autor:
Jochen Hoenicke, Andreas Podelski, Sharon Shoham, Kenneth L. McMillan, Mooly Sagiv, Oded Padon
Publikováno v:
2018 Formal Methods in Computer Aided Design (FMCAD)
FMCAD
FMCAD
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but
Autor:
Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia
Publikováno v:
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation.
Publikováno v:
PLDI
We consider the problem of program synthesis from input-output examples via stochastic search. We identify a robust feature of stochastic synthesis: The search often progresses through a series of discrete plateaus. We observe that the distribution o
Publikováno v:
PLDI
Quantified first-order formulas, often with quantifier alternations, are increasingly used in the verification of complex systems. While automated theorem provers for first-order logic are becoming more robust, invariant inference tools that handle q
Autor:
Oded Padon, Kenneth L. McMillan
Publikováno v:
Computer Aided Verification ISBN: 9783030532901
CAV (2)
CAV (2)
Ivy is a multi-modal verification tool for correct design and implementation of distributed protocols and algorithms, supporting modular specification, implementation and proof. Ivy supports proving safety and liveness properties of parameterized and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3507705bc3639eafe32e4bde7543aa7f
https://doi.org/10.1007/978-3-030-53291-8_12
https://doi.org/10.1007/978-3-030-53291-8_12
Publikováno v:
SOSP
Existing deep neural network (DNN) frameworks optimize the computation graph of a DNN by applying graph transformations manually designed by human experts. This approach misses possible graph optimizations and is difficult to scale, as new DNN operat