Software and Computational Systems Lab

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers.

Goal: Now that a large collection of tools from both hardware and software verification communities are at our disposal, we want to combine forces of them via machine learning (ML). The objective is to construct a selector using information of the circuit structure of a Btor2 circuit [3], and train it on a large Btor2 dataset. Given a Btor2 task, the ML-based selector can then predict the best-suited tool/algorithm(s) for solving it.

Requirements: (general information)

• Ability to program in Python
• Basic knowledge of graph kernel, Kripke structure, and SAT/SMT solving
• Practical knowledge of support vector machine, decision/boosting tree, and random forest

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers.

Goal: Now that a large collection of tools from both hardware and software verification communities are at our disposal, we want to combine forces of them via machine learning (ML). The objective is to construct a selector using syntactic features of a Btor2 circuit, e.g. the numbers of certain operations, and train it on a large Btor2 dataset. Given a Btor2 task, the ML-based selector can then predict the best-suited tool/algorithm(s) for solving it.

Requirements: (general information)

• Ability to program in Python
• Basic knowledge of Kripke structure and SAT/SMT solving
• Practical knowledge of support vector machine, decision/boosting tree, and random forest

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers, e.g. CPAchecker. A Btor2 bit-vector can have an arbitrary width, and Btor2C encodes it with the shortest possible C integer. Thus, the C-integer variable might have some redundant bits, which complicates the analysis and harms the performance of software verifiers.

Goal: In this project, we want to implement a new frontend in CPAchecker to parse a Btor2 verification problem and represent it as a control-flow automaton. With this new frontend, CPAchecker could analyze a Btor2 circuit directly and (hopefully) more efficiently.

Requirements: (general information)

• Ability to program in Java
• Basic knowledge of Kripke structure and SAT/SMT solving

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers, e.g. CPAchecker. A Btor2 bit-vector can have an arbitrary width, and Btor2C encodes it with the shortest possible C integer. Thus, the C-integer variable might have some redundant bits, which complicates the analysis and harms the performance of software verifiers.

Goal: The goal of this project is to support bit-precise integer representation in CPAchecker specifically for these hardware-verification tasks. One possible way to achieve this is by defining a customized C annotation such that CPAchecker can infer the precise bit-width.

Requirements: (general information)

• Ability to program in Java and C
• Basic knowledge of Kripke structure and SAT/SMT solving