2025
On Temporal Verification of Stateful P4 Programs.
Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation, 2025
Robustness Verification for Checking Crash Consistency of Non-volatile Memory.
Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2025
2024
Leveraging Datapath Propagation in IC3 for Hardware Model Checking.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., July, 2024
P4Inv: Inferring Packet Invariants for Verification of Stateful P4 Programs.
Proceedings of the IEEE INFOCOM 2024, 2024
2023
On the methodology of three-way structured merge in version control systems: Top-down, bottom-up, or both.
J. Syst. Archit., December, 2023
Automated Ambiguity Detection in Layout-Sensitive Grammars.
Proc. ACM Program. Lang., October, 2023
Learning Adaptive Node Embeddings Across Graphs.
IEEE Trans. Knowl. Data Eng., June, 2023
A Characterization Study of Merge Conflicts in Java Projects.
ACM Trans. Softw. Eng. Methodol., April, 2023
Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models.
ACM Trans. Program. Lang. Syst., March, 2023
P4b: A Translator from P4 Programs to Boogie.
Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023
Data-driven Recurrent Set Learning For Non-termination Analysis.
Proceedings of the 45th IEEE/ACM International Conference on Software Engineering, 2023
2022
Efficient Summary Reuse for Software Regression Verification.
IEEE Trans. Software Eng., 2022
Consistency-preserving propagation for SMT solving of concurrent program verification.
Proc. ACM Program. Lang., 2022
Lay-it-out: Interactive Design of Layout-Sensitive Grammars.
CoRR, 2022
ProbTA: A sound and complete proof rule for probabilistic verification.
CoRR, 2022
Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022
Mastery: Shifted-Code-Aware Structured Merging.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2022
EqFix: Fixing LaTeX Equation Errors by Examples.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2022
Interference relation-guided SMT solving for multi-threaded program verification.
Proceedings of the PPoPP '22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2, 2022
Data-Driven Loop Bound Learning for Termination Analysis.
Proceedings of the 44th IEEE/ACM 44th International Conference on Software Engineering, 2022
2021
Leveraging Control Flow Knowledge in SMT Solving of Program Verification.
ACM Trans. Softw. Eng. Methodol., 2021
PSpec-SQL: Enabling Fine-Grained Control for Distributed Data Analytics.
IEEE Trans. Dependable Secur. Comput., 2021
Automatic Detection and Resolution of Software Merge Conflicts: Are We There Yet?
CoRR, 2021
Satisfiability modulo ordering consistency theory for multi-threaded program verification.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021
2020
Incremental predicate analysis for regression verification.
Proc. ACM Program. Lang., 2020
Termination analysis for evolving programs: an incremental approach by reusing certified modules.
Proc. ACM Program. Lang., 2020
Interval counterexamples for loop invariant learning.
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020
Proving almost-sure termination by omega-regular decomposition.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020
Proving Termination by k-Induction.
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020
2019
Enhancing precision of structured merge by proper tree matching.
Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, 2019
2018
Conflict resolution for structured merge via version space algebra.
Proc. ACM Program. Lang., 2018
SMT-based query tracking for differentially private data analytics systems.
Frontiers Comput. Sci., 2018
Efficient software product-line model checking using induction and a SAT solver.
Frontiers Comput. Sci., 2018
When Regression Verification Meets CEGAR.
CoRR, 2018
Control flow-guided SMT solving for program verification.
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018
2017
Inferring software behavioral models with MapReduce.
Sci. Comput. Program., 2017
Verification of Implementations of Cryptographic Hash Functions.
IEEE Access, 2017
PSpec: a formal specification language for fine-grained control on distributed data analytics.
Proceedings of the 39th International Conference on Software Engineering, 2017
Assertion Recommendation for Formal Program Verification.
Proceedings of the 41st IEEE Annual Computer Software and Applications Conference, 2017
2016
Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes.
ACM Trans. Softw. Eng. Methodol., 2016
Learning-Based Assume-Guarantee Regression Verification.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016
2015
Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic.
Theory Comput. Syst., 2015
Generalized interface automata with multicast synchronization.
Frontiers Comput. Sci., 2015
Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015
VeRV: A temporal and data-concerned verification framework for the vehicle bus systems.
Proceedings of the 2015 IEEE Conference on Computer Communications, 2015
2014
Array Theory of Bounded Elements and its Applications.
J. Autom. Reason., 2014
Symbolic assume-guarantee reasoning through BDD learning.
Proceedings of the 36th International Conference on Software Engineering, 2014
Clause Replication and Reuse in Incremental Temporal Induction.
Proceedings of the 2014 19th International Conference on Engineering of Complex Computer Systems, 2014
2013
A Unified Framework for DPLL(T) + Certificates.
J. Appl. Math., 2013
Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information.
Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013
Reusing Search Tree for Incremental SAT Solving of Temporal Induction.
Proceedings of the 2013 18th International Conference on Engineering of Complex Computer Systems, 2013
Component-Based Modeling and Code Synthesis for Cyclic Programs.
Proceedings of the 37th Annual IEEE Computer Software and Applications Conference, 2013
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013
VCS: A Verifier for Component-Based Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2013
2012
Maxterm Covering for Satisfiability.
IEEE Trans. Computers, 2012
Thread-Modular Model Checking with Iterative Refinement.
Proceedings of the NASA Formal Methods, 2012
2011
An Efficient Resolution Based Algorithm for SAT.
Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011
2010
Integrating Evolutionary Computation with Abstraction Refinement for Model Checking.
IEEE Trans. Computers, 2010
An Analytical Congestion Model with Bounded-Bend Detours.
J. Circuits Syst. Comput., 2010
Compositional Abstraction Refinement for Timed Systems.
Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010
On Array Theory of Bounded Elements.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010
2009
Heuristic-Guided Abstraction Refinement.
Comput. J., 2009
Data mining based decomposition for assume-guarantee reasoning.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009
Translation-Based Model Checking for PLC Programs.
Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference, 2009
2007
A note on "a mapping algorithm for computer-assisted exploration in the design of embedded systems".
ACM Trans. Design Autom. Electr. Syst., 2007
Effective heuristics for counterexample-guided abstraction refinement.
Proceedings of the 17th ACM Great Lakes Symposium on VLSI 2007, 2007
Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2007
2006
Probabilistic optimization for FPGA board level routing problems.
IEEE Trans. Circuits Syst. II Express Briefs, 2006
Congestion estimation for hexagonal routing.
Int. J. Comput. Math., 2006
A combinatorial congestion estimation approach with generalized detours.
Comput. Math. Appl., 2006
Verifying Java Programs By Theorem Prover HOL.
Proceedings of the 30th Annual International Computer Software and Applications Conference, 2006
A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement.
Proceedings of the Automated Technology for Verification and Analysis, 2006
2005
Multiterminal net assignments by scatter search.
Math. Comput. Model., 2005
On Theoretical Upper Bounds for Routing Estimation.
J. Univers. Comput. Sci., 2005
Probabilistic Estimation for Routing Space.
Comput. J., 2005
A Hierachical Method for Wiring and Congestion Prediction.
Proceedings of the 2005 IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2005), 2005
Segmented channel routing with pin rearrangements via satisfiability.
Proceedings of the International Symposium on Circuits and Systems (ISCAS 2005), 2005
2004
A stochastic model for cellassignments in PCS networks.
Math. Comput. Model., 2004
A comparative study on search strategies for cell assignments.
Int. J. Comput. Math., 2004