1 citations · 2 across the 3 of their papers we have counts for
5 papers
Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs
Po-Chun Chien, Nian-Ze Lee, Armin Biere +1
Formal verification of software programs and hardware designs shares the common goal of reasoning about state-transition systems, yet the two communities have largely developed sep…
Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
Daniel Baier, Dirk Beyer, Po-Chun Chien +8
This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides ma…
MoXIchecker: An Extensible Model Checker for MoXI
Salih Ates, Dirk Beyer, Po-Chun Chien +1
MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-…
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
Dirk Beyer, Po-Chun Chien, Nian-Ze Lee
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 obtain…
Logic Synthesis Meets Machine Learning: Trading Exactness for Generalization
Shubham Rai, Walter Lau Neto, Yukio Miyasaka +37
Logic synthesis is a fundamental step in hardware design whose goal is to find structural representations of Boolean functions while minimizing delay and area. If the function is c…