2024
Verifying Lock-Free Search Structure Templates (Artifact).
Dagstuhl Artifacts Ser., 2024
Characterizing Implementability of Global Protocols with Infinite States and Data.
CoRR, 2024
Arithmetizing Shape Analysis.
CoRR, 2024
Inferring Accumulative Effects of Higher Order Programs.
CoRR, 2024
Deciding Subtyping for Asynchronous Multiparty Sessions.
Proceedings of the Programming Languages and Systems, 2024
Verifying Lock-Free Search Structure Templates.
Proceedings of the 38th European Conference on Object-Oriented Programming, 2024
Verifying Concurrent Search Structures (Invited Talk).
Proceedings of the 35th International Conference on Concurrency Theory, 2024
2023
Embedding Hindsight Reasoning in Separation Logic.
Proc. ACM Program. Lang., 2023
Context-Aware Separation Logic.
CoRR, 2023
Make Flows Small Again: Revisiting the Flow Framework.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023
nekton: A Linearizability Proof Checker.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023
Complete Multiparty Session Type Projection with Automata.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023
2022
A concurrent program logic with a future and history.
Proc. ACM Program. Lang., 2022
Less is more: refinement proofs for probabilistic proofs.
IACR Cryptol. ePrint Arch., 2022
Needles in a Haystack: Using PORT to Catch Bad Behaviors within Application Recordings.
Proceedings of the 17th International Conference on Software Technologies, 2022
2021
Automated Verification of Concurrent Search Structures
Synthesis Lectures on Computer Science, Morgan & Claypool Publishers, ISBN: 978-3-031-01806-0, 2021
Data flow refinement type inference.
Proc. ACM Program. Lang., 2021
Verifying concurrent multicopy search structures.
Proc. ACM Program. Lang., 2021
Automated repair for timed systems.
Formal Methods Syst. Des., 2021
Inverse-Weighted Survival Games.
Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, 2021
2020
Beyond The Text: Analysis of Privacy Statements through Syntactic and Semantic Role Labeling.
CoRR, 2020
Verifying concurrent search structure templates.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020
Local Reasoning for Global Graph Properties.
Proceedings of the Programming Languages and Systems, 2020
TarTar: A Timed Automata Repair Tool.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020
2019
VACCINE: Using Contextual Integrity For Data Leakage Detection.
Proceedings of the World Wide Web Conference, 2019
Charting a Course Through Uncertain Environments: SEA Uses Past Problems to Avoid Future Failures.
Proceedings of the 30th IEEE International Symposium on Software Reliability Engineering, 2019
Clock Bound Repair for Timed Systems.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019
2018
Go with the flow: compositional abstractions for concurrent data structures.
Proc. ACM Program. Lang., 2018
RECIPE: Applying Open Domain Question Answering to Privacy Policies.
Proceedings of the Workshop on Machine Reading for Question Answering@ACL 2018, 2018
2017
Full accounting for verifiable outsourcing.
IACR Cryptol. ePrint Arch., 2017
Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version).
CoRR, 2017
The VACCINE Framework for Building DLP Systems.
CoRR, 2017
Partitioned Memory Models for Program Analysis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017
2016
Complete Instantiation-Based Interpolation.
J. Autom. Reason., 2016
Crowdsourcing Verifiable Contextual Integrity Norms.
CoRR, 2016
Classifying Bugs with Interpolants.
Proceedings of the Tests and Proofs - 10th International Conference, 2016
Learning Privacy Expectations by Crowdsourcing Contextual Informational Norms.
Proceedings of the Fourth AAAI Conference on Human Computation and Crowdsourcing, 2016
Error Invariants for Concurrent Traces.
Proceedings of the FM 2016: Formal Methods, 2016
2015
Learning Invariants using Decision Trees.
CoRR, 2015
Finding Minimum Type Error Sources.
Proceedings of the Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März, 2015
Conflict-Directed Graph Coverage.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015
VERMEER: A Tool for Tracing and Explaining Faulty C Programs.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015
Practical SMT-based type error localization.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015
Deciding Local Theory Extensions via E-matching.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015
2014
Preface - Invariant Generation.
Sci. Comput. Program., 2014
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014
GRASShopper - Complete Heap Verification with Mixed Specifications.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014
Concolic Fault Localization.
Proceedings of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation, 2014
Dynamic Package Interfaces.
Proceedings of the Fundamental Approaches to Software Engineering, 2014
Automating Separation Logic with Trees and Data.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014
2013
Dynamic Package Interfaces - Extended Version.
CoRR, 2013
A Notion of Dynamic Interface for Depth-Bounded Object-Oriented Packages.
CoRR, 2013
Flow-Sensitive Fault Localization.
Proceedings of the Verification, 2013
Structural Counter Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013
Explaining inconsistent code.
Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013
Automating Separation Logic Using SMT.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013
2012
Deciding Functional Lists with Sublist Sets.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2012
Ideal Abstractions for Well-Structured Transition Systems.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012
Proceedings of the FM 2012: Formal Methods, 2012
2011
Decision Procedures for Automating Termination Proofs.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011
Static Scheduling in Clouds.
Proceedings of the 3rd USENIX Workshop on Hot Topics in Cloud Computing, 2011
Scheduling large jobs by abstraction refinement.
Proceedings of the European Conference on Computer Systems, 2011
An Efficient Decision Procedure for Imperative Tree Data Structures.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011
2010
Formal Methods Syst. Des., 2010
Building a Calculus of Data Structures.
Proceedings of the Verification, 2010
Counterexample-guided focus.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010
Forward Analysis of Depth-Bounded Processes.
Proceedings of the Foundations of Software Science and Computational Structures, 2010
A marketplace for cloud resources.
Proceedings of the 10th International conference on Embedded software, 2010
FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment.
Proceedings of the IEEE International Conference on Cloud Computing, 2010
2009
Abstraction Refinement for Quantified Array Assertions.
Proceedings of the Static Analysis, 16th International Symposium, 2009
Combining Theories with Shared Set Operations.
Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009
It's Doomed; We Can Prove It.
Proceedings of the FM 2009: Formal Methods, 2009
Proceedings of the Computer Aided Verification, 21st International Conference, 2009
2008
Heap Assumptions on Demand.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008
2007
Using First-Order Theorem Provers in the Jahob Data Structure Verification System.
Proceedings of the Verification, 2007
Shape Analysis for Composite Data Structures.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007
2006
On Verifying Complex Properties using Symbolic Shape Analysis
CoRR, 2006
Field Constraint Analysis.
Proceedings of the Verification, 2006
2005
Proceedings of the Static Analysis, 12th International Symposium, 2005