We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Distinguished Paper at ETAPS 2026!

Talks about Btor2

Guest lectures, invited talks, and tutorials
  1. Po-Chun Chien. From Programs to Circuits: Bridging Software and Hardware Model Checking with CPV and Pono. Invited talk at Graduate Institute of Electronics Engineering, National Taiwan University, 22. December 2025. Link to this entry Keyword(s): Software Model Checking, Btor2, SMT, Competition on Software Verification Presentation
    BibTeX Entry
    @invitedtalk{NTU25-CPV, author = {Po-Chun Chien}, title = {From Programs to Circuits: Bridging Software and Hardware Model Checking with CPV and Pono}, year = {2025}, presentation = {https://www.sosy-lab.org/research/prs/2025-12-22_GIEE-NTU.From_Programs_to_Circuits_Po-Chun.pdf}, keyword = {Software Model Checking, Btor2, SMT, Competition on Software Verification}, day = {22}, field = {Computer Science}, month = {December}, venue = {Graduate Institute of Electronics Engineering, National Taiwan University}, }

Conference and other Presentations
  1. Po-Chun Chien. MoXIchecker: An Extensible Model Checker for MoXI. Conference talk at SPIN, 07. May 2025. Link to this entry Keyword(s): SMT, Btor2, MoXIchecker Presentation
    BibTeX Entry
    @conferencetalk{SPIN-MoXIchecker, author = {Po-Chun Chien}, title = {{MoXIchecker}: {An} Extensible Model Checker for {MoXI}}, year = {2025}, presentation = {https://www.sosy-lab.org/research/prs/2025-05-07_SPIN_MoXIchecker_An_Extensible_Model_Checker_for_MoXI_Po-Chun.pdf}, keyword = {SMT, Btor2, MoXIchecker}, day = {07}, field = {Computer Science}, month = {May}, venue = {SPIN}, }
  2. Po-Chun Chien. CPV: A Circuit-Based Program Verifier. Conference talk at TACAS, 05. May 2025. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2, Competition on Software Verification Presentation
    BibTeX Entry
    @conferencetalk{SVCOMP25-CPV, author = {Po-Chun Chien}, title = {{CPV}: {A} Circuit-Based Program Verifier}, year = {2025}, presentation = {https://www.sosy-lab.org/research/prs/2025-05-05_SVCOMP_CPV_A_Circuit-Based_Program_Verifier_Po-Chun.pdf}, keyword = {Software Model Checking, Cooperative Verification, Btor2, Competition on Software Verification}, day = {05}, field = {Computer Science}, month = {May}, poster = {https://www.sosy-lab.org/research/pst/2025-05-05_ETAPS_CPV_Poster.pdf}, venue = {TACAS}, }
  3. Po-Chun Chien. Bridging Hardware and Software Formal Verification. Conference talk at FM Doctoral Symposium, 10. September 2024. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2, CPAchecker, Witness-Based Validation Presentation
    BibTeX Entry
    @conferencetalk{FM24-BridgingHwSw, author = {Po-Chun Chien}, title = {Bridging Hardware and Software Formal Verification}, year = {2024}, presentation = {https://www.sosy-lab.org/research/prs/2024-09-10_FM24_Bridging_Hardware_and_Software_Formal_Verification_Po-Chun.pdf}, keyword = {Software Model Checking, Cooperative Verification, Btor2, CPAchecker, Witness-Based Validation}, day = {10}, field = {Computer Science}, month = {September}, poster = {https://www.sosy-lab.org/research/pst/2024-09-10_FM24_Bridging_Hardware_and_Software_Formal_Verification_Poster.pdf}, venue = {FM Doctoral Symposium}, }
  4. Po-Chun Chien. CPV: A Circuit-Based Program Verifier. Conference talk at TACAS, 08. April 2024. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2, Competition on Software Verification Presentation
    BibTeX Entry
    @conferencetalk{SVCOMP24-CPV, author = {Po-Chun Chien}, title = {{CPV}: {A} Circuit-Based Program Verifier}, year = {2024}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-08_SVCOMP_CPV_A_Circuit-Based_Program_Verifier_Po-Chun.pdf}, keyword = {Software Model Checking, Cooperative Verification, Btor2, Competition on Software Verification}, day = {08}, field = {Computer Science}, month = {April}, poster = {https://www.sosy-lab.org/research/pst/2024-03-22_ETAPS_CPV_Poster.pdf}, venue = {TACAS}, }
  5. Po-Chun Chien. Cross-Application of Hardware and Software Verification. Conference talk at ConVeY Workhop 2024 (co-located with ETAPS), 06. April 2024. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Verification Witnesses, Btor2 Presentation
    BibTeX Entry
    @conferencetalk{ConVeY24-CrossApplyHwSwVerification, author = {Po-Chun Chien}, title = {Cross-Application of Hardware and Software Verification}, year = {2024}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-06_ConVeY_Cross-Application_of_HW_SW_Verification_Po-Chun.pdf}, keyword = {Software Model Checking, Cooperative Verification, Verification Witnesses, Btor2}, day = {06}, field = {Computer Science}, month = {April}, venue = {<a href="https://convey.ifi.lmu.de/workshops/2024/spring/program.html">ConVeY Workhop 2024</a> (co-located with ETAPS)}, }
  6. Dirk Beyer. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. Conference talk at AVM, 13. September 2023. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Presentation
    BibTeX Entry
    @conferencetalk{AVM23Btor2C, author = {Dirk Beyer}, title = {Bridging Hardware and Software Analysis with {Btor2C}: {A} Word-Level-Circuit-to-{C} Translator}, year = {2023}, presentation = {https://www.sosy-lab.org/research/prs/2023-09-13_AVM23_Bridging_Hardware_and_Software_Analysis_with_Btor2C_Dirk.pdf}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, day = {13}, field = {Computer Science}, month = {September}, venue = {AVM}, }
  7. Po-Chun Chien. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. Conference talk at TACAS, 26. April 2023. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Presentation
    BibTeX Entry
    @conferencetalk{TACAS23-Btor2C, author = {Po-Chun Chien}, title = {Bridging Hardware and Software Analysis with {Btor2C}: {A} Word-Level-Circuit-to-{C} Translator}, year = {2023}, presentation = {https://www.sosy-lab.org/research/prs/2023-04-26_TACAS23_Bridging_Hardware_and_Software_Analysis_with_Btor2C_Po-Chun.pdf}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, day = {26}, field = {Computer Science}, month = {April}, poster = {https://www.sosy-lab.org/research/pst/2023-04-24_ETAPS_Btor2C_Poster.pdf}, venue = {TACAS}, }

Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Last modified: Mon Feb 09 18:28:37 2026 UTC