2024
Practical Verification of Smart Contracts using Memory Splitting.
Proc. ACM Program. Lang., 2024
A Decidable Case of Query Determinacy: Project-Select Views.
CoRR, 2024
2023
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols.
Proc. ACM Program. Lang., October, 2023
Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks.
IEEE Trans. Dependable Secur. Comput., 2023
2022
Property-directed reachability as abstract interpretation in the monotone theory.
Proc. ACM Program. Lang., 2022
This is not the End: Rethinking Serverless Function Termination.
CoRR, 2022
Blockaid: Data Access Policy Enforcement for Web Applications.
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022
2021
Learning the boundary of inductive invariants.
Proc. ACM Program. Lang., 2021
Temporal prophecy for proving temporal properties of infinite-state systems.
Formal Methods Syst. Des., 2021
Phoenix: A Formally Verified Regenerating Vault.
CoRR, 2021
Cloud-Scale Runtime Verification of Serverless Applications.
Proceedings of the SoCC '21: ACM Symposium on Cloud Computing, 2021
Summing up Smart Transitions.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021
2020
Complexity and information in invariant inference.
Proc. ACM Program. Lang., 2020
Taming callbacks for smart contract modularity.
Proc. ACM Program. Lang., 2020
Invited Talk: Harnessing SMT Solvers for Verifying Low Level Programs.
Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020
2019
Bounded Quantifier Instantiation for Checking Inductive Invariants.
Log. Methods Comput. Sci., 2019
Some complexity results for stateful network verification.
Formal Methods Syst. Des., 2019
Automating Cluster Management with Weave.
CoRR, 2019
Simple and precise static analysis of untrusted Linux kernel extensions.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019
Synthesizing Cluster Management Code for Distributed Systems.
Proceedings of the Workshop on Hot Topics in Operating Systems, 2019
Inferring Inductive Invariants from Phase Structures.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019
2018
Reducing liveness to safety in first-order logic.
Proc. ACM Program. Lang., 2018
Online detection of effectively callback free objects with applications to smart contracts.
Proc. ACM Program. Lang., 2018
Secure serverless computing using dynamic information flow control.
Proc. ACM Program. Lang., 2018
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018
Abstract Interpretation of Stateful Networks.
Proceedings of the Static Analysis - 25th International Symposium, 2018
Modularity for decidability of deductive verification with applications to distributed systems.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018
Core-Guided Minimal Correction Set and Core Enumeration.
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018
Verifying Properties of Binarized Deep Neural Networks.
Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018
2017
Automatic Scalable Atomicity via Semantic Locking.
ACM Trans. Parallel Comput., 2017
Synthesis of circular compositional program proofs via abduction.
Int. J. Softw. Tools Technol. Transf., 2017
Paxos made EPR: decidable reasoning about distributed protocols.
Proc. ACM Program. Lang., 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
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
Abduction for Learning Smart City Rules.
Proceedings of the GCAI 2017, 2017
Verifying Equivalence of Spark Programs.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017
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
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
ACM SIGPLAN Notices, 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
POPL'11 program chair's report.
ACM SIGPLAN Notices, 2012
An introduction to data representation synthesis.
Commun. ACM, 2012
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
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
Log. Methods Comput. Sci., 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
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 Distributed Comput., 2007
A logic of reachable patterns in linked data-structures.
J. Log. Algebraic Methods Program., 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
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
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.
Proceedings of the Compiler Design Handbook: Optimizations and Machine Code Generation, 2007
2006
Install-Time Vaccination of Windows Executables to Defend against Stack Smashing Attacks.
IEEE Trans. Dependable Secur. Comput., 2006
Verifying Temporal Heap Properties Specified via Evolution Logic.
Log. J. 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
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.
Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, 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
Interprocedural Shape Analysis for Cutpoint-Free Programs.
Proceedings of the Static Analysis, 12th International Symposium, 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
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
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.
Proceedings of the 2003 Workshop on Software Model Checking, 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
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.
Proceedings of the Compiler Design Handbook: Optimizations and Machine Code Generation, 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
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
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 Informatica, 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
1996
Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation.
Theor. Comput. Sci., 1996
1995
Demand Interprocedural Dataflow Analysis.
Proceedings of the Third ACM SIGSOFT Symposium on Foundations of Software Engineering, 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
Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, 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
1991
High level formalisms for program flow analysis and their use in compiling.
PhD thesis, 1991
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