Zobrazeno 1 - 10
of 153
pro vyhledávání: '"Mooly Sagiv"'
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:
Logical Methods in Computer Science, Vol Volume 5, Issue 2 (2009)
This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One o
Externí odkaz:
https://doaj.org/article/7a194078d8864248860b9e2de93bfef0
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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3646023232fe77e97a767d75672a6d30
https://doi.org/10.1007/s10703-021-00377-1
https://doi.org/10.1007/s10703-021-00377-1
Autor:
Clara Rodríguez-Núñez, Noam Rinetzky, Shelly Grossman, Albert Rubio, Elvira Albert, Mooly Sagiv
Publikováno v:
Proceedings of the ACM on Programming Languages. 4:1-30
Callbacks are an effective programming discipline for implementing event-driven programming, especially in environments like Ethereum which forbid shared global state and concurrency. Callbacks allow a callee to delegate the execution back to the cal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f6ca5c095b369bb6c8d1314bab94a90f
https://doi.org/10.1145/3428277
https://doi.org/10.1145/3428277
Publikováno v:
Proceedings of the ACM on Programming LanguagesVolume 6Issue POPL
Inferring inductive invariants is one of the main challenges of formal verification. The theory of abstract interpretation provides a rich framework to devise invariant inference algorithms. One of the latest breakthroughs in invariant inference is p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d07d358306a7a806049d81362ab8a9ad
Publikováno v:
SoCC
Serverless platforms aim to simplify the deployment, scaling, and management of cloud applications. Serverless applications are inherently distributed, and are executed using shortlived ephemeral processes. The use of short-lived ephemeral processes
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::552e40c5e87cc77e218b66591d783e45
https://doi.org/10.1145/3472883.3486977
https://doi.org/10.1145/3472883.3486977
Publikováno v:
Proceedings of the ACM on Programming Languages
This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c24290948dfcd60a249d18f61058ce6f
https://doi.org/10.1145/3371073
https://doi.org/10.1145/3371073
Autor:
Alexander Rabinovich, Kalev Alpernas, Mooly Sagiv, Aurojit Panda, Yaron Velner, Sharon Shoham, Scott Shenker
Publikováno v:
Formal Methods in System Design
In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typ
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b7e5b46fa41d746092d385e22c32a4bb
http://arxiv.org/abs/2106.01030
http://arxiv.org/abs/2106.01030
Publikováno v:
Computer Aided Verification-33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I
Computer Aided Verification ISBN: 9783030816841
CAV (1)
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Computer Aided Verification
Computer Aided Verification ISBN: 9783030816841
CAV (1)
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Computer Aided Verification
Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a tr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::97f9e5531f52c33df2d44af6c58887aa
Publikováno v:
Proceedings of the ACM on Programming Languages
We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, which permits applying theoretical results from exact concept learning t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d867c89ac4f5750f9787a7c99bcf2149