Shmuel Sagiv

According to our database1, Shmuel Sagiv
  • authored at least 167 papers between 1989 and 2017.
  • has a "Dijkstra number"2 of three.

Awards

ACM Fellow

ACM Fellow 2015, "For contributions to the theory and practice of automated analysis and verification of software.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2017
Automatic Scalable Atomicity via Semantic Locking.
TOPC, 2017

Synthesis of circular compositional program proofs via abduction.
STTT, 2017

Paxos made EPR: decidable reasoning about distributed protocols.
PACMPL, 2017

Bounded Quantifier Instantiation for Checking Inductive Invariants.
CoRR, 2017

Paxos Made EPR: Decidable Reasoning about Distributed Protocols.
CoRR, 2017

Verifying Properties of Binarized Deep Neural Networks.
CoRR, 2017

Modular Safety Verification for Stateful Networks.
CoRR, 2017

Conjunctive Abstract Interpretation Using Paramodulation.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Property Directed Reachability for Proving Absence of Concurrent Modification Errors.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Bounded Quantifier Instantiation for Checking Inductive Invariants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Verifying Reachability in Networks with Mutable Datapaths.
Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, 2017

On the Automated Verification of Web Applications with Embedded SQL.
Proceedings of the 20th International Conference on Database Theory, 2017

Verification in the Age of Microservices.
Proceedings of the 16th Workshop on Hot Topics in Operating Systems, 2017

Verifying Equivalence of Spark Programs.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
Verifying Reachability in Networks with Mutable Datapaths.
CoRR, 2016

On the automated verification of web applications with embedded SQL.
CoRR, 2016

Some Complexity Results for Stateful Network Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Decidability of inferring inductive invariants.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Ivy: safety verification by interactive generalization.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk).
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

2015
New Directions for Network Verification.
Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis.
Proceedings of the Static Analysis - 22nd International Symposium, 2015

Automatic scalable atomicity via semantic locking.
Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2015

Decentralizing SDN Policies.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Composing concurrency control.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2014
Verifying Isolation Properties in the Presence of Middleboxes.
CoRR, 2014

Automatic semantic locking.
Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2014

Modular reasoning about heap paths via effectively propositional formulas.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

VeriCon: towards verifying controller programs in software-defined networks.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Verifying atomicity via data independence.
Proceedings of the International Symposium on Software Testing and Analysis, 2014

Checking Linearizability of Encapsulated Extended Operations.
Proceedings of the Programming Languages and Systems, 2014

Property-Directed Shape Analysis.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Principles of POPL.
SIGPLAN Notices, 2013

Synthesis of Circular Compositional Program Proofs via Abduction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Concurrent libraries with foresight.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Turning nondeterminism into parallelism.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Effectively-Propositional Reasoning about Reachability in Linked Data Structures.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012
An introduction to data representation synthesis.
Commun. ACM, 2012

Abstractions from tests.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

JANUS: exploiting parallelism via hindsight.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Concurrent data representation synthesis.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Understanding the behavior of database operations under program control.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Reasoning about Lock Placements.
Proceedings of the Programming Languages and Systems, 2012

Eventually Consistent Transactions.
Proceedings of the Programming Languages and Systems, 2012

2011
Data representation synthesis.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Precise and compact modular procedure summaries for heap manipulating programs.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

HAWKEYE: effective discovery of dataflow impediments to parallelization.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Testing atomicity of composed concurrent operations.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Automatic fine-grain locking using shape properties.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

2010
Verifying safety properties of concurrent heap-manipulating programs.
ACM Trans. Program. Lang. Syst., 2010

Finite differencing of logical formulas for static analysis.
ACM Trans. Program. Lang. Syst., 2010

A relational approach to interprocedural shape analysis.
ACM Trans. Program. Lang. Syst., 2010

Decidable fragments of many-sorted logic.
J. Symb. Comput., 2010

Field-sensitive program dependence analysis.
Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Statically Inferring Complex Heap, Array, and Numeric Invariants.
Proceedings of the Static Analysis - 17th International Symposium, 2010

A dynamic evaluation of the precision of static heap abstractions.
Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2010

A simple inductive synthesis methodology and its applications.
Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2010

Specifying and verifying sparse matrix codes.
Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

Data Structure Fusion.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
Self-stabilization preserving compiler.
ACM Trans. Program. Lang. Syst., 2009

Simulating reachability using first-order logic with applications to verification of linked data structures
Logical Methods in Computer Science, 2009

Thread-Modular Shape Analysis.
Proceedings of the Verification, 2009

A combination framework for tracking partition sizes.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs.
Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs.
Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

Generalizing DPLL to Richer Logics.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Abstract Transformers for Thread Correlation Analysis.
Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008
On the complexity of partially-flow-sensitive alias analysis.
ACM Trans. Program. Lang. Syst., 2008

Heap Decomposition for Concurrent Shape Analysis.
Proceedings of the Static Analysis, 15th International Symposium, 2008

Customization change impact analysis for erp professionals via program slicing.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

Ranking Abstractions.
Proceedings of the Programming Languages and Systems, 2008

Proving Conditional Termination.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Thread Quantification for Concurrent Shape Analysis.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Introduction to special ESOP'05 issue.
ACM Trans. Program. Lang. Syst., 2007

Logical characterizations of heap abstractions.
ACM Trans. Comput. Log., 2007

Scaling model checking of dataraces using dynamic information.
J. Parallel Distrib. Comput., 2007

A logic of reachable patterns in linked data-structures.
J. Log. Algebr. Program., 2007

A Logic of Reachable Patterns in Linked Data-Structures
CoRR, 2007

Constructing Specialized Shape Analyses for Uniform Change.
Proceedings of the Verification, 2007

Shape Analysis by Graph Decomposition.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Cartesian Partial-Order Reduction.
Proceedings of the Model Checking Software, 2007

Thread-modular shape analysis.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Decidable Fragments of Many-Sorted Logic.
Proceedings of the Logic for Programming, 2007

Modular Shape Analysis for Dynamically Encapsulated Programs.
Proceedings of the Programming Languages and Systems, 2007

Revamping TVLA: Making Parametric Shape Analysis Competitive.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Leaping Loops in the Presence of Abstraction.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Comparison Under Abstraction for Verifying Linearizability.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Labelled Clauses.
Proceedings of the Automated Deduction, 2007

Local Reasoning for Storable Locks and Threads.
Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

Shape Analysis and Applications.
The Compiler Design Handbook, 2nd ed., 2007

2006
Install-Time Vaccination of Windows Executables to Defend against Stack Smashing Attacks.
IEEE Trans. Dependable Sec. Comput., 2006

Verifying Temporal Heap Properties Specified via Evolution Logic.
Logic Journal of the IGPL, 2006

Combining Shape Analyses by Intersecting Abstractions.
Proceedings of the Verification, 2006

Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm.
Proceedings of the Static Analysis, 13th International Symposium, 2006

Testing, abstraction, theorem proving: better together!
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2006

A Logic of Reachable Patterns in Linked Data-Structures.
Proceedings of the Foundations of Software Science and Computation Structures, 2006

Abstraction for Shape Analysis with Fast and Precise Transformers.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

An Appreciation of the Work of Reinhard Wilhelm.
Proceedings of the Program Analysis and Compilation, 2006

Abstract Counterexample-Based Refinement for Powerset Domains.
Proceedings of the Program Analysis and Compilation, 2006

Refinement-Based Verification for Possibly-Cyclic Lists.
Proceedings of the Program Analysis and Compilation, 2006

2005
Establishing local temporal heap safety properties with applications to compile-time memory management.
Sci. Comput. Program., 2005

Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work.
Electr. Notes Theor. Comput. Sci., 2005

Automatic Verification of Strongly Dynamic Software Systems.
Proceedings of the Verified Software: Theories, 2005

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists.
Proceedings of the Verification, 2005

Self-stabilization Preserving Compiler.
Proceedings of the Self-Stabilizing Systems, 2005

Interprocedural Shape Analysis for Cutpoint-Free Programs.
Proceedings of the Static Analysis, 12th International Symposium, 2005

Scaling model checking of dataraces using dynamic information.
Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2005

A semantics for procedure local heaps and its abstractions.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

A framework for numeric analysis of array operations.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Optimizing C Multithreaded Memory Management Using Thread-Local Storage.
Proceedings of the Compiler Construction, 14th International Conference, 2005

Abstraction Refinement via Inductive Learning.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures.
Proceedings of the Automated Deduction, 2005

2004
On the Expressive Power of Canonical Abstraction.
Proceedings of the Verification, 2004

Symbolic Implementation of the Best Transformer.
Proceedings of the Verification, 2004

Symbolically Computing Most-Precise Abstract Operations for Shape Analysis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Numeric Domains with Summarized Dimensions.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Partially Disjunctive Heap Abstraction.
Proceedings of the Static Analysis, 11th International Symposium, 2004

A Relational Approach to Interprocedural Shape Analysis.
Proceedings of the Static Analysis, 11th International Symposium, 2004

TVLA: A system for generating abstract interpreters.
Proceedings of the Building the Information Society, 2004

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics.
Proceedings of the Computer Science Logic, 18th International Workshop, 2004

Static Program Analysis via 3-Valued Logic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Verification via Structure Simulation.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Automatically Verifying Concurrent Queue Algorithms.
Electr. Notes Theor. Comput. Sci., 2003

Logical Characterizations of Heap Abstractions
CoRR, 2003

Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management.
Proceedings of the Static Analysis, 10th International Symposium, 2003

CSSV: towards a realistic tool for statically detecting all buffer overflows in C.
Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

Verifying Temporal Heap Properties Specified via Evolution Logic.
Proceedings of the Programming Languages and Systems, 2003

Finite Differencing of Logical Formulas for Static Analysis.
Proceedings of the Programming Languages and Systems, 2003

2002
Parametric shape analysis via 3-valued logic.
ACM Trans. Program. Lang. Syst., 2002

Compactly Representing First-Order Structures for Static Analysis.
Proceedings of the Static Analysis, 9th International Symposium, 2002

Deriving Specialized Program Analyses for Certifying Component-Client Conformance.
Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

Semantic Minimization of 3-Valued Propositional Formulae.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Estimating the impact of heap liveness information on space consumption in Java.
Proceedings of The Workshop on Memory Systems Performance (MSP 2002), 2002

Online Subpath Profiling.
Proceedings of the Compiler Construction, 11th International Conference, 2002

Shape Analysis and Applications.
The Compiler Design Handbook, 2002

2001
Kleene's Logic with Equality.
Inf. Process. Lett., 2001

Cleanness Checking of String Manipulations in C Programs via Integer Analysis.
Proceedings of the Static Analysis, 8th International Symposium, 2001

Heap Profiling for Space-Efficient Java.
Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2001

Interprocedural Shape Analysis for Recursive Programs.
Proceedings of the Compiler Construction, 10th International Conference, 2001

2000
TVLA: A System for Implementing Static Analyses.
Proceedings of the Static Analysis, 7th International Symposium, 2000

Checking Cleanness in Linked Lists.
Proceedings of the Static Analysis, 7th International Symposium, 2000

On the Effectiveness of GC in Java.
Proceedings of the ISMM 2000, 2000

Putting static analysis to work for verification: A case study.
Proceedings of the International Symposium on Software Testing and Analysis, 2000

A Kleene Analysis of Mobile Ambients.
Proceedings of the Programming Languages and Systems, 2000

Shape Analysis.
Proceedings of the Compiler Construction, 9th International Conference, 2000

Automatic Removal of Array Memory Leaks in Java.
Proceedings of the Compiler Construction, 9th International Conference, 2000

1999
Finding Circular Attributes in Attribute Grammars.
J. ACM, 1999

Parametric Shape Analysis via 3-Valued Logic.
Proceedings of the POPL '99, 1999

A Decidable Logic for Describing Linked Data Structures.
Proceedings of the Programming Languages and Systems, 1999

1998
Solving Shape-Analysis Problems in Languages with Destructive Updating.
ACM Trans. Program. Lang. Syst., 1998

Building a Bridge between Pointer Aliases and Program Dependences.
Nord. J. Comput., 1998

A Logic-Based Approach to Program Flow Analysis.
Acta Inf., 1998

Edge Profiling versus Path Profiling: The Showdown.
Proceedings of the POPL '98, 1998

Detecting Memory Errors via Static Pointer Analysis (Preliminary Experience).
Proceedings of the SIGPLAN/SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 1998

Building a Bridge between Pointer Aliases and Program Dependences.
Proceedings of the Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28, 1998

1996
Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation.
Theor. Comput. Sci., 1996

Solving Shape-Analysis Problems in Languages with Destructive Updating.
Proceedings of the Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1996

1995
Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation.
Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Demand Interprocedural Dataflow Analysis.
Proceedings of the SIGSOFT '95, 1995

Precise Interprocedural Dataflow Analysis via Graph Reachability.
Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

1994
Speeding up Slicing.
Proceedings of the SIGSOFT '94, 1994

1992
The Expressive Power of Side Effects in Prolog.
J. Log. Program., 1992

Proving Safety of Speculative Load Instructions at Compile Time.
Proceedings of the ESOP '92, 1992

1990
A Logic-Based Approach to Data Flow Analysis Problem.
Proceedings of the Programming Language Implementation and Logic Programming, 1990

1989
Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis.
Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989


  Loading...