Author of the publication

Towards a unified proof framework for automated fixpoint reasoning using matching logic.

, , , , and . Proc. ACM Program. Lang., 4 (OOPSLA): 161:1-161:29 (2020)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

FixBag: A Fixpoint Calculator for Quantified Bag Constraints., , , and . CAV, volume 6806 of Lecture Notes in Computer Science, page 656-662. Springer, (2011)Automating Proofs of Data-Structure Properties in Imperative Programs., , and . CoRR, (2014)Towards a unified proof framework for automated fixpoint reasoning using matching logic., , , , and . Proc. ACM Program. Lang., 4 (OOPSLA): 161:1-161:29 (2020)Towards a Trustworthy Semantics-Based Language Framework via Proof Generation., , , and . CAV (2), volume 12760 of Lecture Notes in Computer Science, page 477-499. Springer, (2021)Inter-theory dependency analysis for SMT string solvers., , and . Proc. ACM Program. Lang., 4 (OOPSLA): 192:1-192:27 (2020)Bi-Abduction with Pure Properties for Specification Inference., , , and . APLAS, volume 8301 of Lecture Notes in Computer Science, page 107-123. Springer, (2013)Model Counting for Recursively-Defined Strings., , and . CAV (2), volume 10427 of Lecture Notes in Computer Science, page 399-418. Springer, (2017)Progressive Reasoning over Recursively-Defined Strings., , and . CAV (1), volume 9779 of Lecture Notes in Computer Science, page 218-240. Springer, (2016)Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier., , , , and . Proc. ACM Program. Lang., 7 (OOPSLA1): 56-84 (April 2023)Automatic induction proofs of data-structures in imperative programs., , and . PLDI, page 457-466. ACM, (2015)