Sharon Shoham | DeepAI

AI Chat

Featured Co-authors

Constantin Enea
23 publications
Mooly Sagiv
19 publications
Eran Yahav
18 publications
Alex Aiken
16 publications
Aurojit Panda
14 publications
Arie Gurfinkel
14 publications
Oded Padon
13 publications
Yuting Chen
11 publications
Scott Shenker
10 publications
Adam Morrison
9 publications
Noam Rinetzky
9 publications

∙ 08/23/2023

State Merging with Quantifiers in Symbolic Execution

We address the problem of constraint encoding explosion which hinders th...

0 David Trabish, et al. ∙

∙ 06/30/2023

Speculative SAT Modulo SAT

State-of-the-art model-checking algorithms like IC3/PDR are based on uni...

0 Hari Govind V K, et al. ∙

∙ 06/16/2023

Fast Approximations of Quantifier Elimination

Quantifier elimination (qelim) is used in many automated reasoning tasks...

0 Isabel Garcia-Contreras, et al. ∙

∙ 04/25/2023

Hyperproperty Verification as CHC Satisfiability

Hyperproperties govern the behavior of a system or systems across multip...

0 Shachar Itzhaky, et al. ∙

∙ 08/15/2022

Invariant Inference With Provable Complexity From the Monotone Theory

Invariant inference algorithms such as interpolation-based inference and...

0 Yotam M. Y. Feldman, et al. ∙

∙ 12/10/2021

Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion

We present a PDR/IC3 algorithm for finding inductive invariants with qua...

0 Jason R. Koenig, et al. ∙

∙ 10/30/2021

Property-Directed Reachability as Abstract Interpretation in the Monotone Theory

Inferring inductive invariants is one of the main challenges of formal v...

0 Yotam M. Y. Feldman, et al. ∙

∙ 07/26/2021

Logical Characterization of Coherent Uninterpreted Programs

An uninterpreted program (UP) is a program whose semantics is defined ov...

0 Hari Govind V K, et al. ∙

∙ 06/02/2021

Some Complexity Results for Stateful Network Verification

In modern networks, forwarding of packets often depends on the history o...

0 Kalev Alpernas, et al. ∙

∙ 06/02/2021

Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems

Various verification techniques for temporal properties transform tempor...

0 Oded Padon, et al. ∙

∙ 06/02/2021

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction

Automatic verification of array manipulating programs is a challenging p...

0 Oren Ish Shalom, et al. ∙

∙ 06/01/2021

Modular Verification of Concurrent Programs via Sequential Model Checking

This work utilizes the plethora of work on verification of sequential pr...

0 Dan Rasin, et al. ∙

∙ 06/01/2021

Quantifiers on Demand

Automated program verification is a difficult problem. It is undecidable...

0 Arie Gurfinkel, et al. ∙

∙ 10/02/2020

Proving Highly-Concurrent Traversals Correct

Modern highly-concurrent search data structures, such as search trees, o...

0 Yotam M. Y. Feldman, et al. ∙

∙ 09/06/2020

A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs

Data race free (DRF) programs constitute an important class of concurren...

0 Suvam Mukherjee, et al. ∙

∙ 08/22/2020

Learning the Boundary of Inductive Invariants

We study the complexity of invariant inference and its connections to ex...

0 Yotam M. Y. Feldman, et al. ∙

∙ 05/27/2020

Global Guidance for Local Generalization in Model Checking

SMT-based model checkers, especially IC3-style ones, are currently the m...

0 Hari Govind V K, et al. ∙

∙ 10/27/2019

Complexity and Information in Invariant Inference

This paper addresses the complexity of SAT-based invariant inference, a ...

0 Yotam M. Y. Feldman, et al. ∙

∙ 05/19/2019

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics

Verification of fault-tolerant distributed protocols is an immensely dif...

0 Idan Berkovits, et al. ∙

∙ 05/19/2019

Inferring Inductive Invariants from Phase Structures

Infinite-state systems such as distributed protocols are challenging to ...

0 Yotam M. Y. Feldman, et al. ∙

∙ 05/19/2019

Property Directed Self Composition

We address the problem of verifying k-safety properties: properties that...

0 Ron Shemer, et al. ∙

∙ 12/03/2018

Undecidability of Inferring Linear Integer Invariants

We show that the problem of determining the existence of an inductive in...

0 Sharon Shoham, et al. ∙

∙ 05/10/2018

Order out of Chaos: Proving Linearizability Using Local Views

Proving the linearizability of highly concurrent data structures, such a...

0 Yotam M. Y. Feldman, et al. ∙

∙ 10/24/2017

Bounded Quantifier Instantiation for Checking Inductive Invariants

We consider the problem of checking whether a proposed invariant ϕ expre...

0 Yotam M. Y. Feldman, et al. ∙

∙ 10/19/2017

Paxos Made EPR: Decidable Reasoning about Distributed Protocols

Distributed protocols such as Paxos play an important role in many compu...

0 Oded Padon, et al. ∙

∙ 10/03/2017

Programming Not Only by Example

In recent years, there has been tremendous progress in automated synthes...

0 Hila Peleg, et al. ∙

∙ 08/19/2017

Abstractions for Verifying Isolation Properties in Stateful Networks

Modern networks achieve robustness and scalability by maintaining states...

0 Kalev Alpernas, et al. ∙

∙ 08/19/2017

Modular Safety Verification for Stateful Networks

Modern networks achieve robustness and scalability by maintaining states...

0 Kalev Alpernas, et al. ∙

Are you a researcher?
Expose your work
to one of the largest
A.I. communities in the world