2024
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations.
Proc. ACM Program. Lang., January, 2024
QED: Scalable Verification of Hardware Memory Consistency.
CoRR, 2024
P4CGO: Control Plane Guided P4 Program Optimization.
Proceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation, 2024
2023
Comparative Synthesis: Learning Near-Optimal Network Designs by Query.
Proc. ACM Program. Lang., January, 2023
2022
Bootstrapping Library-Based Synthesis.
Proceedings of the Static Analysis - 29th International Symposium, 2022
2021
Comparative Synthesis: Learning Optimal Programs with Indeterminate Objectives.
CoRR, 2021
Reasoning about recursive tree traversals.
Proceedings of the PPoPP '21: 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2021
2020
Vision Paper: Grand Challenges in Resilience: Autonomous System Resilience through Design and Runtime Measures.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
IEEE Open J. Comput. Soc., 2020
Streaming Transformations of Infinite Ordered-Data Words.
CoRR, 2020
Reconciling enumerative and deductive program synthesis.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020
2019
Program synthesis with algebraic library specifications.
Proc. ACM Program. Lang., 2019
Grand Challenges of Resilience: Autonomous System Resilience through Design and Runtime Measures.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
CoRR, 2019
A Decidable Logic for Tree Data-Structures with Measurements.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019
Learning Network Design Objectives Using A Program Synthesis Approach.
Proceedings of the 18th ACM Workshop on Hot Topics in Networks, 2019
2018
Reconciling Enumerative and Symbolic Search in Syntax-Guided Synthesis.
CoRR, 2018
2017
Natural synthesis of provably-correct data-structure manipulations.
Proc. ACM Program. Lang., 2017
An empirical study of adaptive concretization for parallel program synthesis.
Formal Methods Syst. Des., 2017
Synthesis of Recursive ADT Transformations from Reusable Templates.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017
2016
Synthesizing framework models for symbolic execution.
Proceedings of the 38th International Conference on Software Engineering, 2016
2015
Type Assisted Synthesis of Recursive Transformers on Algebraic Data Types.
CoRR, 2015
JSketch: sketching for Java.
Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015
Adaptive Concretization for Parallel Program Synthesis.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015
2014
Natural proofs for data structure manipulation in C using separation logic.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014
2013
Automatic techniques for proving correctness of heap-manipulating programs
PhD thesis, 2013
Natural proofs for structure, data, and separation.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013
2012
Recursive proofs for inductive tree data-structures.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012
2011
UML interaction model-driven runtime verification of Java programs.
IET Softw., 2011
Efficient Decision Procedures for Heaps Using STRAND.
Proceedings of the Static Analysis - 18th International Symposium, 2011
Decidable logics combining heap structures and data.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011
2009
UML Activity Diagram-Based Automatic Test Case Generation For Java Programs.
Comput. J., 2009
A Formal Architecture Pattern for Real-Time Distributed Systems.
Proceedings of the 30th IEEE Real-Time Systems Symposium, 2009
2008
UML state machine diagram driven runtime verification of Java programs for message interaction consistency.
Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), 2008
2006
Automatic Test Case Generation for UML Activity Diagrams.
Proceedings of the 2006 International Workshop on Automation of Software Test, 2006
Runtime Verification of Java Programs for Scenario-Based Specifications.
Proceedings of the Reliable Software Technologies, 2006