We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
We receive 5 Contributor Projects for Google Summer of Code 2024

Publications of Po-Chun Chien

Articles in journal or book chapters

  1. Dirk Beyer, Po-Chun Chien, Marek Jankola, and Nian-Ze Lee. A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification. Proc. ACM Softw. Eng., 1(FSE), 2024. ACM. doi:10.1145/3660797 Link to this entry Keyword(s): CPAchecker, Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
    Artifact(s)
    Abstract
    Assuring the correctness of computing systems is fundamental to our society and economy, and formal verification is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, Craig interpolation has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking: (1) Interpolation-Sequence-Based Model Checking (Vizel and Grumberg, 2009) and (2) Intertwined Forward-Backward Reachability Analysis Using Interpolants (Vizel, Grumberg, and Shoham, 2013) for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks in the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware/software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.
    BibTeX Entry
    @article{ItpTransfer-PACMSE, author = {Dirk Beyer and Po-Chun Chien and Marek Jankola and Nian-Ze Lee}, title = {A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification}, journal = {Proc. ACM Softw. Eng.}, volume = {1}, number = {FSE}, year = {2024}, publisher = {ACM}, doi = {10.1145/3660797}, url = {https://www.sosy-lab.org/research/dar-ismc-transferability/}, pdf = {https://www.sosy-lab.org/research/pub/2024-FSE.A_Transferability_Study_of_Interpolation-Based_Hardware_Model_Checking_to_Software_Verification.pdf}, presentation = {}, abstract = {Assuring the correctness of computing systems is fundamental to our society and economy, and <em>formal verification</em> is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, <em>Craig interpolation</em> has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking: (1) <em>Interpolation-Sequence-Based Model Checking</em> (<a href="https://doi.org/10.1109/FMCAD.2009.5351148">Vizel and Grumberg, 2009</a>) and (2) <em>Intertwined Forward-Backward Reachability Analysis Using Interpolants</em> (<a href="https://doi.org/10.1007/978-3-642-36742-7_22">Vizel, Grumberg, and Shoham, 2013</a>) for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks in the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware/software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.}, keyword = {CPAchecker,Software Model Checking}, articleno = {90}, artifact = {10.5281/zenodo.11070973}, funding = {DFG-CONVEY}, issue_date = {July 2024}, numpages = {23}, }

Articles in conference or workshop proceedings

  1. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants. In Proc. SPIN, 2024. Springer. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY PDF Presentation Supplement
    Artifact(s)
    Abstract
    Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
    BibTeX Entry
    @inproceedings{SPIN24b, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants}, booktitle = {Proc.\ SPIN}, pages = {}, year = {2024}, series = {}, publisher = {Springer}, url = {https://www.sosy-lab.org/research/imc-df/}, pdf = {https://www.sosy-lab.org/research/pub/2024-SPIN.Augmenting_Interpolation-Based_Model_Checking_with_Auxiliary_Invariants.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-10_SPIN_Augmenting_IMC_with_Auxiliary_Invariants_Po-Chun.pdf}, abstract = {Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including <i>k</i>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, annote = {This article received the "Best Paper Award" at SPIN 2024! An <a href="https://www.sosy-lab.org/research/bib/All/index.html#TechReport24a">extended version</a> of this article is available on <a href="https://doi.org/10.48550/arXiv.2403.07821">arXiv</a>.}, artifact = {10.5281/zenodo.10548594}, doinone = {Unpublished: Last checked: 2024-03-16}, funding = {DFG-CONVEY}, }
    Additional Infos
    This article received the "Best Paper Award" at SPIN 2024! An extended version of this article is available on arXiv.
  2. Daniel Baier, Dirk Beyer, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Martin Spiessl, Henrik Wachowitz, and Philipp Wendler. CPAchecker 2.3 with Strategy Selection (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 359-364, 2024. Springer. doi:10.1007/978-3-031-57256-2_21 Link to this entry Keyword(s): Software Model Checking, Witness-Based Validation, CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX Publisher's Version PDF Supplement
    Artifact(s)
    Abstract
    CPAchecker is a versatile framework for software verification, rooted in the established concept of configurable program analysis. Compared to the last published system description at SV-COMP 2015, the CPAchecker submission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses in CPAchecker and cover the full spectrum of the diverse program characteristics and specifications in the competition, we use strategy selection to predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses using k-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms in CPAchecker enables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories. CPAchecker also generates verification witnesses in the new YAML format.
    BibTeX Entry
    @inproceedings{TACAS24c, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Martin Spiessl and Henrik Wachowitz and Philipp Wendler}, title = {{CPAchecker} 2.3 with Strategy Selection (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {359-364}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_21}, url = {https://cpachecker.sosy-lab.org/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPAchecker_2.3_with_Strategy_Selection_Competition_Contribution.pdf}, abstract = {CPAchecker is a versatile framework for software verification, rooted in the established concept of configurable program analysis. Compared to the last published system description at SV-COMP 2015, the CPAchecker submission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses in CPAchecker and cover the full spectrum of the diverse program characteristics and specifications in the competition, we use strategy selection to predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses using <i>k</i>-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms in CPAchecker enables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories. CPAchecker also generates verification witnesses in the new YAML format.}, keyword = {Software Model Checking, Witness-Based Validation, CPAchecker}, artifact = {10.5281/zenodo.10203297}, funding = {DFG-CONVEY, DFG-IDEFIX}, }
  3. Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee, and Nils Sirrenberg. Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers. In Proc. TACAS (3), LNCS 14572, pages 129-149, 2024. Springer. doi:10.1007/978-3-031-57256-2_7 Link to this entry Keyword(s): Software Model Checking, Witness-Based Validation, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    Artifact(s)
    Abstract
    Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier CBMC on translated programs, it uniquely solved, with confirmed witnesses, 8% of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.
    BibTeX Entry
    @inproceedings{TACAS24a, author = {Zsófia Ádám and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee and Nils Sirrenberg}, title = {{Btor2-Cert}: {A} Certifying Hardware-Verification Framework Using Software Analyzers}, booktitle = {Proc.\ TACAS~(3)}, pages = {129-149}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_7}, url = {https://www.sosy-lab.org/research/btor2-cert/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.Btor2-Cert_A_Certifying_Hardware-Verification_Framework_Using_Software_Analyzers.pdf}, abstract = {Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier CBMC on translated programs, it uniquely solved, with confirmed witnesses, 8&percnt; of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.}, keyword = {Software Model Checking, Witness-Based Validation, Cooperative Verification, Btor2}, annote = {The reproduction package of this article received the "Distinguished Artifact Award" at TACAS 2024!}, artifact = {10.5281/zenodo.10548597}, funding = {DFG-CONVEY}, }
    Additional Infos
    The reproduction package of this article received the "Distinguished Artifact Award" at TACAS 2024!
  4. Po-Chun Chien and Nian-Ze Lee. CPV: A Circuit-Based Program Verifier (Competition Contribution). In Proc. TACAS, LNCS 14572, pages 365-370, 2024. Springer. doi:10.1007/978-3-031-57256-2_22 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)
    Abstract
    We submit to SV-COMP 2024 CPV, a circuit-based software verifier for C programs. CPV utilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and k-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition, CPV achieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the category ReachSafety, it outperformed several mature software verifiers as a first-year participant. CPV manifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.
    BibTeX Entry
    @inproceedings{CPV-TACAS24, author = {Po-Chun Chien and Nian-Ze Lee}, title = {CPV: A Circuit-Based Program Verifier (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {365-370}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_22}, url = {https://gitlab.com/sosy-lab/software/cpv}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPV_A_Circuit-Based_Program_Verifier_Competition_Contribution.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-08_SVCOMP_CPV_A_Circuit-Based_Program_Verifier_Po-Chun.pdf}, abstract = {We submit to SV-COMP 2024 CPV, a circuit-based software verifier for C programs. CPV utilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and <i>k</i>-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition, CPV achieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the category <i>ReachSafety</i>, it outperformed several mature software verifiers as a first-year participant. CPV manifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, artifact = {10.5281/zenodo.10203472}, funding = {DFG-CONVEY}, }
  5. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification. In Proc. ASE, pages 2050-2053, 2023. IEEE. doi:10.1109/ASE56229.2023.00213 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Artifact(s)
    Abstract
    Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPAchecker, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use CoVeriTeam, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20%.
    Demonstration video: https://youtu.be/l7UG-vhTL_4
    BibTeX Entry
    @inproceedings{ASE23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{CPA-DF}: {A} Tool for Configurable Interval Analysis to Boost Program Verification}, booktitle = {Proc.\ ASE}, pages = {2050-2053}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00213}, url = {https://www.sosy-lab.org/research/cpa-df/}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.CPA-DF_A_Tool_for_Configurable_Interval_Analysis_to_Boost_Program_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-09-13_ASE_CPA-DF_Po-Chun.pdf}, abstract = {Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the <i>k</i>-induction implementation in <a href="https://cpachecker.sosy-lab.org/">CPAchecker</a>, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on <a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">SV-Benchmarks</a>, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain <i>k</i>-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain <i>k</i>-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized <i>k</i>-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use <a href="https://gitlab.com/sosy-lab/software/coveriteam">CoVeriTeam</a>, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20&percnt;. <br> Demonstration video: <a href="https://youtu.be/l7UG-vhTL_4">https://youtu.be/l7UG-vhTL_4</a>}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, artifact = {10.5281/zenodo.8245821}, funding = {DFG-CONVEY}, video = {https://youtu.be/l7UG-vhTL_4}, }
  6. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. In Proc. TACAS, LNCS 13994, pages 152-172, 2023. Springer. doi:10.1007/978-3-031-30820-8_12 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)
    Abstract
    Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose the Btor2 language as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.
    BibTeX Entry
    @inproceedings{TACAS23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Bridging Hardware and Software Analysis with {Btor2C}: {A} Word-Level-Circuit-to-{C} Translator}, booktitle = {Proc.\ TACAS}, pages = {152-172}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_12}, url = {https://www.sosy-lab.org/research/btor2c/}, presentation = {https://www.sosy-lab.org/research/prs/2023-04-26_TACAS23_Bridging_Hardware_and_Software_Analysis_with_Btor2C_Po-Chun.pdf}, abstract = {Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose <a href="https://doi.org/10.1007/978-3-319-96145-3_32">the Btor2 language</a> as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, _pdf = {https://www.sosy-lab.org/research/pub/2023-TACAS.Bridging_Hardware_and_Software_Analysis_with_Btor2C_A_Word-Level-Circuit-to-C_Translator.pdf}, artifact = {10.5281/zenodo.7551707}, funding = {DFG-CONVEY}, }

Internal reports

  1. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version). Technical report 2403.07821, arXiv/CoRR, March 2024. doi:10.48550/arXiv.2403.07821 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Supplement
    Artifact(s)
    Abstract
    Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
    BibTeX Entry
    @techreport{TechReport24a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)}, number = {2403.07821}, year = {2024}, doi = {10.48550/arXiv.2403.07821}, url = {https://www.sosy-lab.org/research/imc-df/}, pdf = {https://arxiv.org/abs/2403.07821}, abstract = {Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including <i>k</i>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#SPIN24b">paper</a> at SPIN 2024.}, artifact = {10.5281/zenodo.10548594}, funding = {DFG-CONVEY}, institution = {arXiv/CoRR}, month = {March}, }
    Additional Infos
    This technical report is an extended version of our paper at SPIN 2024.

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: Wed May 22 01:04:40 2024 UTC