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, 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. If a software verifier finds an error in the program, it generates a violation witness, which records the execution path leading to that error. On the other hand, if a software verifier proves a program correct, it generates a correctness witness [3] containing some program invariants that could reconstruct a correctness proof.

Goal: The goal of this project to certify the correctness witnesses (in GraphML format) produced by software verifiers by following the validation-via-verification approach [4]. The original Btor2 circuit is instrumented with the invariants from a correctness witness, and can then be independently solved by hardware verifiers.

Requirements: (general information)

• Ability to program in Python (, Java, and/or C)
• 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. If a software verifier finds an error in the program, it generates a violation witness [3], which records the execution path leading to that error. On the other hand, if a software verifier proves a program correct, it generates a correctness witness containing some program invariants that could reconstruct a correctness proof.

Goal: The goal of this project to translate the violation witnesses in GraphML format produced by software verifiers to Btor2 format, such that one could use hardware simulators to validate them.

Requirements: (general information)

• Ability to program in Python (, Java, and/or C)
• 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

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 Btor2 circuit structure [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 analyzers. Currently, on every write of an array, Btor2C creates a copy of it, even when unnecessary (see this issue). This might put burdens on software analyzers and hinders their performance.

Goal: The goal of this project is to alleviate such situation and allocate a new array only when necessary. Additionally, we also want to implement a translator that converts Btor2 array tasks to pure bit-vector tasks by blasting the array operations (read and write) into a chain of ite operations.

Requirements: (general information)

• Ability to program in C (and/or Python)
• Basic knowledge of Kripke structure and SAT/SMT solving

Description: Bounded model checking (BMC) is a well-known software analysis technique that searches for execution paths that could lead to the error location from the initial program location. Backward BMC, on the contrary, follows the execution backward and searches paths from the error location to the initial location. The goal of the project is to implement such technique in CPAchecker.

Requirements: (general information)

• Ability to program in Java and understand C code
• Basic knowledge of SAT/SMT solving and weakest precondition